Theorems · Definition · combinatorics

Finpartition.equitabilise

{α : Type u_1} →
  [inst : DecidableEq α] →
    {s : Finset α} → {m a b : ℕ} → {P : Finpartition s} → a * m + b * (m + 1) = s.card → Finpartition s

Given a partition P of s, as well as a proof that a * m + b * (m + 1) = #s, build a new partition Q of s where each part has size m or m + 1, every part of P is the union of parts of Q plus at most m extra elements, there are b parts of size m + 1 and (provided m > 0, because a partition does not have parts of size 0) there are a parts of size m and hence a + b parts in total.

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Cited by

9 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq