toENNReal_le — Mathlib

English

The embedding from ℕ∞ to ℝ≥0∞ is order-preserving: m ≤ n in ENat iff their images satisfy (m:ℝ≥0∞) ≤ (n:ℝ≥0∞).

Русский

Встраивание сохраняет порядок: m ≤ n в ENat эквивалентно их образам в ENNReal: (m) ≤ (n).

LaTeX

$$$(m : \\mathbb{R}_{\\ge 0,\\infty}) \\le n \\iff m \\le n.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_le : (m : ℝ≥0∞) ≤ n ↔ m ≤ n :=
  toENNRealOrderEmbedding.le_iff_le

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