English
If a ≠ 0 or b ≠ ∞ and m → b along f, then the map b ↦ a · m converges to a · b.
Русский
Если a ≠ 0 или b ≠ ∞ и m → b вдоль фильтра, тогда отображение b ↦ a · m сходится к a · b.
LaTeX
$$$\\\\forall {f} {m: α \\to ENNReal} {a b : ENNReal}, \\\\ Tendsto m f (\\\\nhds b) \\\\Rightarrow \\\\text{(a ≠ 0 ∨ b ≠ ∞)} \\\\Rightarrow \\\\text{Tendsto } (\\\\lambda x, a * m x) f (\\\\nhds (a * b)).$$$
Lean4
protected theorem mul {f : Filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞} (hma : Tendsto ma f (𝓝 a))
(ha : a ≠ 0 ∨ b ≠ ∞) (hmb : Tendsto mb f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ∞) :
Tendsto (fun a => ma a * mb a) f (𝓝 (a * b)) :=
show Tendsto ((fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) ∘ fun a => (ma a, mb a)) f (𝓝 (a * b)) from
Tendsto.comp (ENNReal.tendsto_mul ha hb) (hma.prodMk_nhds hmb)
