OAI/Geometry/NearbyLagrangian/FiberHomotopy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Fiberwise equivalences and homotopy invariance of negative fibrations.

  1. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.refl line 22
  2. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.symm line 32
  3. lemma OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.trans_over line 43
  4. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.trans line 53
  5. def OAI.NearbyLagrangian.Tubes.negativeTotalInHomeomorph line 92
  6. def OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv.ofNegativeIn line 109
  7. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_fderiv_gradient line 130
  8. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.smooth_negative_of_approx line 137
  9. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_negative_equiv line 178
  10. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.eventually_uniform_jet_close line 206
  11. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.eventually_negative_equiv line 246
  12. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.negative_equiv_connected line 311
  13. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.negative_equiv_of_homotopic line 336
  14. theorem OAI.NearbyLagrangian.Tubes.exists_smooth_tube line 362
  15. theorem OAI.NearbyLagrangian.Tubes.negative_equiv_tube_of_homotopic line 381
  16. theorem OAI.NearbyLagrangian.Tubes.NegativeTrivial.of_homotopic line 390
  17. theorem OAI.NearbyLagrangian.Tubes.StableNegativeTrivial.of_homotopic line 397