OAI/Geometry/SurfaceImmersion/Atlas/FixedChartGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restricting a fixed phase chart preserves its derivative budgets. Both Jacobian denominators are bounded by the original chart's first jets.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.coordDet_abs_le_norm line 14
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.chart_jacobian_bounds line 27
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.restrict_chart_forward_jets line 46
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.restrict_chart_inverse_jets line 59