ofNat_lt_cast

Mathlib.Data.Rat.Cast.Order

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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