OAI/Geometry/Relativity/CKS/SurfaceDivergence.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CKSSchwarzschild.christoffel_metric_compatibilityline 13 - def
OAI.CKSSchwarzschild.parameterNormalDerivativeline 23 - lemma
OAI.CKSSchwarzschild.parameterSecondForm_eq_normalDerivativeline 27 - def
OAI.CKSSchwarzschild.parameterDivergenceline 46 - lemma
OAI.CKSSchwarzschild.parameterMeanCurvature_eq_divergenceline 51