OAI/Geometry/Relativity/CKS/SchwarzschildCoordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSchwarzschild.angular line 12
2. def OAI.CKSSchwarzschild.firstCoordinate line 14
3. lemma OAI.CKSSchwarzschild.extChart_formula line 16
4. lemma OAI.CKSSchwarzschild.inverseChart_height line 17
5. lemma OAI.CKSSchwarzschild.inverseChart_angular line 21
6. lemma OAI.CKSSchwarzschild.angular_chart_eq line 26
7. lemma OAI.CKSSchwarzschild.height_chart_eq line 44
8. lemma OAI.CKSSchwarzschild.angular_chart_self line 49
9. lemma OAI.CKSSchwarzschild.height_chart_self line 54
10. lemma OAI.CKSSchwarzschild.angular_smooth line 58
11. lemma OAI.CKSSchwarzschild.height_smooth line 63
12. lemma OAI.CKSSchwarzschild.mfderiv_angular line 68
13. lemma OAI.CKSSchwarzschild.mfderiv_height line 72