toNNReal_eq_iff_eq_coe — Mathlib

English

For real r and nonnegative p ≠ 0, r.toNNReal = p if and only if r = p.

Русский

Для действительного r и p ≥ 0, p ≠ 0: r.toNNReal = p ⇔ r = p.

LaTeX

$$$$ r \\in \\mathbb{R},\\ p \\in \\mathbb{R}_{\\ge 0},\\ p \\neq 0 \\Rightarrow r.toNNReal = p \\iff r = p. $$$$

Lean4

theorem toNNReal_eq_iff_eq_coe {r : ℝ} {p : ℝ≥0} (hp : p ≠ 0) : r.toNNReal = p ↔ r = p :=
  ⟨fun h ↦ h ▸ (coe_toNNReal _ <| not_lt.1 fun hlt ↦ hp <| h ▸ toNNReal_of_nonpos hlt.le).symm, fun h ↦
    h.symm ▸ toNNReal_coe⟩

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