toNNReal_eq_ofNat — Mathlib

English

For Real r and Nat n with [n.AtLeastTwo], r.toNNReal = ofNat(n) iff r = ofNat(n).

Русский

Для r ∈ ℝ и n ∈ ℕ с условием [n.AtLeastTwo], r.toNNReal = ofNat(n) ⇔ r = ofNat(n).

LaTeX

$$$$ r.toNNReal = \\operatorname{ofNat}(n) \\iff r = \\operatorname{ofNat}(n), \\quad [n \\text{ AtLeastTwo}]. $$$$

Lean4

@[simp]
theorem toNNReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] : r.toNNReal = ofNat(n) ↔ r = OfNat.ofNat n :=
  toNNReal_eq_natCast (NeZero.ne n)

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