OAI/Geometry/SurfaceImmersion/Whitney/CrosscapAxisFinishGerm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The terminal exterior germ can likewise be made an exact kernel-axis germ while preserving the closed trace and the initial germ.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_axis_finish_germ line 15