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.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 α)}
[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}
[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}
[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
.
Instances For
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.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₂)
:
Elements in distinct slices must be distinct.
theorem
Finset.pairwiseDisjoint_slice
{α : Type u_1}
{𝒜 : Finset (Finset α)}
:
Set.PairwiseDisjoint Set.univ (Finset.slice 𝒜)
@[simp]
theorem
Finset.biUnion_slice
{α : Type u_1}
(𝒜 : Finset (Finset α))
[Fintype α]
[DecidableEq α]
:
Finset.biUnion (Finset.Iic (Fintype.card α)) (Finset.slice 𝒜) = 𝒜
@[simp]
theorem
Finset.sum_card_slice
{α : Type u_1}
(𝒜 : Finset (Finset α))
[Fintype α]
:
(Finset.sum (Finset.Iic (Fintype.card α)) fun r => Finset.card (Finset.slice 𝒜 r)) = Finset.card 𝒜