lim_mul_lim — Mathlib

English

Limit distributes over products: lim f · lim g = lim (f · g).

Русский

Предел распределяется по произведениям: lim f · lim g = lim (f · g).

LaTeX

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

Lean4

theorem lim_mul_lim (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
      have h :
        const abv (lim f * lim g) - f * g = (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g) :=
        by
        apply Subtype.ext
        rw [coe_add]
        simp [sub_mul, mul_sub]
      rw [h]
      exact
        add_limZero (mul_limZero_left _ (Setoid.symm (equiv_lim _))) (mul_limZero_right _ (Setoid.symm (equiv_lim _)))

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