OAI/Geometry/SurfaceImmersion/Atlas/PreferredNormalPhasePullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Pull the actual global preferred normal into the primitive's phase coordinates, preserving smoothness, unit length and orthogonality.

  1. lemma OAI.ClosedSurfaceR4.PreferredNormal.pullback_normal_at line 19
  2. def OAI.ClosedSurfaceR4.PreferredNormal.inPhase line 37
  3. lemma OAI.ClosedSurfaceR4.PreferredNormal.inPhase_smooth line 40
  4. lemma OAI.ClosedSurfaceR4.PreferredNormal.inPhase_unit line 47
  5. lemma OAI.ClosedSurfaceR4.PreferredNormal.inPhase_normal line 53
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.preferred_normal_in_phase line 65