OAI/Geometry/Relativity/CKS/SchwarzschildCharts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.transition_source line 14
2. lemma OAI.CKSSchwarzschild.transition_maps line 21
3. lemma OAI.CKSSchwarzschild.transition_formula line 32
4. lemma OAI.CKSSchwarzschild.boundary_iff line 41
5. lemma OAI.CKSSchwarzschild.interior_iff line 44