OAI/Geometry/SurfaceImmersion/Atlas/PhaseNormalLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pull a local normal field in the phase coordinates back to the surface. The result is smooth, unit length and normal on its actual chart domain.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseNormalLift line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseNormalLift_properties line 21