English
If a sequence f:ℕ→β is close to a CauSeq g termwise (abv(f_j − g_j) small for all j after some index), and g is CauSeq, then f is a CauSeq.
Русский
Если последовательность f близка к CauSeq g покомпонентно после некоторого индекса и g — CauSeq, то и f является CauSeq.
LaTeX
$$$\forall f:\mathbb{N}\to \beta, \forall g: CauSeq(\beta, abv), \bigl( \forall \varepsilon>0, \exists i, \forall j\ge i, abv(f_j - g_j) < \varepsilon \bigr) \Rightarrow IsCauSeq(abv,f)$$$
Lean4
theorem of_near (f : ℕ → β) (g : CauSeq β abv) (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - g j) < ε) : IsCauSeq abv f
| ε, ε0 =>
let ⟨i, hi⟩ := exists_forall_ge_and (h _ (half_pos <| half_pos ε0)) (g.cauchy₃ <| half_pos ε0)
⟨i, fun j ij => by
obtain ⟨h₁, h₂⟩ := hi _ le_rfl; rw [abv_sub abv] at h₁
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij))
rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this⟩
