natCast_lt_ofReal

Mathlib.Data.ENNReal.Real

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

English

For natural n and real r, n < ENNReal.ofReal r iff n < r.

Русский

Для натурального n и действительного r: n < ENNReal.ofReal r тогда и только тогда, когда n < r.

LaTeX

$$ {n : ℕ} {r : ℝ} : n < ENNReal.ofReal r ↔ n < r $$

Lean4

@[simp]
theorem natCast_lt_ofReal {n : ℕ} {r : ℝ} : n < ENNReal.ofReal r ↔ n < r :=
  coe_lt_coe.trans Real.natCast_lt_toNNReal

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

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

Разделы

Аффилиация

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