canLift

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.canLift

English

There exists a canonical lift from ℚ to ℚ≥0 given by q ↦ ⟨q, proof that q ≥ 0⟩.

Русский

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

LaTeX

$$$i(q) = \langle q, q \ge 0 \rangle \quad \text{for all } q \in \mathbb{Q}$$$

Lean4

instance canLift : CanLift ℚ ℚ≥0 (↑) fun q ↦ 0 ≤ q where prf q hq := ⟨⟨q, hq⟩, rfl⟩

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

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

Разделы

Аффилиация

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