# mathlib3documentation

data.finset.slice

# r-sets and slice #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the r-th slice of a set family and provides a way to say that a set family is made of r-sets.

An r-set is a finset of cardinality r (aka of size r). The r-th slice of a set family is the set family made of its r-sets.

## Main declarations #

• set.sized: A.sized r means that A only contains r-sets.
• finset.slice: A.slice r is the set of r-sets in A.

## Notation #

A # r is notation for A.slice r in locale finset_family.

### Families of r-sets #

def set.sized {α : Type u_1} (r : ) (A : set (finset α)) :
Prop

sized r A means that every finset in A has size r.

Equations
theorem set.sized.mono {α : Type u_1} {A B : set (finset α)} {r : } (h : A B) (hB : B) :
A
theorem set.sized_union {α : Type u_1} {A B : set (finset α)} {r : } :
(A B) A B
theorem set.sized.union {α : Type u_1} {A B : set (finset α)} {r : } :
A B (A B)

Alias of the reverse direction of set.sized_union.

@[simp]
theorem set.sized_Union {α : Type u_1} {ι : Sort u_2} {r : } {f : ι set (finset α)} :
( (i : ι), f i) (i : ι), (f i)
@[simp]
theorem set.sized_Union₂ {α : Type u_1} {ι : Sort u_2} {κ : ι Sort u_3} {r : } {f : Π (i : ι), κ i set (finset α)} :
( (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), (f i j)
@[protected]
theorem set.sized.is_antichain {α : Type u_1} {A : set (finset α)} {r : } (hA : A) :
@[protected]
theorem set.sized.subsingleton {α : Type u_1} {A : set (finset α)} (hA : A) :
theorem set.sized.subsingleton' {α : Type u_1} {A : set (finset α)} [fintype α] (hA : A) :
theorem set.sized.empty_mem_iff {α : Type u_1} {A : set (finset α)} {r : } (hA : A) :
A A = {}
theorem set.sized.univ_mem_iff {α : Type u_1} {A : set (finset α)} {r : } [fintype α] (hA : A) :
theorem set.sized_powerset_len {α : Type u_1} (s : finset α) (r : ) :
s)
theorem finset.subset_powerset_len_univ_iff {α : Type u_1} [fintype α] {𝒜 : finset (finset α)} {r : } :
theorem set.sized.subset_powerset_len_univ {α : Type u_1} [fintype α] {𝒜 : finset (finset α)} {r : } :

Alias of the reverse direction of finset.subset_powerset_len_univ_iff.

theorem set.sized.card_le {α : Type u_1} [fintype α] {𝒜 : finset (finset α)} {r : } (h𝒜 : 𝒜) :

### Slices #

def finset.slice {α : Type u_1} (𝒜 : finset (finset α)) (r : ) :

The r-th slice of a set family is the subset of its elements which have cardinality r.

Equations
theorem finset.mem_slice {α : Type u_1} {𝒜 : finset (finset α)} {A : finset α} {r : } :
A 𝒜.slice r A 𝒜 A.card = r

A is in the r-th slice of 𝒜 iff it's in 𝒜 and has cardinality r.

theorem finset.slice_subset {α : Type u_1} {𝒜 : finset (finset α)} {r : } :
𝒜.slice r 𝒜

The r-th slice of 𝒜 is a subset of 𝒜.

theorem finset.sized_slice {α : Type u_1} {𝒜 : finset (finset α)} {r : } :
(𝒜.slice r)

Everything in the r-th slice of 𝒜 has size r.

theorem finset.eq_of_mem_slice {α : Type u_1} {𝒜 : finset (finset α)} {A : finset α} {r₁ r₂ : } (h₁ : A 𝒜.slice r₁) (h₂ : A 𝒜.slice r₂) :
r₁ = r₂
theorem finset.ne_of_mem_slice {α : Type u_1} {𝒜 : finset (finset α)} {A₁ A₂ : finset α} {r₁ r₂ : } (h₁ : A₁ 𝒜.slice r₁) (h₂ : A₂ 𝒜.slice r₂) :
r₁ r₂ A₁ A₂

Elements in distinct slices must be distinct.

theorem finset.pairwise_disjoint_slice {α : Type u_1} {𝒜 : finset (finset α)} :
@[simp]
theorem finset.bUnion_slice {α : Type u_1} (𝒜 : finset (finset α)) [fintype α] [decidable_eq α] :
@[simp]
theorem finset.sum_card_slice {α : Type u_1} (𝒜 : finset (finset α)) [fintype α] :
(finset.Iic (fintype.card α)).sum (λ (r : ), (𝒜.slice r).card) = 𝒜.card