OAI/Geometry/NearbyLagrangian/PositiveSquares.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Retraction and homotopy equivalence after adding a positive square.

  1. abbrev OAI.NearbyLagrangian.RadialTopology.PositiveSplit line 17
  2. def OAI.NearbyLagrangian.RadialTopology.positiveSplitProjection line 20
  3. lemma OAI.NearbyLagrangian.RadialTopology.positiveOrigin_ne line 25
  4. def OAI.NearbyLagrangian.RadialTopology.positiveInclusion line 35
  5. def OAI.NearbyLagrangian.RadialTopology.positiveRetraction line 44
  6. lemma OAI.NearbyLagrangian.RadialTopology.positiveRetraction_inclusion line 61
  7. def OAI.NearbyLagrangian.RadialTopology.positiveDenom line 69
  8. lemma OAI.NearbyLagrangian.RadialTopology.positiveDenom_pos line 73
  9. lemma OAI.NearbyLagrangian.RadialTopology.positiveDenom_sq line 81
  10. lemma OAI.NearbyLagrangian.RadialTopology.continuous_positiveDenom line 86
  11. lemma OAI.NearbyLagrangian.RadialTopology.positiveDenom_zero line 94
  12. lemma OAI.NearbyLagrangian.RadialTopology.positiveDenom_one line 98
  13. lemma OAI.NearbyLagrangian.RadialTopology.positiveDeform_sphere line 102
  14. lemma OAI.NearbyLagrangian.RadialTopology.positiveDeform_nonpositive line 114
  15. def OAI.NearbyLagrangian.RadialTopology.positiveDeform line 130
  16. lemma OAI.NearbyLagrangian.RadialTopology.positiveDeform_zero line 143
  17. lemma OAI.NearbyLagrangian.RadialTopology.positiveDeform_one line 153
  18. def OAI.NearbyLagrangian.RadialTopology.positiveSquareEquiv line 164