toENNReal_inj — Mathlib

English

The coercion from ℕ∞ to ℝ≥0∞ is injective: if m and n have the same image in ℝ≥0∞, then m = n.

Русский

Коэрцировка из ℕ∞ в ℝ≥0∞ инъективна: если два элемента имеют одинаковый образ в ℝ≥0∞, то они равны.

LaTeX

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

Lean4

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

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