OAI/Geometry/SurfaceImmersion/Whitney/GlobalCleanPairRegularization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global regularization with a fixed injectivity cover and frozen crosscap neighborhoods. No distinct double pair is left uncontrolled.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.global_clean_pair_regularization_with_cover line 18