lt_toNNReal_iff_coe_lt

Mathlib.Data.NNReal.Defs

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

English

For n ≥ 2, toNNReal(r) < OfNat(n) iff r < OfNat(n).

Русский

Для n ≥ 2: toNNReal(r) < OfNat(n) ⇔ r < OfNat(n).

LaTeX

$$$$ \operatorname{toNNReal}(r) < \operatorname{OfNat}(n) \iff r < \operatorname{OfNat}(n). $$$$

Lean4

theorem lt_toNNReal_iff_coe_lt {r : ℝ≥0} {p : ℝ} : r < Real.toNNReal p ↔ ↑r < p :=
  lt_iff_lt_of_le_iff_le toNNReal_le_iff_le_coe

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

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

Разделы

Аффилиация

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