OAI/Geometry/NearbyLagrangian/SphereSuspension.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Continuous radial lifts and fiberwise suspension of sphere families.

  1. def OAI.NearbyLagrangian.RadialTopology.radialLift line 18
  2. lemma OAI.NearbyLagrangian.RadialTopology.radialLift_of_zero line 22
  3. lemma OAI.NearbyLagrangian.RadialTopology.radialLift_of_ne_zero line 26
  4. lemma OAI.NearbyLagrangian.RadialTopology.norm_radialLift_le line 30
  5. theorem OAI.NearbyLagrangian.RadialTopology.continuous_radialLift line 38
  6. lemma OAI.NearbyLagrangian.RadialTopology.norm_radialLift line 62
  7. structure OAI.NearbyLagrangian.RadialTopology.SphereFamily line 74
  8. abbrev OAI.NearbyLagrangian.RadialTopology.SphereFamily.Total line 83
  9. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.projection line 85
  10. abbrev OAI.NearbyLagrangian.RadialTopology.SphereFamily.Suspension line 88
  11. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspensionProjection line 93
  12. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.direction line 96
  13. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.continuous_direction line 101
  14. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendedVector line 108
  15. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.norm_suspendedVector line 113
  16. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.continuous_suspendedVector line 119
  17. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendedVector_zero line 134
  18. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendedVector_nonzero line 140
  19. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspend line 148
  20. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspend_base line 170
  21. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspend_latitude line 174
  22. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap line 189
  23. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_base line 196
  24. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_latitude line 200
  25. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.norm_suspendMap_vector line 204
  26. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_vector_zero line 208
  27. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_vector_nonzero line 213
  28. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_direction line 219
  29. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_id line 233
  30. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendMap_comp line 248
  31. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendHomotopy line 273
  32. lemma OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendHomotopy_base line 305
  33. def OAI.NearbyLagrangian.RadialTopology.SphereFamily.suspendFiberwise line 320