continuousAt_const_mul — Mathlib

English

If a ≠ ∞ or b ≠ 0, then the map x ↦ a · x is continuous at x = b.

Русский

Если a не бесконечно, либо b не равен 0, отображение x ↦ a · x непрерывно в точке x = b.

LaTeX

$$$\\\\forall {a b : ENNReal}, (a \\\\neq \\\\infty \\\\lor b \\\\neq 0) \\\\Rightarrow \\\\text{ContinuousAt } (\\\\lambda x, a * x) \\\\ b.$$$

Lean4

protected theorem continuousAt_const_mul {a b : ℝ≥0∞} (h : a ≠ ∞ ∨ b ≠ 0) : ContinuousAt (a * ·) b :=
  Tendsto.const_mul tendsto_id h.symm

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