cauchy₃ — Mathlib

English

A Cau sequence is bounded: there exists an r such that for all i, abv(f(i)) < r.

Русский

Последовательность Cau ограничена: существует r, такого что для всех i выполнено abv(f(i)) < r.

LaTeX

$$∃ r, ∀ i, abv(f(i)) < r$$

Lean4

theorem cauchy₃ (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) : ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε :=
  let ⟨i, H⟩ := hf.cauchy₂ ε0
  ⟨i, fun _ ij _ jk => H _ (le_trans ij jk) _ ij⟩

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