OAI/Geometry/NearbyLagrangian/CylinderFamilies.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Generating families in cylinder coordinates and their critical equivalences.

  1. def OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily line 27
  2. lemma OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_apply line 35
  3. lemma OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_at_chart line 44
  4. lemma OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_vertical line 52
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.contDiffAt_cylinderFamily line 63
  6. lemma OAI.NearbyLagrangian.CotangentGeometry.contDiffAt_cylinderFamily_one line 91
  7. lemma OAI.NearbyLagrangian.CotangentGeometry.scalar_mfderiv_open line 119
  8. lemma OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_base line 129
  9. def OAI.NearbyLagrangian.CotangentGeometry.intrinsicGenerate line 181
  10. def OAI.NearbyLagrangian.CotangentGeometry.cylinderGenerate line 184
  11. lemma OAI.NearbyLagrangian.CotangentGeometry.cylinderGenerate_at_chart line 189
  12. abbrev OAI.NearbyLagrangian.CotangentGeometry.IntrinsicCritical line 208
  13. abbrev OAI.NearbyLagrangian.CotangentGeometry.CylinderCritical line 210
  14. def OAI.NearbyLagrangian.CotangentGeometry.cylinderCriticalEquiv line 214
  15. theorem OAI.NearbyLagrangian.CotangentGeometry.cylinderGenerate_range line 237
  16. theorem OAI.NearbyLagrangian.CotangentGeometry.cylinderGenerate_injective line 260