boundedOrder

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#Interval.boundedOrder

English

If α has a bounded order, then Interval α also has a bounded order.

Русский

Если у α есть ограниченный порядок, то и Interval α имеет ограниченный порядок.

LaTeX

$$$ \text{BoundedOrder}(\alpha) \Rightarrow \text{BoundedOrder}(\mathrm{Interval}(\alpha)) $$$

Lean4

instance boundedOrder : BoundedOrder (Interval α) :=
  WithBot.instBoundedOrder

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

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

Разделы

Аффилиация

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