OAI/Geometry/SurfaceImmersion/Atlas/CoordinateRegularReplacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A supported coordinate replacement preserving differential rank preserves the exact regular locus on the original surface.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.coordinate_regular_replacement line 15