OAI/Geometry/NearbyLagrangian/Immersions.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Local split-derivative immersions and compact smooth embeddings.

  1. theorem OAI.NearbyLagrangian.LocalGeometry.exists_smooth_local_inverse_on line 17
  2. theorem OAI.NearbyLagrangian.LocalGeometry.isImmersionAt_of_split_derivative_on line 49
  3. theorem OAI.NearbyLagrangian.LocalGeometry.exists_split_linear_equiv line 109
  4. theorem OAI.NearbyLagrangian.LocalGeometry.isImmersionAt_of_injective_derivative_on line 130
  5. theorem OAI.NearbyLagrangian.LocalGeometry.trans_mem_maximalAtlas line 149
  6. theorem OAI.NearbyLagrangian.LocalGeometry.isImmersionAt_of_chart line 162
  7. theorem OAI.NearbyLagrangian.LocalGeometry.manifold_isImmersionAt_of_injective_mfderiv line 185
  8. theorem OAI.NearbyLagrangian.LocalGeometry.manifold_isImmersion_of_injective_mfderiv line 220
  9. theorem OAI.NearbyLagrangian.LocalGeometry.isSmoothEmbedding_of_compact_injective_mfderiv line 230
  10. theorem OAI.NearbyLagrangian.CotangentGeometry.bundleTotalSpace_t2Space line 244
  11. lemma OAI.NearbyLagrangian.Generating.vertical_eq_partial line 268
  12. lemma OAI.NearbyLagrangian.Generating.momentum_eq_partial line 276