le_add_one — Mathlib

English

If s is equitable on f, then every a ∈ s satisfies f(a) ≤ average + 1.

Русский

Если s эквитиально по f, то для каждого a ∈ s выполняется f(a) ≤ среднее + 1.

LaTeX

$$$$ \\text{If } s.EquitableOn(f) \\text{ and } a \\in s, \\quad f(a) \\le \\frac{\\sum_{i\\in s} f(i)}{s.card} + 1. $$$$

Lean4

theorem le_add_one (h : EquitableOn (s : Set α) f) (ha : a ∈ s) : f a ≤ (∑ i ∈ s, f i) / s.card + 1 :=
  (equitableOn_iff_le_le_add_one.1 h a ha).2

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