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: Unions and intersections indexed by Finset.sigma
#10851
Conversation
Followup to #8964 From PFR
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.
Thanks!
bors d+
Mathlib/Data/Fintype/Sigma.lean
Outdated
lemma Set.biUnion_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) : | ||
⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩ := by aesop | ||
|
||
lemma Set.biUnion_finsetSigma_univ' (s : Finset ι) (f : ∀ i, κ i → Set α) : |
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.
I am not a big fan of the notatiion f : ∀ i, κ i → Set α
, but I guess PiNotation
is not available here.
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.
It's available, actually, but I'm afraid using it is a lost cause. I can only find it in comments.
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Followup to #8964 From PFR
Pull request successfully merged into master. Build succeeded: |
Finset.sigma
Finset.sigma
Followup to #8964 From PFR
Followup to #8964 From PFR
Followup to #8964
From PFR