English
If not LimZero, there exists a positive K and an index i such that ∀ j≥i, K ≤ abv(f_j).
Русский
Если не выполнено LimZero, существует положительная константа K и индекс i, такие что ∀ j≥i выполняется K ≤ abv(f_j).
LaTeX
$$$\neg \mathrm{LimZero}(f) \Rightarrow \exists K>0, \exists i, \forall j\ge i, K \le abv(f_j)$$$
Lean4
theorem abv_pos_of_not_limZero {f : CauSeq β abv} (hf : ¬LimZero f) : ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (f j) :=
by
by_contra nk
refine hf fun ε ε0 => ?_
simp only [not_exists, not_and, not_forall, not_le] at nk
obtain ⟨i, hi⟩ := f.cauchy₃ (half_pos ε0)
rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩
refine ⟨j, fun k jk => ?_⟩
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi j ij k jk) hj)
rwa [sub_add_cancel, add_halves] at this
