New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(data/set/lattice): add lemmas set.Union_subtype and set.Union_of_singleton_coe #5691
Conversation
In another zulip thread about this same lemma I suggested that instead we should add: lemma set.Union_subtype {α β : Type*} (s : set α) (f : α → set β) :
(⋃ (i : s), f i) = ⋃ (i ∈ s), f i :=
(set.bUnion_eq_Union s $ λ x _, f x).symm But maybe we should just have both. |
…r-community/mathlib into set.bUnion_of_singleton_of_coe
Eric, I added the second lemma as well! |
src/data/set/lattice.lean
Outdated
lemma set.Union_subtype {α β : Type*} (s : set α) (f : α → set β) : | ||
(⋃ (i : s), f i) = ⋃ (i ∈ s), f i := | ||
(set.bUnion_eq_Union s $ λ x _, f x).symm |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For other reviewers - is this a good simp
lemma? My feeling is yes, because we have a lot of other simp lemmas about things of the form ⋃ (i ∈ s)
when s
is some compound expression.
moved lemma bUnion_of_singleton_of_coe and renamed it to Union_of_singleton_coe
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors r+ |
…_singleton_coe (#5691) Add one simp lemma, following a suggestion on the Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/image_bUnion
Pull request successfully merged into master. Build succeeded: |
Add one simp lemma, following a suggestion on the Zulip chat:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/image_bUnion