cauchySeq_finset_of_norm_bounded — Mathlib

English

Assume Summable g and pointwise bound ‖f(i)‖ ≤ g(i) for all i; then the finite-sum net is Cauchy.

Русский

Пусть ∑ g_i сходится и для каждого i верно ‖f(i)‖ ≤ g(i); тогда сеть конечных сумм сходится (Коши).

LaTeX

$$$\\text{Summable } g \\land (\\forall i, \\|f(i)\\| \\le g(i)) \\Rightarrow \\text{CauchySeq} \\bigl( s \\mapsto \\sum_{i\\in s} f(i) \\bigr)$$$

Lean4

theorem cauchySeq_finset_of_norm_bounded {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) :
    CauchySeq fun s : Finset ι => ∑ i ∈ s, f i :=
  cauchySeq_finset_of_norm_bounded_eventually hg <| Eventually.of_forall h

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