# Finite equipartitions #

This file defines finite equipartitions, the partitions whose parts all are the same size up to a difference of 1.

## Main declarations #

def Finpartition.IsEquipartition {α : Type u_1} [] {s : } (P : ) :

An equipartition is a partition whose parts are all the same size, up to a difference of 1.

Equations
• P.IsEquipartition = (P.parts).EquitableOn Finset.card
Instances For
theorem Finpartition.isEquipartition_iff_card_parts_eq_average {α : Type u_1} [] {s : } (P : ) :
P.IsEquipartition aP.parts, a.card = s.card / P.parts.card a.card = s.card / P.parts.card + 1
theorem Finpartition.not_isEquipartition {α : Type u_1} [] {s : } {P : } :
¬P.IsEquipartition aP.parts, bP.parts, b.card + 1 < a.card
theorem Set.Subsingleton.isEquipartition {α : Type u_1} [] {s : } {P : } (h : (P.parts).Subsingleton) :
P.IsEquipartition
theorem Finpartition.IsEquipartition.card_parts_eq_average {α : Type u_1} [] {s : } {t : } {P : } (hP : P.IsEquipartition) (ht : t P.parts) :
t.card = s.card / P.parts.card t.card = s.card / P.parts.card + 1
theorem Finpartition.IsEquipartition.average_le_card_part {α : Type u_1} [] {s : } {t : } {P : } (hP : P.IsEquipartition) (ht : t P.parts) :
s.card / P.parts.card t.card
theorem Finpartition.IsEquipartition.card_part_le_average_add_one {α : Type u_1} [] {s : } {t : } {P : } (hP : P.IsEquipartition) (ht : t P.parts) :
t.card s.card / P.parts.card + 1

### Discrete and indiscrete finpartition #

theorem Finpartition.bot_isEquipartition {α : Type u_1} [] (s : ) :
.IsEquipartition
theorem Finpartition.top_isEquipartition {α : Type u_1} [] (s : ) [Decidable (s = )] :
.IsEquipartition
theorem Finpartition.indiscrete_isEquipartition {α : Type u_1} [] (s : ) {hs : s } :
.IsEquipartition