instContinuousInv₀

Mathlib.Topology.Algebra.Ring.Real

URI: https://scilib.ai/kg/mathlib#NNReal.instContinuousInv₀

English

The inversion map x \mapsto x^{-1} on ENNReal is continuous.

Русский

Обратная ENNReal непрерывна.

LaTeX

$$$x \mapsto x^{-1}$ is continuous on $\mathbb{R}_{\ge 0}^{\infty}$ (ENNReal).$$

Lean4

instance : ContinuousInv₀ ℝ≥0 :=
  inferInstance

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

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

Разделы

Аффилиация

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