OAI/Geometry/Relativity/CKS/SchwarzschildOrientability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.orientation_map_trans line 11
2. lemma OAI.CKSSchwarzschild.orientation_map_inverse_eq line 20
3. def OAI.CKSSchwarzschild.positionTangentEquiv line 43
4. lemma OAI.CKSSchwarzschild.positionTangentEquiv_apply line 48
5. theorem OAI.CKSSchwarzschild.source_orientable line 51