lean_workbook_plus_37227

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $a_{n}< b_{n}$ for all $n$ , and the sums of the two sequences converge, then $\sum a_{n}< \sum b_{n}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37227 (ι : Type*) (a b : ι → ℝ) (h₁ : Nonempty ι) (h₂ : ∀ n, a n < b n) (h₃ : Summable a) (h₄ : Summable b) : ∑' n, a n < ∑' n, b n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph