OAI/Geometry/NearbyLagrangian/FlowLevels.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Flow collars, level translation and homotopy equivalences of negative sets.

  1. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.observable_lipschitz line 19
  2. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.translate_level line 29
  3. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.norm_eq line 70
  4. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.observable_lipschitz_on line 87
  5. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.translate_level_on line 97
  6. def OAI.NearbyLagrangian.ODE.CompleteFlow.levelCollarOn line 140
  7. lemma OAI.NearbyLagrangian.ODE.CompleteFlow.observable_monotone line 189
  8. def OAI.NearbyLagrangian.ODE.CompleteFlow.negativeHomotopyEquiv line 200
  9. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_sphere_level_collar line 257
  10. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_negative_open_equiv line 276