Theorems · Theorem · combinatorics

Finpartition.IsEquipartition.exists_partsEquiv

∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition → ∃ f, ∀ (t : ↥P.parts), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card

There exists an enumeration of an equipartition's parts where larger parts map to smaller numbers and vice versa.

Defined in

Mathlib.Order.Partition.Equipartition

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq