Commit 2025-07-04 16:21 eb796a2a

View on Github →

feat: contMDiffOn_iUnion_iff_of_isOpen (#26673) A function is C^n on a union of open sets iff it is continuous on each individual set. The ContinuousOn analogue of this is proven in #26672. Part of the path towards the geodesics and the Levi-Civita connection.

Estimated changes

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

added theorem ContMDiffOn.iUnion_of_isOpen

added theorem ContMDiffOn.union_of_isOpen

added theorem contMDiffOn_iUnion_iff_of_isOpen

added theorem contMDiffOn_union_iff_of_isOpen

added theorem contMDiff_of_contMDiffOn_iUnion_of_isOpen

added theorem contMDiff_of_contMDiffOn_union_of_isOpen