OAI/Geometry/NearbyLagrangian/NegativeSuspension.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Suspension equivalences for negative domains of homogeneous functions.

  1. def OAI.NearbyLagrangian.RadialTopology.negativeSphere line 18
  2. abbrev OAI.NearbyLagrangian.RadialTopology.NegativeSplit line 22
  3. def OAI.NearbyLagrangian.RadialTopology.negativeSplitProjection line 25
  4. lemma OAI.NearbyLagrangian.RadialTopology.degreeTwo_zero line 30
  5. lemma OAI.NearbyLagrangian.RadialTopology.degreeTwo_normalized line 37
  6. lemma OAI.NearbyLagrangian.RadialTopology.negativeSplit_angular_band line 48
  7. lemma OAI.NearbyLagrangian.RadialTopology.latitudeDeform_negative line 65
  8. lemma OAI.NearbyLagrangian.RadialTopology.latitudeDeform_nonpositive line 99
  9. lemma OAI.NearbyLagrangian.RadialTopology.latitudeDeform_endpoint_nonpositive line 117
  10. lemma OAI.NearbyLagrangian.RadialTopology.suspension_split_equation line 137
  11. def OAI.NearbyLagrangian.RadialTopology.suspensionSplit line 141
  12. lemma OAI.NearbyLagrangian.RadialTopology.suspensionSplit_nonpositive line 146
  13. lemma OAI.NearbyLagrangian.RadialTopology.split_mem_suspension line 159
  14. def OAI.NearbyLagrangian.RadialTopology.suspensionNegativeInclusion line 173
  15. def OAI.NearbyLagrangian.RadialTopology.negativeLatitudeDeform line 179
  16. def OAI.NearbyLagrangian.RadialTopology.suspensionLatitudeDeform line 190
  17. def OAI.NearbyLagrangian.RadialTopology.negativeSuspensionRetraction line 203
  18. def OAI.NearbyLagrangian.RadialTopology.negativeSuspensionEquiv line 216
  19. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_angularDescent line 264
  20. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.homogeneity_nonneg line 327
  21. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.smooth_negativeSuspension_equiv line 333