Finite equipartitions #
This file defines finite equipartitions, the partitions whose parts all are the same size up to a
difference of 1
.
Main declarations #
Finpartition.IsEquipartition
: Predicate for aFinpartition
to be an equipartition.
def
Finpartition.IsEquipartition
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
(P : Finpartition s)
:
An equipartition is a partition whose parts are all the same size, up to a difference of 1
.
Instances For
theorem
Finpartition.isEquipartition_iff_card_parts_eq_average
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
(P : Finpartition s)
:
Finpartition.IsEquipartition P ↔ ∀ (a : Finset α),
a ∈ P.parts →
Finset.card a = Finset.card s / Finset.card P.parts ∨ Finset.card a = Finset.card s / Finset.card P.parts + 1
theorem
Finpartition.Set.Subsingleton.isEquipartition
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{P : Finpartition s}
(h : Set.Subsingleton ↑P.parts)
:
theorem
Finpartition.IsEquipartition.card_parts_eq_average
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{t : Finset α}
{P : Finpartition s}
(hP : Finpartition.IsEquipartition P)
(ht : t ∈ P.parts)
:
Finset.card t = Finset.card s / Finset.card P.parts ∨ Finset.card t = Finset.card s / Finset.card P.parts + 1
theorem
Finpartition.IsEquipartition.average_le_card_part
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{t : Finset α}
{P : Finpartition s}
(hP : Finpartition.IsEquipartition P)
(ht : t ∈ P.parts)
:
Finset.card s / Finset.card P.parts ≤ Finset.card t
theorem
Finpartition.IsEquipartition.card_part_le_average_add_one
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{t : Finset α}
{P : Finpartition s}
(hP : Finpartition.IsEquipartition P)
(ht : t ∈ P.parts)
:
Finset.card t ≤ Finset.card s / Finset.card P.parts + 1
Discrete and indiscrete finpartition #
theorem
Finpartition.top_isEquipartition
{α : Type u_1}
[DecidableEq α]
(s : Finset α)
[Decidable (s = ⊥)]
:
theorem
Finpartition.indiscrete_isEquipartition
{α : Type u_1}
[DecidableEq α]
(s : Finset α)
{hs : s ≠ ∅}
: