English
Symmetric to the previous lemma: for a fixed a, Tendsto of m to b implies Tendsto of a·m to a·b under suitable hypotheses.
Русский
Симметрично предыдущей лемме: при фиксированном a предел m→b влечет предел a·m→a·b при подходящих предположениях.
LaTeX
$$$\\forall a,b:\\; \\mathrm{Tendsto}\\ m\\ f (\\nhds b) \\Rightarrow (a \\neq ⊥ \\lor b \\neq 0) \\Rightarrow (a \\neq ⊤ \\lor b \\neq 0) \\Rightarrow \\mathrm{Tendsto}\\ (\\lambda x, a \\cdot m x)\\ f (\\nhds (a \\cdot b))$$$
Lean4
protected theorem mul_const {f : Filter α} {m : α → EReal} {a b : EReal} (hm : Tendsto m f (𝓝 a)) (h₁ : a ≠ 0 ∨ b ≠ ⊥)
(h₂ : a ≠ 0 ∨ b ≠ ⊤) : Tendsto (fun x ↦ m x * b) f (𝓝 (a * b)) := by
simpa only [mul_comm] using EReal.Tendsto.const_mul hm h₁.symm h₂.symm
