English
There is a canonical map from EReal to ℝ, called toReal, which sends infinities to 0 and acts as the identity on real numbers.
Русский
Существует каноническое отображение from EReal в ℝ, названное toReal, которое отправляет бесконечности в 0 и действует как тождественное отображение на вещественных числах.
LaTeX
$$$\mathrm{toReal}: \mathrm{EReal} \to \mathbb{R},\quad \mathrm{toReal}(\bot)=0,\quad \mathrm{toReal}(\top)=0,\quad \mathrm{toReal}(r)=r\ (r\in\mathbb{R}).$$$
Lean4
/-- The map from extended reals to reals sending infinities to zero. -/
def toReal : EReal → ℝ
| ⊥ => 0
| ⊤ => 0
| (x : ℝ) => x
