OAI/Geometry/Relativity/CKS/SchwarzschildBoundary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.boundary_height line 13
2. def OAI.CKSSchwarzschild.boundarySphere line 16
3. lemma OAI.CKSSchwarzschild.boundarySphere_smooth line 29
4. lemma OAI.CKSSchwarzschild.mfderiv_boundarySphere line 31
5. lemma OAI.CKSSchwarzschild.boundarySphere_symm_chart line 42
6. lemma OAI.CKSSchwarzschild.boundarySphere_symm_smooth line 51
7. lemma OAI.CKSSchwarzschild.mfderiv_boundarySphere_symm line 59
8. lemma OAI.CKSSchwarzschild.boundary_compact line 68