instOrderedSub

Mathlib.Data.NNRat.Order

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

English

The nonnegative rationals ℚ≥0 carry an OrderedSub structure compatible with the usual order.

Русский

У ℚ≥0 задана структура упорядоченного вычитания, совместимая с обычным порядком.

LaTeX

$$$\\operatorname{OrderedSub} (\\\\mathbb{Q}_{\\\\ge 0}).$$$

Lean4

instance instOrderedSub : OrderedSub ℚ≥0 :=
  Nonneg.orderedSub

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

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

Разделы

Аффилиация

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