OAI/Geometry/Symplectic/MorseBounds/CapTransfer.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MorseArnold.CapTransfer.AE line 15
2. abbrev OAI.MorseArnold.CapTransfer.AJ line 16
3. instance OAI.MorseArnold.CapTransfer.ambientCharts line 17
4. def OAI.MorseArnold.CapTransfer.CapTransferObligation line 21
5. lemma OAI.MorseArnold.CapTransfer.ambient_model line 55
6. lemma OAI.MorseArnold.CapTransfer.local_model line 57
7. lemma OAI.MorseArnold.CapTransfer.preserves_comp line 60
8. lemma OAI.MorseArnold.CapTransfer.local_charts line 74
9. lemma OAI.MorseArnold.CapTransfer.exterior_zero line 83
10. lemma OAI.MorseArnold.CapTransfer.exterior_inverse_neg line 86
11. def OAI.MorseArnold.CapTransfer.deltaInv line 90
12. lemma OAI.MorseArnold.CapTransfer.delta_inverse_data line 94
13. lemma OAI.MorseArnold.CapTransfer.delta_preserves line 121
14. lemma OAI.MorseArnold.CapTransfer.insert_preserves line 161
15. lemma OAI.MorseArnold.CapTransfer.cap_form line 239
16. theorem OAI.MorseArnold.CapTransfer.capTransferObligation line 305