instNoMaxOrderElemIci

Mathlib.Order.Interval.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.instNoMaxOrderElemIci

English

If α has no maximal element, then the interval Ici(a) has no maximal element as well.

Русский

Если в порядке отсутствует максимальный элемент, то интервал Ici(a) не имеет максимального элемента.

LaTeX

$$$ \operatorname{NoMaxOrder}(\mathrm{Ici}(a)) $$$

Lean4

instance [NoMaxOrder α] : NoMaxOrder (Ici a) :=
  OrderDual.noMaxOrder (α := Iic (toDual a))

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

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

Разделы

Аффилиация

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