OAI/Geometry/SurfaceImmersion/Whitney/CrosscapCutoffBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A smooth compact cutoff with the derivative bound needed to remove a polynomial pair of crosscaps on a fixed rectangle.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_crosscap_cutoff line 12
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_crosscap_cutoff_scale line 38