ofReal_eq_ofNat

Mathlib.Data.ENNReal.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.ofReal_eq_ofNat

English

For r ∈ ℝ and n ∈ ℕ with n ≥ 2, ENNReal.ofReal r = ofNat(n) iff r = n.

Русский

Для r ∈ ℝ и n ∈ ℕ, n ≥ 2: ENNReal.ofReal r = ofNat(n) тогда и только если r = n.

LaTeX

$$$ ENNReal.ofReal r = ofNat(n) \iff r = n.cast $$$

Lean4

@[simp]
theorem ofReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] : ENNReal.ofReal r = ofNat(n) ↔ r = OfNat.ofNat n :=
  ofReal_eq_natCast (NeZero.ne n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru