toNNReal_mono — Mathlib

English

If r1 ≤ r2 for real numbers, then r1.toNNReal ≤ r2.toNNReal.

Русский

Если r1 ≤ r2 для действительных чисел, то r1.toNNReal ≤ r2.toNNReal.

LaTeX

$$$ \\forall r_1,r_2 \\in \\mathbb{R}, \\; r_1 \\le r_2 \\Rightarrow \\operatorname{toNNReal}(r_1) \\le \\operatorname{toNNReal}(r_2). $$$

Lean4

@[gcongr]
protected theorem _root_.Real.toNNReal_mono {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) : r₁.toNNReal ≤ r₂.toNNReal :=
  Real.toNNReal_monotone h

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