lt_toNNRat_iff_coe_lt

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.lt_toNNRat_iff_coe_lt

English

For q ∈ ℚ≥0, q < toNNRat p ↔ ↑q < p.

Русский

Для q ∈ ℚ≥0, q < toNNRat p ↔ ↑q < p.

LaTeX

$$$q < toNNRat p \iff \uparrow q < p.$$$

Lean4

theorem lt_toNNRat_iff_coe_lt {q : ℚ≥0} : q < toNNRat p ↔ ↑q < p :=
  NNRat.gi.gc.lt_iff_lt

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

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

Разделы

Аффилиация

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