denselyOrdered

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.denselyOrdered

English

WithBot α is densely ordered when α is densely ordered and NoMinOrder α, given LT.

Русский

WithBot α плотно упорядочен, когда α плотно упорядочен и NoMinOrder α, при LT.

LaTeX

$$$DenselyOrdered(WithBot \alpha)$$$

Lean4

instance denselyOrdered [LT α] [DenselyOrdered α] [NoMinOrder α] : DenselyOrdered (WithBot α) :=
  denselyOrdered_iff.mpr inferInstance

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

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

Разделы

Аффилиация

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