cast_lt_ofNat

Mathlib.Data.Rat.Cast.Order

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

English

For p ∈ ℚ≥0 and n ≥ 2, the strict inequality (p : K) < ofNat(n) in K is equivalent to p < OfNat.ofNat n in ℚ≥0.

Русский

Для p ∈ ℚ≥0 и n ≥ 2: (p : K) < ofNat(n) в K эквивалентно p < OfNat.ofNat n в ℚ≥0.

LaTeX

$$$(p : K) < \operatorname{ofNat}(n) \iff p < \operatorname{OfNat}.ofNat(n)$$$

Lean4

@[simp]
theorem cast_lt_ofNat : (p : K) < ofNat(n) ↔ p < OfNat.ofNat n := by simp [← cast_lt (K := K)]

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

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

Разделы

Аффилиация

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