zero_smul_isBoundedUnder_le — Mathlib

English

If f tends to 0 and g is bounded in a monotone sense, then f x • g x tends to 0.

Русский

Если f стремится к 0 и g ограничено по лексикографическому отношению, то f x • g x стремится к 0.

LaTeX

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

Lean4

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

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