Documentation

Mathlib.Data.Finset.Slice

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 #

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 α)) :

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

Equations
Instances For
    theorem Set.Sized.mono {α : Type u_1} {A : Set (Finset α)} {B : Set (Finset α)} {r : } (h : A B) (hB : Set.Sized r B) :
    @[simp]
    theorem Set.sized_empty {α : Type u_1} {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 : } :
    theorem Set.sized.union {α : Type u_1} {A : Set (Finset α)} {B : Set (Finset α)} {r : } :
    Set.Sized r A Set.Sized r BSet.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 : ι) → κ iSet (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 (x x_1 : Finset α) => x x_1) 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 : ) :
    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 : ) :

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

    Equations
    Instances For

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

      Equations
      Instances For
        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 α] :
        rFinset.Iic (Fintype.card α), (𝒜.slice r).card = 𝒜.card