tsum_pos — Mathlib

English

If g: α → ℝ≥0 is summable and some i satisfies 0 < g(i), then the total sum ∑' g is positive.

Русский

Если сумма по g суммируема и есть элемент, где g(i) > 0, тогда общая сумма положительна.

LaTeX

$$$\\\\mathrm{Summable}(g) \\\\Rightarrow \\\\forall i, 0 < g(i) \\\\Rightarrow 0 < \\\\sum' b, g(b)$$$

Lean4

theorem tsum_pos {g : α → ℝ≥0} (hg : Summable g) (i : α) (hi : 0 < g i) : 0 < ∑' b, g b := by
  simpa using tsum_lt_tsum (fun a => zero_le _) hi hg

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