toNNReal — Mathlib

English

There is a natural map from the unit interval I to the nonnegative reals NNReal given by sending i to the pair ⟨i.1, i.2.1⟩, i.e., the real coordinate together with its nonnegativity proof.

Русский

Существует естественное отображение от единичного интервала к множеству NNReal: i ↦ ⟨i.1, i.2.1⟩, то есть число i в ℝ и доказательство неотрицательности.

LaTeX

$$$toNNReal: I \\to \\mathbb{R}_{\\ge 0},\\quad toNNReal(i) = \\langle i.1, i.2.1 \\rangle$$$

Lean4

/-- The coercion from `I` to `ℝ≥0`. -/
def toNNReal : I → ℝ≥0 := fun i ↦ ⟨i.1, i.2.1⟩

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