OAI/Geometry/SurfaceImmersion/Whitney/DoubleLocusAugmentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A three-dimensional submersion on the four-dimensional pair chart admits one additional linear coordinate with invertible derivative.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.double_locus_linear_augmentation line 14