OAI/Geometry/Relativity/CKS/SchwarzschildHorizonExclusionDefinitions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSchwarzschild.parameterSecondForm line 18
2. def OAI.CKSSchwarzschild.parameterMeanCurvature line 22
3. def OAI.CKSSchwarzschild.parameterTensorTrace line 27
4. def OAI.CKSSchwarzschild.surfaceParameter line 35
5. def OAI.CKSSchwarzschild.surfaceMeanCurvature line 37
6. def OAI.CKSSchwarzschild.surfaceTensorTrace line 40
7. structure OAI.CKSSchwarzschild.InteriorImmersion line 43