Theorem OpenPartialHomeomorph.contMDiffAt_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.contMDiffAt_extendView on Github →