instDenselyOrderedOfNoMaxOrder

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.instDenselyOrderedOfNoMaxOrder

English

If α is LT, densely ordered, and NoMaxOrder, then WithTop α is densely ordered.

Русский

Если α обладает LT, плотностью и NoMaxOrder, то WithTop α плотен.

LaTeX

$$$\\operatorname{DenselyOrdered}(\\mathrm{WithTop}\\,\\alpha)$ given LT α, densely ordered and NoMaxOrder α.$$

Lean4

instance [LT α] [DenselyOrdered α] [NoMaxOrder α] : DenselyOrdered (WithTop α) :=
  denselyOrdered_iff.mpr inferInstance

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

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

Разделы

Аффилиация

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