smul_tendsto_zero — Mathlib

English

If f is bounded under ≤ and g tends to 0, then f(x) • g(x) tends to 0.

Русский

Если f ограничено по ≤ и g(x) → 0, то f(x) • g(x) → 0.

LaTeX

$$$\\text{Tendsto } g \\; l \\to 0 \\Rightarrow \\text{Tendsto } (\\lambda x, f(x) \\cdot g(x)) \\; l \\to 0$$$

Lean4

theorem smul_tendsto_zero {f : α → 𝕜} {g : α → E} {l : Filter α} (hf : IsBoundedUnder (· ≤ ·) l (norm ∘ f))
    (hg : Tendsto g l (𝓝 0)) : Tendsto (fun x => f x • g x) l (𝓝 0) :=
  hg.op_zero_isBoundedUnder_le hf (flip (· • ·)) fun x y => (norm_smul_le y x).trans_eq (mul_comm _ _)

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