English
If m tends to b and a ≠ ⊥ or b ≠ 0, and a ≠ ⊤ or b ≠ 0, then x ↦ a · m(x) tends to a · b.
Русский
Если m(x) стремится к b и выполняются условия a ≠ ⊥ или b ≠ 0, и a ≠ ⊤ или b ≠ 0, то x ↦ a·m(x) сходится к a·b.
LaTeX
$$$\\mathrm{Tendsto}\\ m\\ f\\ (\\nhds\\ b) \\Rightarrow \\text{(if } a \\neq \\bot \\lor b \\neq 0) \\land (a \\neq \\top \\lor b \\neq 0) \\Rightarrow \\mathrm{Tendsto}\\ (\\lambda x, a \\cdot m x)\\ f\\ (\\nhds (a \\cdot b))$$$
Lean4
protected theorem const_mul {f : Filter α} {m : α → EReal} {a b : EReal} (hm : Tendsto m f (𝓝 b)) (h₁ : a ≠ ⊥ ∨ b ≠ 0)
(h₂ : a ≠ ⊤ ∨ b ≠ 0) : Tendsto (fun b ↦ a * m b) f (𝓝 (a * b)) :=
by_cases (fun (this : a = 0) => by simp [this, tendsto_const_nhds]) fun ha : a ≠ 0 =>
EReal.Tendsto.mul tendsto_const_nhds hm (Or.inl ha) (Or.inl ha) h₁ h₂
