ofNat_lt_toNNReal

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Real.ofNat_lt_toNNReal

English

For real r and nat n with [n.AtLeastTwo], ofNat(n) < r.toNNReal ↔ n < r.

Русский

Для r ∈ ℝ и n ∈ ℕ, [n.AtLeastTwo], ofNat(n) < r.toNNReal ⇔ n < r.

LaTeX

$$$$ \\operatorname{ofNat}(n) < r.toNNReal \\iff n < r, \\quad [n \\ge 2]. $$$$

Lean4

@[simp]
theorem ofNat_lt_toNNReal {r : ℝ} {n : ℕ} [n.AtLeastTwo] : ofNat(n) < r.toNNReal ↔ n < r :=
  natCast_lt_toNNReal

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

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

Разделы

Аффилиация

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