Theorem contMDiffAt_iff_of_mem_maximalAtlas

Modification history

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