sum_le_tsum — Mathlib

English

For any finite set s ⊆ α, the finite sum is bounded above by the infinite sum: ∑_{x ∈ s} f(x) ≤ ∑' x, f(x).

Русский

Для любого конечного множества s ⊆ α скалярная сумма не превосходит бесконечную сумму: ∑_{x ∈ s} f(x) ≤ ∑' x, f(x).

LaTeX

$$$\sum_{x \in s} f(x) \le \sum'_{x \in \alpha} f(x)$$$

Lean4

protected theorem sum_le_tsum {f : α → ℝ≥0∞} (s : Finset α) : ∑ x ∈ s, f x ≤ ∑' x, f x :=
  ENNReal.summable.sum_le_tsum s (fun _ _ => zero_le _)

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