instSemilatticeInf

Mathlib.Algebra.Order.Ring.Unbundled.Rat

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

English

The rationals form a semilattice with infimum (greatest lower bound) operation.

Русский

Рациональные числа образуют полуручку с операцией Inf (наибольшего нижнего

LaTeX

$$$(\\mathbb{Q}, \\le)$ is a semilatticeInf$$

Lean4

instance instSemilatticeInf : SemilatticeInf ℚ :=
  inferInstance

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

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

Разделы

Аффилиация

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