OAI/Geometry/SurfaceImmersion/Whitney/DoubleLocusImmersion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The natural inclusion of the smooth double locus into the pair of surfaces has injective differential.

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