Theorem ContMDiffAt.iff_comp_isImmersionAtOfComplement

Modification history

2026-07-11 11:20
Mathlib/Geometry/Manifold/Immersion.lean
feat: a map is smooth iff its post-composition with an immersion is (#28865) …
Added ContMDiffAt.iff_comp_isImmersionAtOfComplementView on Github →