OAI/Geometry/Relativity/CKS/SurfaceChristoffel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.metric_normal_pair line 12
2. lemma OAI.CKSSchwarzschild.christoffel_tangent_radial line 22
3. lemma OAI.CKSSchwarzschild.christoffel_neg_normal line 48
4. lemma OAI.CKSSchwarzschild.parameterSecondForm_neg line 52
5. lemma OAI.CKSSchwarzschild.parameterMeanCurvature_neg line 56