# 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 ()) :

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

Equations
• = ∀ ⦃x : ⦄, x Ax.card = r
Instances For
theorem Set.Sized.mono {α : Type u_1} {A : Set ()} {B : Set ()} {r : } (h : A B) (hB : ) :
@[simp]
theorem Set.sized_empty {α : Type u_1} {r : } :
@[simp]
theorem Set.sized_singleton {α : Type u_1} {s : } {r : } :
Set.Sized r {s} s.card = r
theorem Set.sized_union {α : Type u_1} {A : Set ()} {B : Set ()} {r : } :
Set.Sized r (A B)
theorem Set.sized.union {α : Type u_1} {A : Set ()} {B : Set ()} {r : } :
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 ()} :
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 ()} :
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 ()} {r : } (hA : ) :
IsAntichain (fun (x x_1 : ) => x x_1) A
theorem Set.Sized.subsingleton {α : Type u_1} {A : Set ()} (hA : ) :
theorem Set.Sized.subsingleton' {α : Type u_1} {A : Set ()} [] (hA : ) :
theorem Set.Sized.empty_mem_iff {α : Type u_1} {A : Set ()} {r : } (hA : ) :
A A = {}
theorem Set.Sized.univ_mem_iff {α : Type u_1} {A : Set ()} {r : } [] (hA : ) :
Finset.univ A A = {Finset.univ}
theorem Set.sized_powersetCard {α : Type u_1} (s : ) (r : ) :
Set.Sized r ()
theorem Finset.subset_powersetCard_univ_iff {α : Type u_1} [] {𝒜 : Finset ()} {r : } :
𝒜 Finset.powersetCard r Finset.univ Set.Sized r 𝒜
theorem Set.Sized.subset_powersetCard_univ {α : Type u_1} [] {𝒜 : 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} [] {𝒜 : Finset ()} {r : } (h𝒜 : Set.Sized r 𝒜) :
𝒜.card

### Slices #

def Finset.slice {α : Type u_1} (𝒜 : 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 ()} {A : } {r : } :
A 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 ()} {r : } :
𝒜

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

theorem Finset.sized_slice {α : Type u_1} {𝒜 : Finset ()} {r : } :
Set.Sized r ()

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

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

Elements in distinct slices must be distinct.

theorem Finset.pairwiseDisjoint_slice {α : Type u_1} {𝒜 : Finset ()} :
@[simp]
theorem Finset.biUnion_slice {α : Type u_1} (𝒜 : Finset ()) [] [] :
= 𝒜
@[simp]
theorem Finset.sum_card_slice {α : Type u_1} (𝒜 : Finset ()) [] :
(Finset.sum () fun (r : ) => ().card) = 𝒜.card