coe_toNNReal_eq_toReal

Mathlib.Data.ENNReal.Basic

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

English

For z ∈ ENNReal, (z.toNNReal : ℝ) = z.toReal.

Русский

Для z ∈ ENNReal, (z.toNNReal : ℝ) = z.toReal.

LaTeX

$$$ (z.toNNReal : \mathbb{R}) = z.toReal $$$

Lean4

@[norm_cast]
theorem coe_toNNReal_eq_toReal (z : ℝ≥0∞) : (z.toNNReal : ℝ) = z.toReal :=
  rfl

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

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

Разделы

Аффилиация

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