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 thatA
only containsr
-sets.Finset.slice
:A.slice r
is the set ofr
-sets inA
.
Notation #
A # r
is notation for A.slice r
in locale finset_family
.
Families of r
-sets #
theorem
Set.sized_unionᵢ₂
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
{r : ℕ}
{f : (i : ι) → κ i → Set (Finset α)}
:
Set.Sized r (Set.unionᵢ fun i => Set.unionᵢ fun j => 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 => x ⊆ x_1) A
theorem
Set.Sized.subsingleton'
{α : Type u_1}
{A : Set (Finset α)}
[inst : Fintype α]
(hA : Set.Sized (Fintype.card α) A)
:
theorem
Set.sized_powersetLen
{α : Type u_1}
(s : Finset α)
(r : ℕ)
:
Set.Sized r ↑(Finset.powersetLen r s)
theorem
Set.Sized.subset_powersetLen_univ
{α : Type u_1}
[inst : Fintype α]
{𝒜 : Finset (Finset α)}
{r : ℕ}
:
Set.Sized r ↑𝒜 → 𝒜 ⊆ Finset.powersetLen r Finset.univ
Alias of the reverse direction of Finset.subset_powersetLen_univ_iff
.
theorem
Finset.Set.Sized.card_le
{α : Type u_1}
[inst : Fintype α]
{𝒜 : Finset (Finset α)}
{r : ℕ}
(h𝒜 : Set.Sized r ↑𝒜)
:
Finset.card 𝒜 ≤ Nat.choose (Fintype.card α) r
Slices #
The r
-th slice of a set family is the subset of its elements which have cardinality r
.
Equations
- Finset.slice 𝒜 r = Finset.filter (fun i => Finset.card i = r) 𝒜
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 ∈ Finset.slice 𝒜 r ↔ A ∈ 𝒜 ∧ Finset.card A = r
A
is in the r
-th slice of 𝒜
iff it's in 𝒜
and has cardinality r
.
The r
-th slice of 𝒜
is a subset of 𝒜
.
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
.
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₂
theorem
Finset.pairwiseDisjoint_slice
{α : Type u_1}
{𝒜 : Finset (Finset α)}
:
Set.PairwiseDisjoint Set.univ (Finset.slice 𝒜)
@[simp]
theorem
Finset.bunionᵢ_slice
{α : Type u_1}
(𝒜 : Finset (Finset α))
[inst : Fintype α]
[inst : DecidableEq α]
:
Finset.bunionᵢ (Finset.Iic (Fintype.card α)) (Finset.slice 𝒜) = 𝒜
@[simp]
theorem
Finset.sum_card_slice
{α : Type u_1}
(𝒜 : Finset (Finset α))
[inst : Fintype α]
:
(Finset.sum (Finset.Iic (Fintype.card α)) fun r => Finset.card (Finset.slice 𝒜 r)) = Finset.card 𝒜