toNNReal_coe — Mathlib

English

On nonnegative reals, Real.toNNReal acts as the identity: Real.toNNReal r = r for r ∈ ℝ≥0.

Русский

На неотрицательных вещественных числах отображение Real.toNNReal является тождественным: Real.toNNReal r = r при r ∈ ℝ≥0.

LaTeX

$$$ \\operatorname{Real.toNNReal}(r) = r \\quad \\text{for } r \\in \\mathbb{R}_{\\ge 0}. $$$

Lean4

@[simp]
theorem _root_.Real.toNNReal_coe {r : ℝ≥0} : Real.toNNReal r = r :=
  NNReal.eq <| max_eq_left r.2

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