OAI/Geometry/SurfaceImmersion/Whitney/NarrowedRulingBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The supported ruled correction tends to zero globally in C1.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.narrowedRuling_C1_bound line 13
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.narrowedRuling_small line 43