English
For a CauSeq f with nonzero limit, for every ε>0 there exists i such that for all j ≥ i, abv((f(j))^{-1} - (f(i))^{-1}) < ε.
Русский
Для кау-секвенции f с ненулевой предельной величиной для любого ε>0 существует i, такое что для всех j≥i выполняется abv((f(j))^{-1} - (f(i))^{-1}) < ε.
LaTeX
$$$ \forall \varepsilon>0,\; \exists i,\; \forall j \ge i,\; abv\left((f(j))^{-1} - (f(i))^{-1}\right) < \varepsilon. $$$
Lean4
theorem inv_aux {f : CauSeq β abv} (hf : ¬LimZero f) : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv ((f j)⁻¹ - (f i)⁻¹) < ε
| _, ε0 =>
let ⟨_, K0, HK⟩ := abv_pos_of_not_limZero hf
let ⟨_, δ0, Hδ⟩ := rat_inv_continuous_lemma abv ε0 K0
let ⟨i, H⟩ := exists_forall_ge_and HK (f.cauchy₃ δ0)
⟨i, fun _ ij =>
let ⟨iK, H'⟩ := H _ le_rfl
Hδ (H _ ij).1 iK (H' _ ij)⟩
