English
LimZero is the property that a CauSeq approaches zero; f.LimZero means for every ε>0 there exists i with abv(f_j) < ε for all j ≥ i.
Русский
LimZero — это свойство, что CauSeq стремится к нулю; f.LimZero означает, что для любого ε>0 существует i такое, что abv(f_j) < ε при всех j ≥ i.
LaTeX
$$$\text{LimZero}(f) := \forall \varepsilon>0, \exists i, \forall j\ge i, abv(f_j) < \varepsilon$$$
Lean4
theorem add_limZero {f g : CauSeq β abv} (hf : LimZero f) (hg : LimZero g) : LimZero (f + g)
| ε, ε0 =>
(exists_forall_ge_and (hf _ <| half_pos ε0) (hg _ <| half_pos ε0)).imp fun _ H j ij =>
by
let ⟨H₁, H₂⟩ := H _ ij
simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)
