OAI/Geometry/SplitTangent/BoxTransportBase.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SplitTangent.ReciprocalCharts.torus line 17
2. lemma OAI.SplitTangent.ReciprocalCharts.torus_open line 18
3. lemma OAI.SplitTangent.ReciprocalCharts.torus_dense line 21
4. def OAI.SplitTangent.ReciprocalCharts.coord line 24
5. def OAI.SplitTangent.ReciprocalCharts.scale line 25
6. def OAI.SplitTangent.ReciprocalCharts.changeChart line 26
7. lemma OAI.SplitTangent.ReciprocalCharts.coord_involutive line 28
8. lemma OAI.SplitTangent.ReciprocalCharts.coord_ne_zero line 30
9. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_involutive line 32
10. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_torus line 35
11. lemma OAI.SplitTangent.ReciprocalCharts.coord_xor line 37
12. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_xor line 39
13. lemma OAI.SplitTangent.ReciprocalCharts.coord_deriv line 42
14. lemma OAI.SplitTangent.ReciprocalCharts.coord_analytic line 47
15. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_analytic line 51
16. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_fderiv line 55
17. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_fderiv_first line 62
18. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_fderiv_second line 66
19. def OAI.SplitTangent.ReciprocalCharts.overlap line 72
20. lemma OAI.SplitTangent.ReciprocalCharts.torus_subset_overlap line 74
21. lemma OAI.SplitTangent.ReciprocalCharts.overlap_open line 76
22. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_analytic_on_overlap line 85
23. lemma OAI.SplitTangent.ReciprocalCharts.changeChart_transition line 100
24. structure OAI.SplitTangent.TangentBox line 111
25. def OAI.SplitTangent.TangentBox.firstFactor line 130
26. lemma OAI.SplitTangent.TangentBox.firstFactor_diagonal line 141
27. lemma OAI.SplitTangent.TangentBox.firstFactor_tangent line 144
28. theorem OAI.SplitTangent.TangentBox.exists_normalized_second_map line 162