OAI/Geometry/Relativity/CKS/SchwarzschildPosition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.radius_pos line 13
2. lemma OAI.CKSSchwarzschild.radius_ge line 17
3. lemma OAI.CKSSchwarzschild.radius_smooth line 21
4. lemma OAI.CKSSchwarzschild.directionAmbient_smooth line 23
5. lemma OAI.CKSSchwarzschild.position_smooth line 25
6. lemma OAI.CKSSchwarzschild.norm_direction line 27
7. lemma OAI.CKSSchwarzschild.norm_position line 29
8. lemma OAI.CKSSchwarzschild.position_ne_zero line 31
9. lemma OAI.CKSSchwarzschild.mfderiv_radius line 34
10. lemma OAI.CKSSchwarzschild.mfderiv_directionAmbient line 42
11. lemma OAI.CKSSchwarzschild.directionAmbient_orthogonal line 52
12. def OAI.CKSSchwarzschild.ambientDerivative line 64
13. lemma OAI.CKSSchwarzschild.mfderiv_position line 67
14. lemma OAI.CKSSchwarzschild.position_derivative_injective line 87