OAI/Geometry/Relativity/CKS/CollarLogSlices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSAngularSlice.AMat line 11
2. abbrev OAI.CKSAngularSlice.MJ line 12
3. abbrev OAI.CKSAngularSlice.M3 line 13
4. abbrev OAI.CKSAngularSlice.AJ line 14
5. abbrev OAI.CKSAngularSlice.A3 line 15
6. structure OAI.CKSAngularSlice.LogCollarData line 17
7. def OAI.CKSAngularSlice.LogCollarData.angular line 28
8. structure OAI.CKSAngularSlice.LogCollarData.RegularAt line 45
9. structure OAI.CKSAngularSlice.LogCollarData.BoundedAt line 56
10. theorem OAI.CKSAngularSlice.angular_thin_bounded line 67