coe_lt_one

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_lt_one

English

For r ∈ ℝ≥0, (r : ℝ) < 1 iff r < 1 in NNReal.

Русский

Для r ∈ ℝ≥0: (r : ℝ) < 1 ⇔ r < 1 в NNReal.

LaTeX

$$$(r : \mathbb{R}) < 1 \;\Leftrightarrow\; r < 1$$$

Lean4

@[simp, norm_cast]
theorem coe_lt_one : (r : ℝ) < 1 ↔ r < 1 := by rw [← coe_lt_coe, coe_one]

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

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

Разделы

Аффилиация

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