OAI/Geometry/SurfaceImmersion/Atlas/OuterChartDifferential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recover the actual differential wherever the outer chart cutoff equals one on a neighborhood, including a collar beyond the primitive support.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorChartRead_comp_chart_of_outer line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorChartRead_differential_of_outer line 27