English
Let f: I → ℝ satisfy f(i) ≥ 0 for all i and suppose that every finite partial sum ∑_{x∈U} f(x) is bounded above by a constant c. Then f is summable (the series ∑ f(i) converges).
Русский
Пусть f: I → ℝ удовлетворяет f(i) ≥ 0 для всех i и каждую конечную подпоследовательность U ⊆ I имеет сумму ∑_{x∈U} f(x) ≤ c. Тогда серия ∑ f(i) сходится (суммируема).
LaTeX
$$$\left(\forall i, f(i) \ge 0\right) \land \left(\forall U \subseteq \iota,\ U \text{ finite }\Rightarrow \sum_{x\in U} f(x) \le c\right) \Rightarrow \text{Summable } f$$$
Lean4
theorem summable_of_sum_le {ι : Type*} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f) (h : ∀ u : Finset ι, ∑ x ∈ u, f x ≤ c) :
Summable f :=
⟨⨆ u : Finset ι, ∑ x ∈ u, f x, tendsto_atTop_ciSup (Finset.sum_mono_set_of_nonneg hf) ⟨c, fun _ ⟨u, hu⟩ => hu ▸ h u⟩⟩
