OAI/Geometry/NearbyLagrangian/TelescopeClasses.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Equivalence of stable tube classes with telescope homotopy classes.

  1. instance OAI.NearbyLagrangian.Tubes.tubeSpaceDirectedSystem line 16
  2. abbrev OAI.NearbyLagrangian.Tubes.Telescope line 23
  3. def OAI.NearbyLagrangian.Tubes.telescopeStage line 25
  4. def OAI.NearbyLagrangian.Tubes.telescopeHomotopySetoid line 30
  5. abbrev OAI.NearbyLagrangian.Tubes.TelescopeClass line 34
  6. def OAI.NearbyLagrangian.Tubes.telescopeClass line 36
  7. def OAI.NearbyLagrangian.Tubes.telescopeClassOnStage line 38
  8. theorem OAI.NearbyLagrangian.Tubes.telescopeClassOnStage_stabilize line 42
  9. def OAI.NearbyLagrangian.Tubes.stableClassToTelescope line 51
  10. theorem OAI.NearbyLagrangian.Tubes.stableClassToTelescope_apply line 55
  11. theorem OAI.NearbyLagrangian.Tubes.stableClassToTelescope_surjective line 58
  12. theorem OAI.NearbyLagrangian.Tubes.stableClassToTelescope_injective line 67
  13. def OAI.NearbyLagrangian.Tubes.stableClassTelescopeEquiv line 76
  14. theorem OAI.NearbyLagrangian.Tubes.stableClassTelescopeEquiv_apply line 80
  15. theorem OAI.NearbyLagrangian.Tubes.telescope_stage_null_iff line 85
  16. theorem OAI.NearbyLagrangian.Tubes.stablyNonNull_iff_telescope_nonnull line 97