lim_eq_zero_iff — Mathlib

English

lim f = 0 if and only if LimZero f.

Русский

lim f = 0 тогда и только тогда, когда LimZero f.

LaTeX

$$$\\lim f = 0 \\ \\,\\Longleftrightarrow\\, \\mathrm{LimZero}(f)$$$

Lean4

theorem lim_eq_zero_iff (f : CauSeq β abv) : lim f = 0 ↔ LimZero f :=
  ⟨fun h => by
    have hf := equiv_lim f
    rw [h] at hf
    exact (limZero_congr hf).mpr (const_limZero.mpr rfl), fun h =>
    by
    have h₁ : f = f - const abv 0 := ext fun n => by simp
    rw [h₁] at h
    exact lim_eq_of_equiv_const h⟩

Похожие утверждения