r-sets and slice

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

• Set.Sized r A = ∀ ⦃x : Finset α⦄, x ∈ A → x.card = r

theorem Set.Sized.mono {α : Type u_1} {A : Set (Finset α)} {B : Set (Finset α)} {r : ℕ} (h : A ⊆ B) (hB : Set.Sized r B) : Set.Sized r A

@[simp]

theorem Set.sized_empty {α : Type u_1} {r : ℕ} : Set.Sized r ∅

@[simp]

theorem Set.sized_singleton {α : Type u_1} {s : Finset α} {r : ℕ} : Set.Sized r {s} ↔ s.card = r

theorem Set.sized_union {α : Type u_1} {A : Set (Finset α)} {B : Set (Finset α)} {r : ℕ} : Set.Sized r (A ∪ B) ↔ Set.Sized r A ∧ Set.Sized r B

theorem Set.sized.union {α : Type u_1} {A : Set (Finset α)} {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.

@[simp]

theorem Set.sized_iUnion {α : Type u_1} {ι : Sort u_2} {r : ℕ} {f : ι → Set (Finset α)} : Set.Sized r (⋃ (i : ι), f i) ↔ ∀ (i : ι), Set.Sized r (f i)

theorem Set.sized_iUnion₂ {α : 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)

theorem Set.Sized.isAntichain {α : Type u_1} {A : Set (Finset α)} {r : ℕ} (hA : Set.Sized r A) : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) A

theorem Set.Sized.subsingleton {α : Type u_1} {A : Set (Finset α)} (hA : Set.Sized 0 A) : A.Subsingleton

theorem Set.Sized.subsingleton' {α : Type u_1} {A : Set (Finset α)} [Fintype α] (hA : Set.Sized (Fintype.card α) A) : A.Subsingleton

theorem Set.Sized.empty_mem_iff {α : Type u_1} {A : Set (Finset α)} {r : ℕ} (hA : Set.Sized r A) : ∅ ∈ A ↔ A = {∅}

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}

theorem Set.sized_powersetCard {α : Type u_1} (s : Finset α) (r : ℕ) : Set.Sized r ↑(Finset.powersetCard r s)

theorem Finset.subset_powersetCard_univ_iff {α : Type u_1} [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} : 𝒜 ⊆ Finset.powersetCard r Finset.univ ↔ Set.Sized r ↑𝒜

theorem Set.Sized.subset_powersetCard_univ {α : Type u_1} [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} : Set.Sized r ↑𝒜 → 𝒜 ⊆ Finset.powersetCard r Finset.univ

Alias of the reverse direction of Finset.subset_powersetCard_univ_iff.

theorem Set.Sized.card_le {α : Type u_1} [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} (h𝒜 : Set.Sized r ↑𝒜) : 𝒜.card ≤ (Fintype.card α).choose r

Slices

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

• 𝒜.slice r = Finset.filter (fun (A : Finset α) => A.card = r) 𝒜

def Finset.«term_#_» : Lean.TrailingParserDescr

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

Equations

• Finset.«term_#_» = Lean.ParserDescr.trailingNode `Finset.term_#_ 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 91))

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 : ℕ} : Set.Sized 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₁ : Finset α} {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.pairwiseDisjoint_slice {α : Type u_1} {𝒜 : Finset (Finset α)} : Set.univ.PairwiseDisjoint 𝒜.slice

@[simp]

theorem Finset.biUnion_slice {α : Type u_1} (𝒜 : Finset (Finset α)) [Fintype α] [DecidableEq α] : (Finset.Iic (Fintype.card α)).biUnion 𝒜.slice = 𝒜

@[simp]

theorem Finset.sum_card_slice {α : Type u_1} (𝒜 : Finset (Finset α)) [Fintype α] : ∑ r ∈ Finset.Iic (Fintype.card α), (𝒜.slice r).card = 𝒜.card