`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 #

source

def Set.Sized {α : Type u_1} (r : ℕ) (A : Set (Finset α)) :

Prop

Sized r A means that every Finset in A has size r.

Instances For

source

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

source

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

source

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.

source

@[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)

source

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)

source

theorem Set.Sized.isAntichain {α : Type u_1} {A : Set (Finset α)} {r : ℕ} (hA : Set.Sized r A) :

IsAntichain (fun x x_1 => x ⊆ x_1) A

source

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

Set.Subsingleton A

source

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

Set.Subsingleton A

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_powersetLen {α : Type u_1} (s : Finset α) (r : ℕ) :

Set.Sized r ↑(Finset.powersetLen r s)

source

theorem Finset.subset_powersetLen_univ_iff {α : Type u_1} [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} :

𝒜 ⊆ Finset.powersetLen r Finset.univ ↔ Set.Sized r ↑𝒜

source

theorem Set.Sized.subset_powersetLen_univ {α : Type u_1} [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} :

Set.Sized r ↑𝒜 → 𝒜 ⊆ Finset.powersetLen r Finset.univ

Alias of the reverse direction of Finset.subset_powersetLen_univ_iff.

source

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

Finset.card 𝒜 ≤ Nat.choose (Fintype.card α) 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.

Instances For

source

def Finset.«term_#_» :

Lean.TrailingParserDescr

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

Instances For

source

theorem Finset.mem_slice {α : Type u_1} {𝒜 : Finset (Finset α)} {A : Finset α} {r : ℕ} :

A ∈ Finset.slice 𝒜 r ↔ A ∈ 𝒜 ∧ Finset.card A = 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 : ℕ} :

Finset.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 ↑(Finset.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 ∈ Finset.slice 𝒜 r₁) (h₂ : A ∈ Finset.slice 𝒜 r₂) :

r₁ = r₂

source

theorem Finset.ne_of_mem_slice {α : Type u_1} {𝒜 : Finset (Finset α)} {A₁ : Finset α} {A₂ : Finset α} {r₁ : ℕ} {r₂ : ℕ} (h₁ : A₁ ∈ Finset.slice 𝒜 r₁) (h₂ : A₂ ∈ Finset.slice 𝒜 r₂) :

r₁ ≠ r₂ → A₁ ≠ A₂

Elements in distinct slices must be distinct.

source