OAI/Geometry/NearbyLagrangian/RealizationInjectivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of the realization from exact momentum coefficients.

  1. def OAI.NearbyLagrangian.EmbeddedRealization.cotangentCoefficient line 34
  2. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceGeneratingMap_coefficient line 40
  3. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceGeneratingMap_injective line 76