OAI/Geometry/NearbyLagrangian/CotangentProducts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Smooth cotangent pullbacks, sums and product decompositions.

  1. def OAI.NearbyLagrangian.CotangentGeometry.cotangentPullbackMap line 30
  2. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_cotangentPullbackMap line 34
  3. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentPullbackMap line 73
  4. def OAI.NearbyLagrangian.CotangentGeometry.cotangentAddMap line 97
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_cotangentAddMap line 101
  6. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentAddMap line 150
  7. def OAI.NearbyLagrangian.CotangentGeometry.cotangentLeft line 177
  8. def OAI.NearbyLagrangian.CotangentGeometry.cotangentRight line 180
  9. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentLeft_eq_pullback line 184
  10. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentRight_eq_pullback line 199
  11. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentLeft line 213
  12. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentRight line 235
  13. def OAI.NearbyLagrangian.CotangentGeometry.cotangentMerge line 277
  14. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentMerge_eq_addPullback line 283
  15. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentMerge line 302
  16. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentMerge_left_right line 338
  17. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentLeft_merge line 360
  18. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentRight_merge line 374
  19. def OAI.NearbyLagrangian.CotangentGeometry.cotangentProductDiffeomorph line 387