Skip to content

[Merged by Bors] - feat: add continuousOn_iUnion#26672

Closed
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:continuousOn_iunion
Closed

[Merged by Bors] - feat: add continuousOn_iUnion#26672
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:continuousOn_iunion

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jul 3, 2025 •
edited
Loading

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.

This exposed the naming bikeshed here, which is however independent of this PR.

Open in Gitpod

@grunweg grunweg added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 3, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 3, 2025

@vlad902 Would you like to take a look at this PR?

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 3, 2025 •
edited
Loading

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

+ ContinuousOn.iUnion_of_isOpen
+ continuousOn_iUnion_iff_of_isOpen
+ continuous_of_continuousOn_iUnion_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).

This was referenced Jul 3, 2025
Closed
Draft
Closed
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jul 3, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 3, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 3, 2025
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jul 3, 2025

bors r+

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 3, 2025
@grunweg
feat: add continuousOn_iUnion (#26672)
4fb1c97 
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.
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 3, 2025

Thanks everybody for the quick review!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 3, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: add continuousOn_iUnion [Merged by Bors] - feat: add continuousOn_iUnion Jul 3, 2025
@mathlib-bors mathlib-bors bot closed this Jul 3, 2025
@grunweg grunweg deleted the continuousOn_iunion branch July 3, 2025 22:54
mathlib-bors bot pushed a commit that referenced this pull request Jul 4, 2025
@grunweg
feat: contMDiffOn_iUnion_iff_of_isOpen (#26673)
c976828 
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 bot pushed a commit that referenced this pull request Jul 4, 2025
@grunweg
feat: contMDiffOn_iUnion_iff_of_isOpen (#26673)
eb796a2 
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.
@vihdzp vihdzp mentioned this pull request Jul 5, 2025
Closed
2 tasks
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@grunweg @joelriou
feat: add continuousOn_iUnion (leanprover-community#26672)
0aa78f5 
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.
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@grunweg @joelriou
feat: contMDiffOn_iUnion_iff_of_isOpen (leanprover-community#26673)
8419fb1 
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.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@grunweg @callesonne
feat: add continuousOn_iUnion (leanprover-community#26672)
dd41615 
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.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@grunweg @callesonne
feat: contMDiffOn_iUnion_iff_of_isOpen (leanprover-community#26673)
85dbbda 
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.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@grunweg @hrmacbeth
feat: add continuousOn_iUnion (leanprover-community#26672)
897b293 
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.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@grunweg @hrmacbeth
feat: contMDiffOn_iUnion_iff_of_isOpen (leanprover-community#26673)
7b1e054 
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

+1 more reviewer

@vlad902 vlad902 vlad902 approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@grunweg @sgouezel @vlad902 @Ruben-VandeVelde