le_toNNRat_iff_coe_le'

Mathlib.Data.NNRat.Defs

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

← MathLib Explorer

English

For q > 0, q ≤ toNNRat p ↔ ↑q ≤ p.

Русский

Для q > 0, q ≤ toNNRat p ⇔ ↑q ≤ p.

LaTeX

$$$q > 0 \Rightarrow q \le \operatorname{toNNRat}(p) \iff \uparrow q \le p.$$$

Lean4

theorem le_toNNRat_iff_coe_le' {q : ℚ≥0} (hq : 0 < q) : q ≤ toNNRat p ↔ ↑q ≤ p :=
  (le_or_gt 0 p).elim le_toNNRat_iff_coe_le fun hp ↦ by
    simp only [(hp.trans_le q.coe_nonneg).not_ge, toNNRat_eq_zero.2 hp.le, hq.not_ge]

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

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

Разделы

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

Аффилиация

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