tendsto_mul_zero_of_right — Mathlib

English

If R is linearly topologized (on the right), then similar right-multiplication convergence holds.

Русский

Если правая линейная топология, сохраняется сходство по правому умножению.

LaTeX

$$$ [IsLinearTopology R R] \\Rightarrow \\text{tendsto\\_mul\\_zero\_of\_right} : a,b \\to 0 \\Rightarrow a\\cdot b \\to 0. $$$

Lean4

theorem tendsto_mul_zero_of_right [IsLinearTopology R R] {ι : Type*} {f : Filter ι} (a b : ι → R)
    (hb : Tendsto b f (𝓝 0)) : Tendsto (a * b) f (𝓝 0) :=
  tendsto_smul_zero (R := R) _ _ hb

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