Commit 2024-02-28 09:50 e69cb643

View on Github →

feat: Unions and intersections indexed by Finset.sigma (#10851) Followup to #8964 From PFR

Estimated changes

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Fintype/Sigma.lean

modified theorem Finset.univ_sigma_univ

added theorem Set.biInter_finsetSigma_univ'

added theorem Set.biInter_finsetSigma_univ

added theorem Set.biUnion_finsetSigma_univ'

added theorem Set.biUnion_finsetSigma_univ