OAI/Geometry/SurfaceImmersion/Atlas/PhaseChartNormalField.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A normal vector in the nonlinear phase coordinates is normal to the actual immersion on the corresponding atlas support.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_chart_normal_at_weight line 20
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_chart_normal_of_outer line 63