Commit 2026-03-19 14:41 0401a172

View on Github →

feat: smoothness on a set can be checked in extended charts (#36816) Cherry-picked from #28796: it might not get used in the eventual PR there, but this lemma seems useful independently. (In any case, I would like to use these lemmas now, and there is no reason to wait until I have filled in the missing API for #28796.)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Comp.lean

added theorem ContDiffWithinAt.fst

added theorem ContDiffWithinAt.snd

added theorem contDiffAt_prod_iff

added theorem contDiffOn_prod_iff

added theorem contDiffWithinAt_prod_iff

added theorem contDiff_prod_iff

Modified Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

added theorem OpenPartialHomeomorph.contMDiffOn_writtenInExtend_iff

added theorem OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff

added theorem contMDiffOn_extend

Modified Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

added theorem OpenPartialHomeomorph.extend_target_eq_image_source