OAI/Geometry/SurfaceImmersion/Atlas/CrossPhaseExteriorControl.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exterior control in a fixed curve chart, while the analytic construction and projected normal use the current immersion's smoothing atlas.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_phase_exterior_control line 20