English
If f ≈ g, then for every ε>0 there exists i with ∀ j≥i ∀ k≥j, abv(f_k − g_j) < ε.
Русский
Если f ≈ g, для каждого ε>0 существует i, такое что ∀ j≥i ∀ k≥j выполняется abv(f_k − g_j) < ε.
LaTeX
$$$f \approx g \Rightarrow \forall \varepsilon>0, \exists i, \forall j\ge i, \forall k\ge j, abv(f_k - g_j) < \varepsilon$$$
Lean4
theorem equiv_def₃ {f g : CauSeq β abv} (h : f ≈ g) {ε : α} (ε0 : 0 < ε) : ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - g j) < ε :=
(exists_forall_ge_and (h _ <| half_pos ε0) (f.cauchy₃ <| half_pos ε0)).imp fun _ H j ij k jk =>
by
let ⟨h₁, h₂⟩ := H _ ij
have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk))
rwa [sub_add_sub_cancel', add_halves] at this
