card_part_le_average_add_one — Mathlib

English

Every part t of an equipartition satisfies |t| ≤ floor(|s|/|P.parts|) + 1.

Русский

Для каждой части t равноправного разбиения выполняется |t| ≤ ⌊|s|/|P.parts|⌋ + 1.

LaTeX

$$P.IsEquipartition → ∀ t ∈ P.parts, |t| ≤ floor(|s|/|P.parts|) + 1$$

Lean4

theorem card_part_le_average_add_one (hP : P.IsEquipartition) (ht : t ∈ P.parts) : #t ≤ #s / #P.parts + 1 :=
  by
  rw [← P.sum_card_parts]
  exact Finset.EquitableOn.le_add_one hP ht

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