finset_sup_le_sum — Mathlib

English

For a finite set s, the supremum of p is bounded by the sum of p_i over i in s: s.sup p ≤ ∑_{i∈s} p_i.

Русский

Для конечного множества s супремум p не превосходит суммы p_i по i∈s.

LaTeX

$$$s.su p p \le \sum_{i \in s} p_i$$$

Lean4

theorem finset_sup_le_sum (p : ι → Seminorm 𝕜 E) (s : Finset ι) : s.sup p ≤ ∑ i ∈ s, p i := by
  classical
  refine Finset.sup_le_iff.mpr ?_
  intro i hi
  rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]
  exact bot_le

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