English
A variant of Tendsto for multiplication: given suitable hypotheses, the product tends to the product of limits.
Русский
Вариант теоремы о пределках для умножения: при подходящих предположениях произведение стремится к произведению пределов.
LaTeX
$$$\\mathrm{Tendsto}\\ (f,ma,mb)\\ to\\ nhds(a b) \\\\text{under appropriate hypotheses}$$$
Lean4
protected theorem mul {f : Filter α} {ma : α → EReal} {mb : α → EReal} {a b : EReal} (hma : Tendsto ma f (𝓝 a))
(hmb : Tendsto mb f (𝓝 b)) (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) (h₃ : a ≠ ⊥ ∨ b ≠ 0) (h₄ : a ≠ ⊤ ∨ b ≠ 0) :
Tendsto (fun x ↦ ma x * mb x) f (𝓝 (a * b)) :=
(EReal.tendsto_mul h₁ h₂ h₃ h₄).comp (hma.prodMk_nhds hmb)
