toEReal — Mathlib

English

There is a canonical embedding Real → EReal, preserving order and structure.

Русский

Существует каноническое вложение Real в EReal, сохраняющее порядок и структуру.

LaTeX

$$$ \exists i:\mathbb{R} \to \mathrm{EReal},\; i \\text{ is injective and order-preserving}. $$$

Lean4

/-- The canonical inclusion from reals to ereals. Registered as a coercion. -/
@[coe]
def toEReal : ℝ → EReal :=
  WithBot.some ∘ WithTop.some

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