OAI/Geometry/Relativity/CKS/CollarOrientation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.rawExpansionValue line 12
2. def OAI.CKSAngularGeometry.rawOrientedDomain line 13
3. lemma OAI.CKSAngularGeometry.rawExpansionValue_continuousAt line 15
4. lemma OAI.CKSAngularGeometry.rawOrientedDomain_open line 21
5. lemma OAI.CKSAngularGeometry.rawOrientedFamily_regular line 29
6. lemma OAI.CKSAngularGeometry.field_expansion_value line 38
7. theorem OAI.CKSAngularGeometry.bounded_thin_oriented_fields line 46
8. lemma OAI.CKSAngularGeometry.fieldNormalizedLapse_positive line 77