sub_def

Mathlib.Data.NNRat.Defs

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

English

For p,q in ℚ≥0, p − q equals the nonnegative representation of the difference: p − q = toNNRat(p − q).

Русский

Для p,q ∈ ℚ≥0 разность p − q равна отображению toNNRat от разности: p − q = toNNRat(p − q).

LaTeX

$$$p - q = \operatorname{toNNRat}(p - q)\quad( p,q \in \mathbb{Q}_{\ge 0}).$$$

Lean4

theorem sub_def (p q : ℚ≥0) : p - q = toNNRat (p - q) :=
  rfl

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

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

Разделы

Аффилиация

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