OAI/Geometry/SurfaceImmersion/Whitney/ActualRuledRectangle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single explicit rectangular ruled region in the supported surface replacement, with retained actual coordinate and crosscap jets.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ActualRuledRectangle line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapCoordinateStrip.exists_actual_ruled_rectangle line 40