cauchySeq_of_edist_le_of_tsum_ne_top

English

If a sequence has successive edist bounded by a summable series with tsum finite, then the sequence is Cauchy.

Русский

Если расстояния между соседними элементами управляются суммируемой последовательностью, чья сумма конечна, то последовательность Коши.

LaTeX

$$$\forall d: \mathbb{N} \to \mathbb{R}_{≥0}, (\forall n, edist(f_n,f_{n+1}) ≤ d(n)) → (tsum d ≠ ∞) → \text{CauchySeq}(f).$$$

Lean4

theorem cauchySeq_of_edist_le_of_tsum_ne_top {f : ℕ → α} (d : ℕ → ℝ≥0∞) (hf : ∀ n, edist (f n) (f n.succ) ≤ d n)
    (hd : tsum d ≠ ∞) : CauchySeq f :=
  by
  lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i
  rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd
  exact cauchySeq_of_edist_le_of_summable d hf hd

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