OAI/Topology/Homotopy/ConeHomotopy.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Right suspension homotopies and suspension of maps and homotopies.

  1. def OAI.NearbyLagrangian.FiberCone.sweepBase line 17
  2. def OAI.NearbyLagrangian.FiberCone.sweepRay line 19
  3. def OAI.NearbyLagrangian.FiberCone.sweepApex line 25
  4. lemma OAI.NearbyLagrangian.FiberCone.sweepRay_bottom line 27
  5. lemma OAI.NearbyLagrangian.FiberCone.sweepRay_top line 33
  6. def OAI.NearbyLagrangian.FiberCone.sweep line 38
  7. lemma OAI.NearbyLagrangian.FiberCone.sweep_base line 42
  8. lemma OAI.NearbyLagrangian.FiberCone.sweep_ray line 44
  9. lemma OAI.NearbyLagrangian.FiberCone.sweep_apex line 46
  10. lemma OAI.NearbyLagrangian.FiberCone.sweep_zero line 49
  11. lemma OAI.NearbyLagrangian.FiberCone.sweep_one line 58
  12. lemma OAI.NearbyLagrangian.FiberCone.sweep_over line 67
  13. def OAI.NearbyLagrangian.FiberCone.Contraction.rightRay line 77
  14. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightRay_bottom line 86
  15. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightRay_top line 90
  16. def OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation line 96
  17. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation_south line 100
  18. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation_meridian line 102
  19. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation_north line 104
  20. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation_zero line 107
  21. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation_one line 117
  22. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightDeformation_over line 128
  23. def OAI.NearbyLagrangian.FiberCone.Contraction.rightHomotopy line 140
  24. lemma OAI.NearbyLagrangian.FiberCone.Contraction.rightHomotopy_over line 146
  25. lemma OAI.NearbyLagrangian.FiberCone.suspMap_id line 164
  26. lemma OAI.NearbyLagrangian.FiberCone.suspMap_comp line 172
  27. def OAI.NearbyLagrangian.FiberCone.suspHomotopyRay line 186
  28. lemma OAI.NearbyLagrangian.FiberCone.suspHomotopyRay_bottom line 192
  29. lemma OAI.NearbyLagrangian.FiberCone.suspHomotopyRay_top line 198
  30. def OAI.NearbyLagrangian.FiberCone.suspHomotopy line 203
  31. lemma OAI.NearbyLagrangian.FiberCone.suspHomotopy_over line 223