le_coe_toNNRat

Mathlib.Data.NNRat.Defs

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

English

There exists a canonical embedding of ℚ into ℚ≥0 given by q ↦ ⟨q, q ≥ 0⟩.

Русский

Существует каноническое встраивание ℚ в ℚ≥0, задаваемое q ↦ ⟨q, q ≥ 0⟩.

LaTeX

$$$i(q) = \langle q, q \ge 0 \rangle$$$

Lean4

theorem _root_.Rat.le_coe_toNNRat (q : ℚ) : q ≤ q.toNNRat :=
  le_max_left _ _

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

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

Разделы

Аффилиация

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