card_parts_eq_average — Mathlib

English

For an equipartition P of s, the average of the part sizes equals |s|/|P.parts| and each part size equals either this average or this average plus 1.

Русский

При равноправном разбиении P множества s средний размер частей равен |s|/|P.parts|, и каждая часть имеет размер либо этот средний, либо на 1 больше.

LaTeX

$$P.IsEquipartition → ∀ a ∈ P.parts, |a| ∈ { |s|/|P.parts|, |s|/|P.parts| + 1 }$$

Lean4

theorem card_parts_eq_average (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
    #t = #s / #P.parts ∨ #t = #s / #P.parts + 1 :=
  P.isEquipartition_iff_card_parts_eq_average.1 hP _ ht

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