Theorem ContMDiff.iff_comp_isImmersionOfComplement

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 ContMDiff.iff_comp_isImmersionOfComplementView on Github →