OAI/Geometry/Relativity/CKS/FoliationOrthonormalFrame.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.adaptedFrame line 11
2. lemma OAI.CKSAngularGeometry.metricPair_foliationNormal line 16
3. lemma OAI.CKSAngularGeometry.metricPair_normal_tangent line 21
4. lemma OAI.CKSAngularGeometry.adaptedFrame_radial line 37
5. lemma OAI.CKSAngularGeometry.adaptedFrame_first line 40
6. lemma OAI.CKSAngularGeometry.metricPair_tangent_expanded line 43
7. lemma OAI.CKSAngularGeometry.adaptedFrame_orthonormal line 50