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 a Finpartition to be an equipartition.

def Finpartition.IsEquipartition {α : Type u_1} [DecidableEq α] {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

• Finpartition.IsEquipartition P = Set.EquitableOn (↑P.parts) Finset.card

theorem Finpartition.isEquipartition_iff_card_parts_eq_average {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : Finpartition.IsEquipartition P ↔ ∀ a ∈ P.parts, a.card = s.card / P.parts.card ∨ a.card = s.card / P.parts.card + 1

theorem Finpartition.not_isEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} : ¬Finpartition.IsEquipartition P ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, b.card + 1 < a.card

theorem Finpartition.Set.Subsingleton.isEquipartition {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (h : Set.Subsingleton ↑P.parts) : Finpartition.IsEquipartition P

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) : 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} [DecidableEq α] {s : Finset α} {t : Finset α} {P : Finpartition s} (hP : Finpartition.IsEquipartition P) (ht : t ∈ P.parts) : s.card / P.parts.card ≤ t.card

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) : t.card ≤ s.card / P.parts.card + 1

Discrete and indiscrete finpartition

theorem Finpartition.bot_isEquipartition {α : Type u_1} [DecidableEq α] (s : Finset α) : Finpartition.IsEquipartition ⊥

theorem Finpartition.top_isEquipartition {α : Type u_1} [DecidableEq α] (s : Finset α) [Decidable (s = ⊥)] : Finpartition.IsEquipartition ⊤

theorem Finpartition.indiscrete_isEquipartition {α : Type u_1} [DecidableEq α] (s : Finset α) {hs : s ≠ ∅} : Finpartition.IsEquipartition (Finpartition.indiscrete hs)