toENNReal_mono — Mathlib

English

The map is monotone: if m ≤ n in ENat then (m) ≤ (n) in ENNReal.

Русский

Тождественно монотонно: если m ≤ n в ENat, то их образы в ENNReal удовлетворяют (m) ≤ (n).

LaTeX

$$$\\text{Monotone}(\\uparrow): m \\le n \\Rightarrow (m : \\mathbb{R}_{\\ge 0,\\infty}) \\le (n : \\mathbb{R}_{\\ge 0,\\infty}).$$$

Lean4

@[mono]
theorem toENNReal_mono : Monotone ((↑) : ℕ∞ → ℝ≥0∞) :=
  toENNRealOrderEmbedding.monotone

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