toENNReal_zero

Mathlib.Data.Real.ENatENNReal

URI: https://scilib.ai/kg/mathlib#ENat.toENNReal_zero

English

The image of zero is zero: 0 in ENnat∞ maps to 0 in ENNReal.

Русский

Образ нуля равен нулю: 0 в ENnat∞ переходит в 0 в ENNReal.

LaTeX

$$$((0 : \\mathbb{N}_\\infty) : \\mathbb{R}_{\\ge 0,\\infty}) = 0.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_zero : ((0 : ℕ∞) : ℝ≥0∞) = 0 :=
  map_zero toENNRealRingHom

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

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

Разделы

Аффилиация

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