OAI/Geometry/SurfaceImmersion/Atlas/LocalGenericAtlasPhases.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Phase selection on compact portions of local boundary arcs. Smooth extension supplies the global parameter argument without imposing global chart-domain assumptions on an arc.

  1. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_generic_atlas_phases_on line 18