English
A family of partial sums indexed by finite subsets is Cauchy if and only if tails over disjoint finite sets can be made arbitrarily small.
Русский
Пусть частичные суммы по конечным подмножествам образуют дробный ряд, тогда он является Коши тогда и только тогда, когда хвосты по взаимно непересекающимся конечным множествам можно сделать произвольно малыми.
LaTeX
$$$\\left( \\text{CauchySeq} \\bigl( s \\mapsto \\sum_{i \\in s} f(i) \\bigr) \\right) \\iff \\forall \\varepsilon>0,\\ \\exists S: Finset\\ ι,\\ \\forall T,\\ Disjoint(T,S) \\Rightarrow \\Bigl\\|\\sum_{i \\in T} f(i)\\Bigr| < \\varepsilon$$$
Lean4
theorem cauchySeq_finset_iff_vanishing_norm {f : ι → E} :
(CauchySeq fun s : Finset ι => ∑ i ∈ s, f i) ↔
∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε :=
by
rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
· simp only [ball_zero_eq, Set.mem_setOf_eq]
· rintro s t hst ⟨s', hs'⟩
exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩
