toNNRat_lt_toNNRat_iff'

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.toNNRat_lt_toNNRat_iff'

English

For q ∈ ℚ≥0, q < toNNRat p iff q < p ∧ 0 < p.

Русский

Для q ∈ ℚ≥0, q < toNNRat p эквивалентно q < p и 0 < p.

LaTeX

$$$\mathrm{toNNRat}\,q < \mathrm{toNNRat}\,p \;\iff\; q < p \land 0 < p.$$$

Lean4

@[simp]
theorem toNNRat_lt_toNNRat_iff' : toNNRat q < toNNRat p ↔ q < p ∧ 0 < p := by simp [← coe_lt_coe, toNNRat]

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

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

Разделы

Аффилиация

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