Theorem contMDiffOn_extend

Modification history

2026-06-30 12:29

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

chore: namespace `contMDiffAt_extend` and friends under `OpenPartialH… (#41174) …

Deleted contMDiffOn_extend View on Github →

2026-03-19 14:41

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

feat: smoothness on a set can be checked in extended charts (#36816) …

Added contMDiffOn_extend View on Github →