toNNReal_monotone — Mathlib

English

The map Real.toNNReal from real numbers to NNReal is order-preserving: if r1 ≤ r2, then Real.toNNReal(r1) ≤ Real.toNNReal(r2).

Русский

Отображение Real.toNNReal из действительных чисел в ℝ≥0 сохраняет порядок: если r1 ≤ r2, то Real.toNNReal(r1) ≤ Real.toNNReal(r2).

LaTeX

$$$ \\forall a,b \\in \\mathbb{R}, a \\le b \\Rightarrow \\operatorname{toNNReal}(a) \\le \\operatorname{toNNReal}(b). $$$

Lean4

protected theorem _root_.Real.toNNReal_monotone : Monotone Real.toNNReal := fun _ _ h => max_le_max_right _ h

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