instBoundedOrderElemOfOrderBot

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Iic.instBoundedOrderElemOfOrderBot

English

Iic(a) forms a bounded order whenever α is a preorder with top and bottom.

Русский

Iic(a) образует ограниченную упорядоченность при условии наличия верхнего и нижнего пределов в α.

LaTeX

$$$$\\text{BoundedOrder}(\\mathrm{Iic}(a)).$$$$

Lean4

instance [Preorder α] [OrderBot α] : BoundedOrder (Iic a) :=
  { Iic.orderTop, Iic.orderBot with }

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

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

Разделы

Аффилиация

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