mathlib3 documentation

order.partition.equipartition

Finite equipartitions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

finpartition.is_equipartition: Predicate for a finpartition to be an equipartition.

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

P.is_equipartition = ↑(P.parts).equitable_on finset.card

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.parts → a.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) :

P.is_equipartition

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) :

t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1

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) :

s.card / P.parts.card ≤ t.card

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) :

t.card ≤ s.card / P.parts.card + 1

Discrete and indiscrete finpartition #

theorem finpartition.bot_is_equipartition {α : Type u_1} [decidable_eq α] (s : finset α) :

⊥.is_equipartition

theorem finpartition.top_is_equipartition {α : Type u_1} [decidable_eq α] (s : finset α) :

⊤.is_equipartition

theorem finpartition.indiscrete_is_equipartition {α : Type u_1} [decidable_eq α] (s : finset α) {hs : s ≠ ∅} :

(finpartition.indiscrete hs).is_equipartition