Commit 2023-01-29 23:22 d517d821

View on Github →

feat: Port Data.Finset.Slice (#1928)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Slice.lean

added theorem Finset.Set.Sized.card_le

added theorem Finset.bunionᵢ_slice

added theorem Finset.eq_of_mem_slice

added theorem Finset.mem_slice

added theorem Finset.ne_of_mem_slice

added theorem Finset.pairwiseDisjoint_slice

added theorem Finset.sized_slice

added def Finset.slice

added theorem Finset.slice_subset

added theorem Finset.subset_powersetLen_univ_iff

added theorem Finset.sum_card_slice

added theorem Set.Sized.empty_mem_iff

added theorem Set.Sized.mono

added theorem Set.Sized.subsingleton'

added theorem Set.Sized.univ_mem_iff

added def Set.Sized

added theorem Set.sized_powersetLen

added theorem Set.sized_union

added theorem Set.sized_unionᵢ

added theorem Set.sized_unionᵢ₂