to_noMaxOrder

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#NoTopOrder.to_noMaxOrder

← MathLib Explorer

English

In a linear order, NoTopOrder α implies NoMaxOrder α.

Русский

В линейном порядке отсутствие верхнего элемента приводит к отсутствию максимума.

LaTeX

$$$\text{NoTopOrder}(\alpha) \Rightarrow \text{NoMaxOrder}(\alpha)$$$

Lean4

theorem to_noMaxOrder (α : Type*) [LinearOrder α] [NoTopOrder α] : NoMaxOrder α :=
  { exists_gt := fun a => by simpa [not_le] using exists_not_le a }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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