mul_const — Mathlib

English

If a and b are ENNReal, and not both infinite, then Tendsto (λ p, p.1 - p.2) (nhds {fst:=a, snd:=b}) (nhds (a-b)).

Русский

Если пары (a,b) в ENNReal не обе бесконечны, то отображение (x,y) ↦ x − y непрерывно в точке (a,b).

LaTeX

$$$\\\\forall {a,b : ENNReal}, (a ≠ ∞ \\\\lor b ≠ ∞) \\\\Rightarrow \\\\mathrm{Tendsto} (\\\\lambda p: ENNReal \\times ENNReal, p.1 - p.2) (\\\\nhds (\\\\langle a,b \\\\rangle)) (\\\\nhds (a-b)).$$$

Lean4

protected theorem mul_const {f : Filter α} {m : α → ℝ≥0∞} {a b : ℝ≥0∞} (hm : Tendsto m f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ∞) :
    Tendsto (fun x => m x * b) f (𝓝 (a * b)) := by simpa only [mul_comm] using ENNReal.Tendsto.const_mul hm ha

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