average_le_card_part — Mathlib

English

For any part t of an equipartition P of s, the average size of s divided by the number of parts is a lower bound for |s| divided by |P.parts|, hence #s/ #P.parts ≤ |t|.

Русский

Для любой части t равноправного разбиения P множества s средний размер — нижняя граница для |t|, то есть |s|/|P.parts| ≤ |t|.

LaTeX

$$#s / #P.parts ≤ #t$$

Lean4

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

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