instContinuousInv

Mathlib.Topology.Algebra.Ring.Real

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

English

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

Русский

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

LaTeX

$$$x \mapsto x^{-1}$ is continuous on ENNReal.$$

Lean4

instance : ContinuousInv ℝ≥0∞ :=
  ⟨OrderIso.invENNReal.continuous⟩

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

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

Разделы

Аффилиация

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