OAI/Geometry/NearbyLagrangian/TelescopeKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The ninth telescope homotopy group and stable tube kernels.

  1. def OAI.NearbyLagrangian.Tubes.telescopeBase line 17
  2. def OAI.NearbyLagrangian.Tubes.standardTelescopeClass line 21
  3. theorem OAI.NearbyLagrangian.Tubes.telescope_nullhomotopic_iff_standard line 24
  4. theorem OAI.NearbyLagrangian.Tubes.telescopeClass_eq_standard_iff line 32
  5. theorem OAI.NearbyLagrangian.Tubes.stableClassTelescopeEquiv_standard line 38
  6. abbrev OAI.NearbyLagrangian.Tubes.TelescopePi9 line 44
  7. def OAI.NearbyLagrangian.Tubes.telescopePi9ToFree line 46
  8. theorem OAI.NearbyLagrangian.Tubes.telescopePi9ToFree_surjective line 52
  9. theorem OAI.NearbyLagrangian.Tubes.telescopePi9ToFree_eq_standard_iff line 59
  10. def OAI.NearbyLagrangian.Tubes.telescopePi9ToStable line 68
  11. theorem OAI.NearbyLagrangian.Tubes.telescopePi9ToStable_surjective line 71
  12. theorem OAI.NearbyLagrangian.Tubes.telescopePi9ToStable_eq_standard_iff line 78
  13. def OAI.NearbyLagrangian.Tubes.telescopePi9NegativeClass line 85
  14. theorem OAI.NearbyLagrangian.Tubes.kernelFamilyGoal_iff_telescope_pi9_kernel line 89