OAI/Geometry/Relativity/CKS/SchwarzschildEnd.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSchwarzschild.sphereDefault line 13
2. def OAI.CKSSchwarzschild.sphereDirection line 14
3. lemma OAI.CKSSchwarzschild.sphereDirection_val line 16
4. lemma OAI.CKSSchwarzschild.sphereDirection_smoothAt line 18
5. def OAI.CKSSchwarzschild.positionInverse line 27
6. lemma OAI.CKSSchwarzschild.positionInverse_radius line 29
7. lemma OAI.CKSSchwarzschild.position_left_inverse line 33
8. lemma OAI.CKSSchwarzschild.position_right_inverse line 44
9. lemma OAI.CKSSchwarzschild.pair_smoothAt line 53
10. lemma OAI.CKSSchwarzschild.positionInverse_smoothAt line 69
11. lemma OAI.CKSSchwarzschild.radius_sublevel_compact line 79
12. def OAI.CKSSchwarzschild.coordinateEnd line 93