OAI/Geometry/NearbyLagrangian/ProductSymplectic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Preservation of Liouville and symplectic forms by cotangent products.

  1. lemma OAI.NearbyLagrangian.CotangentGeometry.liouville_apply_mfderiv_general line 24
  2. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentMerge_liouville line 50
  3. lemma OAI.NearbyLagrangian.chartInverse_mfderiv line 94
  4. lemma OAI.NearbyLagrangian.comp_chartInverse_mfderiv line 101
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentMerge_pullback_liouville line 134
  6. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentMerge_symplectic line 156