continuousAt_mul_const

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.continuousAt_mul_const

English

If a ≠ ∞, then the map x ↦ a · x is continuous at every x.

Русский

Если a ≠ ∞, отображение x ↦ a · x непрерывно в каждой точке.

LaTeX

$$$\\\\forall a b, a \\\\neq ∞ \\\\Rightarrow \\\\text{ContinuousAt } (\\\\lambda x, a * x) \\\\ b.$$$

Lean4

protected theorem continuousAt_mul_const {a b : ℝ≥0∞} (h : a ≠ ∞ ∨ b ≠ 0) : ContinuousAt (fun x => x * a) b :=
  Tendsto.mul_const tendsto_id h.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru