cast_lt_one

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#NNRat.cast_lt_one

English

For p ∈ ℚ≥0, p.cast < 1 if and only if p < 1.

Русский

Для p ∈ ℚ≥0 верно: p.cast < 1 ⇔ p < 1.

LaTeX

$$$(p : K) < 1 \iff p < 1$$$

Lean4

@[simp]
theorem cast_lt_one : (p : K) < 1 ↔ p < 1 := by norm_cast

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

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

Разделы

Аффилиация

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