toNNRat_lt_toNNRat_iff

Mathlib.Data.NNRat.Defs

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

English

If 0 < p, then toNNRat q < toNNRat p iff q < p.

Русский

Если 0 < p, то toNNRat q < toNNRat p эквивалентно q < p.

LaTeX

$$$0 < p \Rightarrow toNNRat(q) < toNNRat(p) \iff q < p.$$$

Lean4

theorem toNNRat_lt_toNNRat_iff (h : 0 < p) : toNNRat q < toNNRat p ↔ q < p :=
  toNNRat_lt_toNNRat_iff'.trans (and_iff_left h)

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

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

Разделы

Аффилиация

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