OAI/Geometry/SurfaceImmersion/Whitney/CompactPairC1Regularization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Regularize any compact collection of distinct pairs outside the frozen diagonal squares, while keeping the map uniformly close and unchanged up to translations near the frozen closed sets.

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