OAI/Geometry/Immersion/ClosedSurface/ChartTransition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.coordinateChart line 15
2. lemma OAI.ClosedSurfaceR4.coordinateChart_source line 18
3. lemma OAI.ClosedSurfaceR4.coordinateChart_apply line 22
4. lemma OAI.ClosedSurfaceR4.coordinateChart_symm_apply line 24
5. lemma OAI.ClosedSurfaceR4.coordinateChart_target line 28
6. lemma OAI.ClosedSurfaceR4.coordinateChart_smoothOn line 34
7. lemma OAI.ClosedSurfaceR4.coordinateChart_symm_smoothOn line 39
8. def OAI.ClosedSurfaceR4.coordinateTransition line 48
9. lemma OAI.ClosedSurfaceR4.coordinateTransition_smoothOn line 51
10. lemma OAI.ClosedSurfaceR4.coordinateTransition_symm line 58
11. lemma OAI.ClosedSurfaceR4.coordinateTransition_symm_smoothOn line 62
12. theorem OAI.ClosedSurfaceR4.coordinateTransition_compact_bounds line 70