isBoundedUnder_le_mul_tendsto_zero

English

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

Русский

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

LaTeX

$$$ \\text{If } \\forall \\epsilon>0, \\exists M:\\, \\|f(x)\\| \\le M \\\\text{ and } g \\to 0, \\text{ then } f(x)g(x) \\to 0.$$$

Lean4

theorem isBoundedUnder_le_mul_tendsto_zero {f g : ι → α} {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_mul_le y x).trans_eq (mul_comm _ _)

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