OAI/Geometry/SurfaceImmersion/Atlas/SurfaceChartRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every smooth surface map has a globally smooth Euclidean representative on an actual smaller neighborhood of any chosen point.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surface_chart_representative line 16