OAI/Geometry/SurfaceImmersion/Whitney/CornerParameterOrientation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The explicit corner parameters run forward along the original path at each joining endpoint.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_homeomorph_inverse_deriv_ne line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_homeomorph_inverse_deriv_pos line 25
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_homeomorph_inverse_deriv_neg line 35
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.returning_left_parameter_deriv_pos line 48
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.returning_right_parameter_deriv_pos line 62
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.advancing_parameter_deriv_pos line 76