English
If h is a constructive inequality between f and g and sums are finite, then sf < sg.
Русский
Если между f и g существует строгая неравенство и суммы конечны, тогда sf < sg.
LaTeX
$$$\\\\forall f,g : \\\\mathbb{N} \\\\to \\\\mathbb{R}_{\\\\ge 0∞}, \\\\forall sf sg \\\\in \\\\mathbb{R}_{\\\\ge 0∞}, \\\\Big(\\\\forall a, f(a) \\\\le g(a)\\\\Rightarrow \\\\exists a, f(a) < g(a)\\\\Rightarrow \\\\mathrm{HasSum}(f,sf) \\\\land \\\\mathrm{HasSum}(g,sg) \\\\Rightarrow \\\\mathrm{Real}.lt sf sg\\\\Big)$$$
Lean4
theorem tsum_lt_tsum {f g : α → ℝ≥0∞} {i : α} (hfi : tsum f ≠ ∞) (h : ∀ a : α, f a ≤ g a) (hi : f i < g i) :
∑' x, f x < ∑' x, g x :=
hasSum_lt h hi hfi ENNReal.summable.hasSum ENNReal.summable.hasSum
