OAI/Geometry/SurfaceImmersion/Whitney/SurfacePairLocalRegularization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth scalar separator regularizes a neighborhood of one ordered pair by arbitrarily small translations. It is locally constant near a prescribed finite set, so those first jets are retained.

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