OAI/Geometry/SurfaceImmersion/Atlas/ThinPairCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Model fillings can be made arbitrarily thin around the connecting interval.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.thin_pair_coordinates line 12