[Merged by Bors] - feat(data/finset/basic): disj_Union #16421
Conversation
eric-wieser
added
awaiting-review
eric-wieser
added
awaiting-CI
There was a problem hiding this comment.
I fully agree on principle, but I should at least mention the reason I didn't introduce this myself:
finpartition is basically a bundling of this, so I was trying to find ways to make it practical to use without a new definition.
I now doubt this is achievable, so this PR is probably the right way forward.
| It is the same as `s.bUnion f`, but it does not require decidable equality on the type. The | ||
| hypothesis ensures that the sets are disjoint. -/ | ||
| def disj_Union (s : finset α) (t : α → finset β) | ||
| (hf : (s : set α).pairwise $ λ a b, ∀ x, x ∈ t a → x ∉ t b) : finset β := |
There was a problem hiding this comment.
Once #16434 has gone through, you could use the following, right?
| (hf : (s : set α).pairwise $ λ a b, ∀ x, x ∈ t a → x ∉ t b) : finset β := | |
| (hf : (s : set α).pairwise_disjoint t) : finset β := |
That sounds desirable, so maybe we should make them dependent.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors merge |
`finset.disj_Union` is to `finset.bUnion` as: * `finset.disj_union` is to `finset.union` * `finset.cons` is to `insert` * `finset.map` is to `finset.image` Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
This PR was included in a batch that was canceled, it will be automatically retried |
`finset.disj_Union` is to `finset.bUnion` as: * `finset.disj_union` is to `finset.union` * `finset.cons` is to `insert` * `finset.map` is to `finset.image` Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
Build failed (retrying...): |
`finset.disj_Union` is to `finset.bUnion` as: * `finset.disj_union` is to `finset.union` * `finset.cons` is to `insert` * `finset.map` is to `finset.image` Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
finset.disj_Unionis tofinset.bUnionas:finset.disj_unionis tofinset.unionfinset.consis toinsertfinset.mapis tofinset.image