OAI/Geometry/Relativity/CKS/PhysicalLeafConnection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.angularLowerConnection line 11
2. lemma OAI.CKSAngularGeometry.foliation_lower_angular line 17
3. lemma OAI.CKSAngularGeometry.tangential_sum_pair line 23
4. lemma OAI.CKSAngularGeometry.tangential_sum_triple line 33
5. lemma OAI.CKSAngularGeometry.foliationMetric_angular line 50
6. lemma OAI.CKSAngularGeometry.source_tangential_connection line 54
7. def OAI.CKSAngularGeometry.inducedFrameCoefficient line 76
8. theorem OAI.CKSAngularGeometry.physical_leaf_connection line 86