OAI/Topology/Homotopy/RayTelescope.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Sequential ray telescopes, finite-stage representatives and path connectedness.

  1. abbrev OAI.NearbyLagrangian.RayTelescope.Raw line 16
  2. inductive OAI.NearbyLagrangian.RayTelescope.Glue line 18
  3. abbrev OAI.NearbyLagrangian.RayTelescope.Space line 23
  4. def OAI.NearbyLagrangian.RayTelescope.rawHeight line 25
  5. def OAI.NearbyLagrangian.RayTelescope.height line 28
  6. theorem OAI.NearbyLagrangian.RayTelescope.height_quot line 32
  7. def OAI.NearbyLagrangian.RayTelescope.bottomTime line 34
  8. def OAI.NearbyLagrangian.RayTelescope.stage line 36
  9. theorem OAI.NearbyLagrangian.RayTelescope.height_stage line 42
  10. def OAI.NearbyLagrangian.RayTelescope.rawCollapse line 47
  11. lemma OAI.NearbyLagrangian.RayTelescope.stage_le_of_height_lt line 56
  12. lemma OAI.NearbyLagrangian.RayTelescope.collapse_compatible line 61
  13. abbrev OAI.NearbyLagrangian.RayTelescope.Trunc line 84
  14. def OAI.NearbyLagrangian.RayTelescope.representative line 86
  15. theorem OAI.NearbyLagrangian.RayTelescope.representative_mk line 89
  16. def OAI.NearbyLagrangian.RayTelescope.retract line 92
  17. theorem OAI.NearbyLagrangian.RayTelescope.retract_quot line 113
  18. theorem OAI.NearbyLagrangian.RayTelescope.retract_stage line 122
  19. def OAI.NearbyLagrangian.RayTelescope.raiseTime line 144
  20. lemma OAI.NearbyLagrangian.RayTelescope.le_raiseTime line 146
  21. theorem OAI.NearbyLagrangian.RayTelescope.raiseTime_zero line 150
  22. theorem OAI.NearbyLagrangian.RayTelescope.raiseTime_one line 151
  23. def OAI.NearbyLagrangian.RayTelescope.cylinderRaise line 153
  24. def OAI.NearbyLagrangian.RayTelescope.rawRaise line 163
  25. def OAI.NearbyLagrangian.RayTelescope.raiseFamily line 167
  26. theorem OAI.NearbyLagrangian.RayTelescope.raiseFamily_apply line 176
  27. def OAI.NearbyLagrangian.RayTelescope.raised line 180
  28. def OAI.NearbyLagrangian.RayTelescope.raiseHomotopy line 184
  29. theorem OAI.NearbyLagrangian.RayTelescope.height_raised line 195
  30. theorem OAI.NearbyLagrangian.RayTelescope.raised_eq_stage_retract line 203
  31. theorem OAI.NearbyLagrangian.RayTelescope.exists_height_bound line 233
  32. def OAI.NearbyLagrangian.RayTelescope.finiteMap line 242
  33. def OAI.NearbyLagrangian.RayTelescope.finiteHomotopy line 245
  34. theorem OAI.NearbyLagrangian.RayTelescope.exists_finite_representative line 252
  35. theorem OAI.NearbyLagrangian.RayTelescope.finiteMap_stage line 258
  36. theorem OAI.NearbyLagrangian.RayTelescope.stage_stabilize_homotopic line 264
  37. def OAI.NearbyLagrangian.RayTelescope.finiteStageHomotopy line 276
  38. theorem OAI.NearbyLagrangian.RayTelescope.stage_homotopic_iff line 300
  39. theorem OAI.NearbyLagrangian.RayTelescope.stage_nullhomotopic_iff line 318
  40. theorem OAI.NearbyLagrangian.RayTelescope.joined_base line 366
  41. instance OAI.NearbyLagrangian.RayTelescope.pathConnected line 374