[Merged by Bors] - feat(Topology): add ContinuousOn union API lemmas#22684
[Merged by Bors] - feat(Topology): add ContinuousOn union API lemmas#22684
ContinuousOn union API lemmas#22684Conversation
PR summary 5ecc602a70Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Add two lemmas to allow going from continuity of a union to continuity on the individual sets, and continuity on two open sets to continuity on their union. Note that there is already one lemma for continuity of two closed sets.
1739c0f to
45686c0
Compare
|
Done, thanks for the feedback |
grunweg
left a comment
There was a problem hiding this comment.
Thanks: this PR looks basically good to me - except for a naming question I'm not sure about.
Mathlib/Topology/ContinuousOn.lean
Outdated
| fun h ↦ ContinuousOn.union_of_isClosed hs ht h.1 h.2⟩ | ||
|
|
||
| /-- If a function is continuous on two open sets, it is also continuous on their union. -/ | ||
| theorem ContinuousOn.union_of_isOpen (hs : IsOpen s) (ht : IsOpen t) {f : α → β} |
There was a problem hiding this comment.
Should this be called continuousOn_union_of_isOpen? @YaelDillies as you're a local naming expert
There was a problem hiding this comment.
(Note that there is also an iff version below, so perhaps a slightly different name is needed.)
There was a problem hiding this comment.
If the current name is fine, the ContinuousOn hypothesis should come first.
|
This looks mostly good to me now - thanks. Regarding the question Michael raised earlier, my suggestion would be to rename |
updated names / param ordering |
grunweg
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
bors r+ |
Add lemmas to allow going from continuity on two open sets to continuity on their union. Note that there is already an existing lemma for continuity on the union of two closed sets. Co-authored-by: Vlad Tsyrklevich <vlad@tsyrklevich.net>
|
Pull request successfully merged into master. Build succeeded: |
ContinuousOn union API lemmasContinuousOn union API lemmas
Add lemmas to allow going from continuity on two open sets to continuity on their union. Note that there is already an existing lemma for continuity on the union of two closed sets. Co-authored-by: Vlad Tsyrklevich <vlad@tsyrklevich.net>
…nity#22684) Add lemmas to allow going from continuity on two open sets to continuity on their union. Note that there is already an existing lemma for continuity on the union of two closed sets. Co-authored-by: Vlad Tsyrklevich <vlad@tsyrklevich.net>
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.
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.
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.
Add lemmas to allow going from continuity on two open sets to continuity on their union. Note that there is already an existing lemma for continuity on the union of two closed sets.