continuousAt_toReal

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

For x ≠ ∞, ENNReal.toReal is continuous at x.

Русский

Для x ≠ ∞ функця ENNReal.toReal непрерывна в точке x.

LaTeX

$$$\\operatorname{ContinuousAt} \\mathrm{ENNReal}.toReal x \\;\\text{ for } x \\neq \\infty$$$

Lean4

theorem continuousAt_toReal (hx : x ≠ ∞) : ContinuousAt ENNReal.toReal x :=
  continuousOn_toReal.continuousAt (isOpen_ne_top.mem_nhds_iff.mpr hx)

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

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

Разделы

Аффилиация

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