IsEquipartition — Mathlib

English

An equipartition of a finite partition is one in which all parts have sizes that are as equal as possible (differing by at most 1).

Русский

Равноправное разбиение — это разбиение, у которого все части имеют размеры, максимально близкие друг к другу и различаются не более чем на 1.

LaTeX

$$$P.IsEquipartition\iff (P.parts : Set( Finset\ α)).EquitableOn\; card$$$

Lean4

/-- An equipartition is a partition whose parts are all the same size, up to a difference of `1`. -/
def IsEquipartition : Prop :=
  (P.parts : Set (Finset α)).EquitableOn card

Похожие утверждения