OAI/Geometry/NearbyLagrangian/IntrinsicRealization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic realization data and compatible changes of Euclidean dimension.

  1. def OAI.NearbyLagrangian.EmbeddedRealization.sourceIntrinsicEquiv line 23
  2. lemma OAI.NearbyLagrangian.EmbeddedRealization.intrinsicGenerate_familyCriticalParam line 43
  3. theorem OAI.NearbyLagrangian.EmbeddedRealization.source_intrinsic_data line 48
  4. def OAI.NearbyLagrangian.Tubes.euclideanCast line 97
  5. lemma OAI.NearbyLagrangian.Tubes.pullback_euclideanCast_refl line 101
  6. lemma OAI.NearbyLagrangian.Tubes.smoothFamily_pullback_euclideanCast line 106
  7. lemma OAI.NearbyLagrangian.Tubes.gradient_injective_pullback_euclideanCast line 113
  8. def OAI.NearbyLagrangian.CotangentGeometry.verticalCast line 126
  9. lemma OAI.NearbyLagrangian.CotangentGeometry.verticalCast_refl line 130
  10. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_verticalCast line 133
  11. lemma OAI.NearbyLagrangian.CotangentGeometry.verticalCast_regular line 139
  12. lemma OAI.NearbyLagrangian.CotangentGeometry.verticalCast_injective line 149
  13. lemma OAI.NearbyLagrangian.CotangentGeometry.verticalCast_range line 156
  14. lemma OAI.NearbyLagrangian.CotangentGeometry.verticalCast_tail line 164
  15. lemma OAI.NearbyLagrangian.CotangentGeometry.verticalCast_reference line 171
  16. theorem OAI.NearbyLagrangian.EmbeddedRealization.exists_realization_with_intrinsic_data line 189