OAI/Geometry/SurfaceImmersion/Whitney/SurfaceCrosscapNormalForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Source and target charts putting an actual prepared surface crosscap into the standard umbrella form.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surface_crosscap_normal_form line 16