OAI/Geometry/Immersion/ClosedSurface/AtlasMargins.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.coordinateMap_transition line 16
2. lemma OAI.ClosedSurfaceR4.coordinateMap_transition_eventuallyEq line 28
3. theorem OAI.ClosedSurfaceR4.actual_chart_phase_margin line 37
4. lemma OAI.ClosedSurfaceR4.coordinateChart_compact_image line 75
5. lemma OAI.ClosedSurfaceR4.coordinateChart_image_overlap line 80
6. theorem OAI.ClosedSurfaceR4.compact_overlap_phase_margin line 93