tsum_le_tsum — Mathlib

English

If f,g : α → ENNReal satisfy f(a) ≤ g(a) for all a, then the total sum is monotone: ∑' a, f(a) ≤ ∑' a, g(a).

Русский

Если для всех a выполняется f(a) ≤ g(a), то сумма монотонна: ∑'_a f(a) ≤ ∑'_a g(a).

LaTeX

$$$\left( \forall a, f(a) \le g(a) \right) \rightarrow \sum'_{a \in \alpha} f(a) \le \sum'_{a \in \alpha} g(a)$$$

Lean4

protected theorem tsum_le_tsum (h : ∀ a, f a ≤ g a) : ∑' a, f a ≤ ∑' a, g a :=
  ENNReal.summable.tsum_le_tsum h ENNReal.summable

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