mathlib3 documentation

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 #

Notation #

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

Families of r-sets #

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

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

Equations
source
theorem set.sized.mono {α : Type u_1} {A B : set (finset α)} {r : ℕ} (h : A ⊆ B) (hB : set.sized r B) :
set.sized r A
source
theorem set.sized_union {α : Type u_1} {A B : set (finset α)} {r : ℕ} :
set.sized r (A ∪ B) ↔ set.sized r A ∧ set.sized r B
source
theorem set.sized.union {α : Type u_1} {A B : set (finset α)} {r : ℕ} :
set.sized r A ∧ set.sized r B → set.sized r (A ∪ B)

Alias of the reverse direction of set.sized_union.

source
@[simp]
theorem set.sized_Union {α : Type u_1} {ι : Sort u_2} {r : ℕ} {f : ι → set (finset α)} :
set.sized r (⋃ (i : ι), f i) ↔ ∀ (i : ι), set.sized r (f i)
source
@[simp]
theorem set.sized_Union₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {r : ℕ} {f : Π (i : ι), κ i → set (finset α)} :
set.sized r (⋃ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), set.sized r (f i j)
source
@[protected]
theorem set.sized.is_antichain {α : Type u_1} {A : set (finset α)} {r : ℕ} (hA : set.sized r A) :
is_antichain has_subset.subset A
source
@[protected]
theorem set.sized.subsingleton {α : Type u_1} {A : set (finset α)} (hA : set.sized 0 A) :
A.subsingleton
source
theorem set.sized.subsingleton' {α : Type u_1} {A : set (finset α)} [fintype α] (hA : set.sized (fintype.card α) A) :
A.subsingleton
source
theorem set.sized.empty_mem_iff {α : Type u_1} {A : set (finset α)} {r : ℕ} (hA : set.sized r A) :
∅ ∈ A ↔ A = {∅}
source
theorem set.sized.univ_mem_iff {α : Type u_1} {A : set (finset α)} {r : ℕ} [fintype α] (hA : set.sized r A) :
finset.univ ∈ A ↔ A = {finset.univ}
source
theorem set.sized_powerset_len {α : Type u_1} (s : finset α) (r : ℕ) :
set.sized r ↑(finset.powerset_len r s)
source
theorem finset.subset_powerset_len_univ_iff {α : Type u_1} [fintype α] {𝒜 : finset (finset α)} {r : ℕ} :
𝒜 ⊆ finset.powerset_len r finset.univ ↔ set.sized r ↑𝒜
source
theorem set.sized.subset_powerset_len_univ {α : Type u_1} [fintype α] {𝒜 : finset (finset α)} {r : ℕ} :
set.sized r ↑𝒜 → 𝒜 ⊆ finset.powerset_len r finset.univ

Alias of the reverse direction of finset.subset_powerset_len_univ_iff.

source
theorem set.sized.card_le {α : Type u_1} [fintype α] {𝒜 : finset (finset α)} {r : ℕ} (h𝒜 : set.sized r ↑𝒜) :
𝒜.card ≤ (fintype.card α).choose r

Slices #

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

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

Equations
source
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.

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

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

source
theorem finset.sized_slice {α : Type u_1} {𝒜 : finset (finset α)} {r : ℕ} :
set.sized r ↑(𝒜.slice r)

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

source
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₂
source
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.

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