zero_mul_isBoundedUnder_le — Mathlib

English

If f tends to zero and g is bounded in norm along a filter, then the pointwise product f(x)g(x) tends to zero.

Русский

Если f сходится к нулю и g ограничен по норме вдоль фильтра, то произведение f(x)g(x) сходится к нулю.

LaTeX

$$$ \\text{If } f:\\iota\\to \\alpha,\\ g:\\iota\\to \\alpha, \\text{ with } f\\to 0 \\text{ along } l \\text{ and } \\|g\\| \\text{ bounded along } l, \\; f\\cdot g \\to 0.$$$

Lean4

theorem zero_mul_isBoundedUnder_le {f g : ι → α} {l : Filter ι} (hf : Tendsto f l (𝓝 0))
    (hg : IsBoundedUnder (· ≤ ·) l ((‖·‖) ∘ g)) : Tendsto (fun x => f x * g x) l (𝓝 0) :=
  hf.op_zero_isBoundedUnder_le hg (· * ·) norm_mul_le

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