instCompleteLinearOrder

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#LowerSet.instCompleteLinearOrder

English

LowerSet α is equipped with a complete linear order structure, i.e., a complete lattice with linear order.

Русский

LowerSet α обладает полным линейным порядком, то есть полной решёткой.

LaTeX

$$$ \text{CompleteLinearOrder}(\text{LowerSet}(\alpha)) $$$

Lean4

noncomputable instance instCompleteLinearOrder : CompleteLinearOrder (LowerSet α) :=
  { completelyDistribLattice, instLinearOrder with }

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

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

Разделы

Аффилиация

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