OAI/Geometry/Symplectic/MorseBounds/CapProduct.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MorseArnold.CapProduct.PlaneFour line 14
  2. abbrev OAI.MorseArnold.CapProduct.SphereFour line 15
  3. abbrev OAI.MorseArnold.CapProduct.Choices line 16
  4. abbrev OAI.MorseArnold.CapProduct.SP line 17
  5. abbrev OAI.MorseArnold.CapProduct.PP line 18
  6. def OAI.MorseArnold.CapProduct.disk line 20
  7. lemma OAI.MorseArnold.CapProduct.disk_open line 21
  8. def OAI.MorseArnold.CapProduct.bigChart line 24
  9. def OAI.MorseArnold.CapProduct.oneChart line 27
  10. def OAI.MorseArnold.CapProduct.fourChart line 30
  11. def OAI.MorseArnold.CapProduct.box line 35
  12. def OAI.MorseArnold.CapProduct.fourFlow line 36
  13. def OAI.MorseArnold.CapProduct.quadFlow line 39
  14. lemma OAI.MorseArnold.CapProduct.bigChart_target line 43
  15. lemma OAI.MorseArnold.CapProduct.oneChart_source line 47
  16. lemma OAI.MorseArnold.CapProduct.oneChart_target line 50
  17. theorem OAI.MorseArnold.CapProduct.four_chart_target line 60
  18. lemma OAI.MorseArnold.CapProduct.bigChart_smooth line 68
  19. lemma OAI.MorseArnold.CapProduct.oneChart_smooth line 78
  20. theorem OAI.MorseArnold.CapProduct.four_chart_smooth line 84
  21. lemma OAI.MorseArnold.CapProduct.one_cap_disjoint line 100
  22. lemma OAI.MorseArnold.CapProduct.one_overlap_eq line 109
  23. theorem OAI.MorseArnold.CapProduct.four_caps_disjoint line 118
  24. lemma OAI.MorseArnold.CapProduct.one_endpoint line 132
  25. theorem OAI.MorseArnold.CapProduct.four_endpoint line 140
  26. lemma OAI.MorseArnold.CapProduct.pole_in_cap line 151
  27. theorem OAI.MorseArnold.CapProduct.exterior_not_fixed line 168
  28. lemma OAI.MorseArnold.CapProduct.one_preserves line 187
  29. theorem OAI.MorseArnold.CapProduct.four_preserves line 208
  30. lemma OAI.MorseArnold.CapProduct.smooth_time_pair line 217
  31. lemma OAI.MorseArnold.CapProduct.pairFlow_smooth line 232
  32. theorem OAI.MorseArnold.CapProduct.four_flow_smooth line 238