toNNReal_lt_natCast

Mathlib.Data.NNReal.Defs

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

English

r.toNNReal < n iff r < n, given n ≠ 0.

Русский

r.toNNReal < n ⇔ r < n, при n ≠ 0.

LaTeX

$$$$ r^{\mathrm{toNNReal}} < n \iff r < n. $$$$

Lean4

theorem toNNReal_lt_natCast {r : ℝ} {n : ℕ} (hn : n ≠ 0) : r.toNNReal < n ↔ r < n := by simp [hn]

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

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

Разделы

Аффилиация

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