one_lt_coe

Mathlib.Data.NNReal.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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