OAI/Geometry/SurfaceImmersion/Whitney/SmoothDoubleTransitions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The transition functions of the actual smooth double-locus charts have smooth local inverses and nonzero derivative.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.transition_mem_overlap line 17
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.transition_inverse line 25
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.transition_derivative_product line 30
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.transition_derivative_ne_zero line 45