instPreorder

Mathlib.Algebra.Order.Ring.Unbundled.Rat

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

English

The rationals are endowed with a preorder relation, i.e., a reflexive and transitive relation ≤ on ℚ.

Русский

Рациональные числа имеют предорядок, то есть отношение ≤ на ℚ является рефлексивным и транзитивным.

LaTeX

$$$\\text{Preorder}(\\mathbb{Q}, \\le)$$$

Lean4

instance instPreorder : Preorder ℚ :=
  inferInstance

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

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

Разделы

Аффилиация

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