card_part_eq_average_iff — Mathlib

English

If P is equipartition and t is a part of P, then either t.card equals the average |s|/|P.parts| or it equals that plus 1.

Русский

Если P — равноправное разбиение и t является частью P, то |t| либо равно среднему, либо на единицу больше.

LaTeX

$$P.IsEquipartition → ∀ t ∈ P.parts, |t| = |s|/|P.parts| ∨ |t| = |s|/|P.parts| + 1$$

Lean4

theorem card_part_eq_average_iff (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
    #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1 :=
  by
  have a := hP.card_parts_eq_average ht
  cutsat

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