mathlib documentation

order.partition.equipartition

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.is_equipartition {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :
Prop

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

Equations
theorem finpartition.is_equipartition_iff_card_parts_eq_average {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :
P.is_equipartition ∀ (a : finset α), a P.partsa.card = s.card / P.parts.card a.card = s.card / P.parts.card + 1
theorem set.subsingleton.is_equipartition {α : Type u_1} [decidable_eq α] {s : finset α} {P : finpartition s} (h : (P.parts).subsingleton) :
theorem finpartition.is_equipartition.card_parts_eq_average {α : Type u_1} [decidable_eq α] {s t : finset α} {P : finpartition s} (hP : P.is_equipartition) (ht : t P.parts) :
theorem finpartition.is_equipartition.average_le_card_part {α : Type u_1} [decidable_eq α] {s t : finset α} {P : finpartition s} (hP : P.is_equipartition) (ht : t P.parts) :
theorem finpartition.is_equipartition.card_part_le_average_add_one {α : Type u_1} [decidable_eq α] {s t : finset α} {P : finpartition s} (hP : P.is_equipartition) (ht : t P.parts) :

Discrete and indiscrete finpartition #