[Merged by Bors] - feat: `contMDiffOn_iUnion_iff_of_isOpen` by grunweg · Pull Request #26673 · leanprover-community/mathlib4

grunweg · 2025-07-03T15:49:32Z

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.

github-actions · 2025-07-03T15:50:41Z

PR summary 7672327e9c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ContMDiffOn.iUnion_of_isOpen
+ ContMDiffOn.union_of_isOpen
+ contMDiffOn_iUnion_iff_of_isOpen
+ contMDiffOn_union_iff_of_isOpen
+ contMDiff_of_contMDiffOn_iUnion_of_isOpen
+ contMDiff_of_contMDiffOn_union_of_isOpen

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Ruben-VandeVelde

maintainer delegate

Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

Ruben-VandeVelde · 2025-07-03T19:13:30Z

Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

+variable {s t : Set M}
+
+/-- If a function is `C^k` on two open sets, it is also `C^n` on their union. -/
+lemma ContMDiffOn.union_of_isOpen (hf : ContMDiffOn I I' n f s) (hf' : ContMDiffOn I I' n f t)


Question for all of those: is _of_isOpen needed? Are there other true lemmas you'd confuse them with if you removed the suffix?

Good question, I'm honestly not sure.
Given that this lemma has four different cousins with the same issue (ContinuousOn, DifferentiableOn, MDifferentiableOn and ContDiffOn), I'd rather land this PR as-is, being consistent with the others. But feel free to make a PR remaining all these 8 theorems (and I can review that one quickly)!

github-actions · 2025-07-03T19:14:00Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

A function is continuous on a union of open sets iff it is continuous on each individual set. This extends the results in #22684 to arbitrary unions; the `ContMDiffOn` analogue is proven in #26673.

sgouezel · 2025-07-03T21:33:17Z

bors d+

mathlib-bors · 2025-07-03T21:33:19Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Analogue of #26673 for `ContDifferentiableOn`. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

Analogue of #26673 for `DifferentiableOn`. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

Analogue of #26673 for `MDifferentiableOn`. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

grunweg · 2025-07-04T16:02:48Z

Thanks for the reviews!
bors merge

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.

mathlib-bors · 2025-07-04T16:11:10Z

Build failed (retrying...):

CI Success

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.

mathlib-bors · 2025-07-04T16:33:04Z

Pull request successfully merged into master.

Build succeeded:

CI Success

A function is continuous on a union of open sets iff it is continuous on each individual set. This extends the results in leanprover-community#22684 to arbitrary unions; the `ContMDiffOn` analogue is proven in leanprover-community#26673.

Analogue of leanprover-community#26673 for `ContDifferentiableOn`. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

Analogue of leanprover-community#26673 for `DifferentiableOn`. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

Analogue of leanprover-community#26673 for `MDifferentiableOn`. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

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 leanprover-community#26672. Part of the path towards the geodesics and the Levi-Civita connection.