toReal

Mathlib.Data.ENNReal.Basic

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

English

The toReal map is defined by taking the NNReal part of ENNReal, i.e., toReal(a) = a.toNNReal.

Русский

Функция toReal определяется как взятие части NNReal у ENNReal, то есть toReal(a) = a.toNNReal.

LaTeX

$$$\operatorname{toReal}(a) = a^{\mathrm{toNNReal}}$$$

Lean4

/-- `toReal x` returns `x` if it is real, `0` otherwise. -/
protected def toReal (a : ℝ≥0∞) : Real :=
  a.toNNReal

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

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

Разделы

Аффилиация

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