isEquipartition_iff_card_parts_eq_average

English

For a Finpartition P, being equipartition is equivalent to every part having size either floor(|s|/|P|) or floor(|s|/|P|) + 1.

Русский

Для Finpartition P равноправие эквивалентно тому, что каждая часть имеет размер либо floor(|s|/|P|), либо floor(|s|/|P|) + 1.

LaTeX

$$$P.IsEquipartition \iff \forall a \in P.parts,\ |a| = \left\lfloor\frac{|s|}{|P.parts|}\right\rfloor \text{ or } |a| = \left\lfloor\frac{|s|}{|P.parts|}\right\rfloor + 1$$$

Lean4

theorem isEquipartition_iff_card_parts_eq_average :
    P.IsEquipartition ↔ ∀ a : Finset α, a ∈ P.parts → #a = #s / #P.parts ∨ #a = #s / #P.parts + 1 := by
  simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]

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