OAI/Geometry/Symplectic/MorseBounds/CapEnd.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MorseArnold.CapEnd.chart line 17
2. def OAI.MorseArnold.CapEnd.ambient line 21
3. def OAI.MorseArnold.CapEnd.quadratic line 24
4. def OAI.MorseArnold.CapEnd.correction line 27
5. def OAI.MorseArnold.CapEnd.closedPath line 31
6. lemma OAI.MorseArnold.CapEnd.plane_inverse line 36
7. lemma OAI.MorseArnold.CapEnd.quad_inverse line 47
8. lemma OAI.MorseArnold.CapEnd.ambient_inverse line 54
9. lemma OAI.MorseArnold.CapEnd.chart_disjoint line 62
10. lemma OAI.MorseArnold.CapEnd.ambient_preserves line 70
11. lemma OAI.MorseArnold.CapEnd.ambient_outside line 76
12. lemma OAI.MorseArnold.CapEnd.correction_endpoint line 84
13. theorem OAI.MorseArnold.CapEnd.endpoint_count line 95
14. lemma OAI.MorseArnold.CapEnd.chart_target line 128
15. lemma OAI.MorseArnold.CapEnd.chart_smooth line 134
16. theorem OAI.MorseArnold.CapEnd.endpoint_nondegenerate line 144