instCompleteLinearOrder

Mathlib.Order.UpperLower.CompleteLattice

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

English

UpperSet α carries a complete linear order structure, i.e., a complete lattice whose order is linear.

Русский

UpperSet α образует полную линейную решётку; порядок линейный и полон.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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