toENNReal_strictMono — Mathlib

English

The embedding is strictly monotone: m < n implies (m) < (n) in ENNReal.

Русский

Встраивание строго монотонно: если m < n, то образ m менее образа n в ENNReal.

LaTeX

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

Lean4

@[mono]
theorem toENNReal_strictMono : StrictMono ((↑) : ℕ∞ → ℝ≥0∞) :=
  toENNRealOrderEmbedding.strictMono

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