natCast_le_toNNReal

Mathlib.Data.NNReal.Defs

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

English

↑n ≤ r.toNNReal ↔ n ≤ r, for n ≠ 0.

Русский

↑n ≤ r.toNNReal ↔ n ≤ r, при n ≠ 0.

LaTeX

$$$$ \uparrow n \le r^{\mathrm{toNNReal}} \iff n \le r. $$$$

Lean4

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

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

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

Разделы

Аффилиация

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