Commit 2022-01-04 13:36 8bd20598

View on Github →

feat(data/finset/slice): r-sets and slice (#10685) Two simple nonetheless useful definitions about set families. A family of r-sets is a set of finsets of cardinality r. The slice of a set family is its subset of r-sets.

Estimated changes

Modified src/combinatorics/set_family/shadow.lean

Created src/data/finset/slice.lean

added theorem finset.eq_of_mem_slice

added theorem finset.mem_slice

added theorem finset.ne_of_mem_slice

added theorem finset.pairwise_disjoint_slice

added theorem finset.sized_slice

added def finset.slice

added theorem finset.slice_subset

added theorem finset.subset_powerset_len_univ_iff

added theorem set.sized.card_le

added theorem set.sized.mono

added def set.sized

added theorem set.sized_union

Modified src/data/fintype/basic.lean

added theorem finset.mem_powerset_len_univ_iff