Theorem OpenPartialHomeomorph.contMDiffOn_extend

Modification history

2026-06-30 12:29
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
chore: namespace `contMDiffAt_extend` and friends under `OpenPartialH… (#41174) …
Added OpenPartialHomeomorph.contMDiffOn_extendView on Github →