OAI/Geometry/NearbyLagrangian/StandardNegative.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Negative domains of standard quadratic tubes and their sphere homotopy types.

  1. abbrev OAI.NearbyLagrangian.Tubes.UnitSphere line 14
  2. abbrev OAI.NearbyLagrangian.Tubes.UnitBall line 15
  3. def OAI.NearbyLagrangian.Tubes.NegativeDomain line 17
  4. instance OAI.NearbyLagrangian.Tubes.(instance at line 20) line 20
  5. theorem OAI.NearbyLagrangian.Tubes.unitSphere_norm line 24
  6. theorem OAI.NearbyLagrangian.Tubes.unitSphere_ne_zero line 27
  7. abbrev OAI.NearbyLagrangian.Tubes.StandardNegative line 32
  8. def OAI.NearbyLagrangian.Tubes.negativeCoordinates line 34
  9. theorem OAI.NearbyLagrangian.Tubes.negative_second_le_first line 39
  10. theorem OAI.NearbyLagrangian.Tubes.negative_first_ne_zero line 49
  11. def OAI.NearbyLagrangian.Tubes.standardNegativeToProduct line 62
  12. def OAI.NearbyLagrangian.Tubes.standardNegativeRaw line 79
  13. theorem OAI.NearbyLagrangian.Tubes.standardNegativeRaw_ne_zero line 85
  14. def OAI.NearbyLagrangian.Tubes.productToStandardNegative line 91
  15. theorem OAI.NearbyLagrangian.Tubes.negativeCoordinates_productToStandardNegative line 109
  16. theorem OAI.NearbyLagrangian.Tubes.standardNegativeToProduct_productToStandardNegative line 119
  17. theorem OAI.NearbyLagrangian.Tubes.productToStandardNegative_standardNegativeToProduct line 141
  18. def OAI.NearbyLagrangian.Tubes.standardNegativeHomeomorph line 160
  19. def OAI.NearbyLagrangian.Tubes.unitBallContract line 168
  20. def OAI.NearbyLagrangian.Tubes.standardNegativeSphereEquiv line 179
  21. def OAI.NearbyLagrangian.Tubes.constantNegativeTotalHomeomorph line 203
  22. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.ofProduct line 216
  23. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.precomposeHomeomorph line 243
  24. theorem OAI.NearbyLagrangian.Tubes.negativeTrivial_standard line 269
  25. theorem OAI.NearbyLagrangian.Tubes.stableNegativeTrivial_standard line 273