OAI/Geometry/SurfaceImmersion/Whitney/FinitePairC1Regularization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite regularization of prescribed compact pair pieces, with arbitrarily small uniform displacement and frozen translation germs.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_surface_pair_regularization_C1 line 18