toNNRat_le_iff_le_coe

Mathlib.Data.NNRat.Defs

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

English

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

Русский

Для p ∈ ℚ≥0, q ∈ ℚ имеет место toNNRat q ≤ p ⇔ q ≤ ↑p.

LaTeX

$$$q \le \operatorname{toNNRat}(p) \iff q \le p\;\text{(in }\mathbb{Q}).$$$

Lean4

theorem toNNRat_le_iff_le_coe {p : ℚ≥0} : toNNRat q ≤ p ↔ q ≤ ↑p :=
  NNRat.gi.gc q p

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

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

Разделы

Аффилиация

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