le — Mathlib · SciLib

English

If h is EquitableOn for the finite set s and f, then the average over s does not exceed f(a) for any a ∈ s.

Русский

Пусть h: EquitableOn( s, f ). Тогда для любого a ∈ s среднее значение ∑_{i∈s} f(i)/|s| не превосходит значение f(a).

LaTeX

$$$$ s.toSet.EquitableOn(f) \\wedge a \\in s \\Rightarrow \\frac{\\sum_{i\\in s} f(i)}{s.card} \\le f(a). $$$$

Lean4

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

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