mul — Mathlib

English

If f and g converge to a and b respectively, then f·g converges to a·b under multiplication.

Русский

Если f стремится к a, а g стремится к b, то произведение f·g стремится к a·b.

LaTeX

$$$\\forall \\alpha\\, f,g : \\alpha \\to M,\\; x:\\text{Filter } \\alpha,\\; (hf : Tendsto\\ f\\ x\\ (nhds a))\\to (hg : Tendsto\\ g\\ x\\ (nhds b))\\Rightarrow Tendsto (\\lambda t. f t \\cdot g t)\\ x\\ (nhds (a\\cdot b))$$$

Lean4

@[to_additive]
theorem mul {α : Type*} {f g : α → M} {x : Filter α} {a b : M} (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) :
    Tendsto (fun x ↦ f x * g x) x (𝓝 (a * b)) :=
  (continuous_mul.tendsto _).comp (hf.prodMk_nhds hg)

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