lim_add — Mathlib

English

Limit preserves addition: lim f + lim g = lim(f + g).

Русский

Предел сохраняет сложение: lim f + lim g = lim(f + g).

LaTeX

$$$\\lim(f+g) = \\lim f + \\lim g$$$

Lean4

theorem lim_add (f g : CauSeq β abv) : lim f + lim g = lim (f + g) :=
  eq_lim_of_const_equiv <|
    show LimZero (const abv (lim f + lim g) - (f + g))
      by
      rw [const_add, add_sub_add_comm]
      exact add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))

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