OAI/Geometry/Relativity/CKS/MainProof.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSMain.InteriorSurface.schwarzschildImmersion line 16
2. lemma OAI.CKSMain.schwarzschild_no_additional_horizons line 28
3. lemma OAI.CKSMain.schwarzschild_attainment line 36
4. theorem OAI.CKSMain.conditional_connected_horizon line 56