Commit 2026-06-10 21:56 433572dd

View on Github →

feat: immersions are smooth (#28796) The conventional textbook definition demands that an immersion be smooth. When asking for the immersion to have local slice charts (as we do), this implies smoothness automatically.

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

Modified Mathlib/Geometry/Manifold/Immersion.lean

added theorem Manifold.IsImmersion.contMDiff

added theorem Manifold.IsImmersionAt.contMDiffAt

added theorem Manifold.IsImmersionAt.contMDiffOn

added theorem Manifold.IsImmersionAt.continuousAt

added theorem Manifold.IsImmersionAt.continuousOn

added theorem Manifold.IsImmersionAtOfComplement.contMDiffAt

added theorem Manifold.IsImmersionAtOfComplement.contMDiffOn

added theorem Manifold.IsImmersionAtOfComplement.continuousAt

added theorem Manifold.IsImmersionAtOfComplement.continuousOn

added theorem Manifold.IsImmersionAtOfComplement.mapsto_domChart_source_codChart_source

added theorem Manifold.IsImmersionOfComplement.contMDiff

Modified Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean

modified theorem Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source

added theorem Manifold.LocalPresentationAt.mapsto_domChart_source_codChart_source

Modified Mathlib/Geometry/Manifold/SmoothEmbedding.lean

added theorem Manifold.IsSmoothEmbedding.contMDiff