OAI/Geometry/Relativity/CKS/SchwarzschildHorizon.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CKSSchwarzschild.future_horizon_realization line 11
2. lemma OAI.CKSSchwarzschild.radialNormal_unit line 36
3. lemma OAI.CKSSchwarzschild.radialNormal_points_out line 45
4. lemma OAI.CKSSchwarzschild.radialNormal_orthogonal line 51