OAI/Geometry/SurfaceImmersion/Atlas/IntervalInteriorCutoff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compactly supported smooth interval cutoff with a full unit germ at every point of a specified smaller closed interval.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.interval_interior_cutoff line 12