OAI/Geometry/Symplectic/MorseBounds/CapGluing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MorseArnold.CapGluing.insert line 18
2. def OAI.MorseArnold.CapGluing.zeroExtend line 24
3. def OAI.MorseArnold.CapGluing.generator line 27
4. lemma OAI.MorseArnold.CapGluing.source_index_unique line 35
5. lemma OAI.MorseArnold.CapGluing.insert_in_source line 41
6. lemma OAI.MorseArnold.CapGluing.insert_outside line 50
7. lemma OAI.MorseArnold.CapGluing.coord_not_mem line 54
8. theorem OAI.MorseArnold.CapGluing.zeroExtend_smooth line 59
9. lemma OAI.MorseArnold.CapGluing.insert_off_support line 88
10. theorem OAI.MorseArnold.CapGluing.insert_smooth line 99
11. theorem OAI.MorseArnold.CapGluing.generator_smooth line 136
12. lemma OAI.MorseArnold.CapGluing.generator_in_source line 145
13. lemma OAI.MorseArnold.CapGluing.generator_outside line 160
14. lemma OAI.MorseArnold.CapGluing.insert_inverse line 165
15. theorem OAI.MorseArnold.CapGluing.insert_diffeomorphism line 181
16. lemma OAI.MorseArnold.CapGluing.inserted_in_source line 209
17. theorem OAI.MorseArnold.CapGluing.inserted_fixed_count line 219