toNNRat_lt_toNNRat_iff_of_nonneg

Mathlib.Data.NNRat.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem toNNRat_lt_toNNRat_iff_of_nonneg (hq : 0 ≤ q) : toNNRat q < toNNRat p ↔ q < p :=
  toNNRat_lt_toNNRat_iff'.trans ⟨And.left, fun h ↦ ⟨h, hq.trans_lt h⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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