le_toNNRat_iff_coe_le

Mathlib.Data.NNRat.Defs

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

English

For q ≥ 0 and p ∈ ℚ, q ≤ toNNRat p iff ↑q ≤ p.

Русский

Для q ≥ 0 и p ∈ ℚ, q ≤ toNNRat p ⇔ ↑q ≤ p.

LaTeX

$$$q \le \operatorname{toNNRat}(p) \iff \uparrow q \le p \quad( q \in \mathbb{Q}_{\ge 0},\ p \in \mathbb{Q}).$$$

Lean4

theorem le_toNNRat_iff_coe_le {q : ℚ≥0} (hp : 0 ≤ p) : q ≤ toNNRat p ↔ ↑q ≤ p := by
  rw [← coe_le_coe, Rat.coe_toNNRat p hp]

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

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

Разделы

Аффилиация

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