isBoundedUnder_ge_sum — Mathlib

English

For a finite κ, if each u_k is f-bounded below under ≥, then the sum over s is f-bounded below under ≥.

Русский

Для конечного множества κ, если каждый u_k ограничен снизу по ≥, то сумма по k∈s также ограничена снизу.

LaTeX

$$$\forall s,\ (\forall k ∈ s\, f.IsBoundedUnder(≥)\ (u_k)) \Rightarrow f.IsBoundedUnder(≥)\left(\sum_{k \in s} u_k\right)$$$

Lean4

theorem isBoundedUnder_ge_sum {κ : Type*} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R}
    (s : Finset κ) : (∀ k ∈ s, f.IsBoundedUnder (· ≥ ·) (u k)) → f.IsBoundedUnder (· ≥ ·) (∑ k ∈ s, u k) := fun h ↦
  isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_ge_add) le_rfl s h

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