instNoMaxOrderElemIoi

Mathlib.Order.Interval.Set.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

instance [NoMaxOrder α] : NoMaxOrder (Ioi a) :=
  OrderDual.noMaxOrder (α := Iio (toDual a))

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

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

Разделы

Аффилиация

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