OAI/Geometry/NearbyLagrangian/SuspensionEquivalence.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Fiberwise suspension equivalences and spherical quotient coordinates.

  1. def OAI.NearbyLagrangian.FiberCone.Contraction.suspensionEquiv line 18
  2. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.suspension line 43
  3. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.ofHomeomorph line 74
  4. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.latitude line 108
  5. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.latitude_range line 109
  6. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.latitude_sq_le line 114
  7. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.latitude_injective line 117
  8. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.latitude_zero line 122
  9. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.latitude_one line 123
  10. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.equatorialRadius line 125
  11. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.equatorialRadius_nonneg line 126
  12. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.equatorialRadius_sq line 127
  13. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.equatorialRadius_zero line 129
  14. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.equatorialRadius_one line 130
  15. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.equatorialRadius_pos line 131
  16. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.continuous_latitude line 138
  17. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.continuous_equatorialRadius line 140
  18. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.southPole line 143
  19. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.northPole line 146
  20. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.sphereMeridian_mem line 151
  21. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.sphereMeridian line 169
  22. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.sphereMeridian_zero line 176
  23. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.sphereMeridian_one line 180
  24. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionMap line 185
  25. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionMap_over line 189
  26. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.meridian_eq_of_sphereMeridian_eq line 209
  27. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.south_eq_of_quotientSuspensionMap_eq line 240
  28. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.north_eq_of_quotientSuspensionMap_eq line 261
  29. theorem OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionMap_injective line 282
  30. theorem OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionMap_surjective line 294
  31. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionEquiv line 330
  32. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionHomeomorph line 334
  33. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.quotientSuspensionHomeomorph_over line 341