noTopOrder_iff_noMaxOrder

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#noTopOrder_iff_noMaxOrder

← MathLib Explorer

English

For linear orders, NoTopOrder α is equivalent to NoMaxOrder α.

Русский

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

LaTeX

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

Lean4

theorem noTopOrder_iff_noMaxOrder (α : Type*) [LinearOrder α] : NoTopOrder α ↔ NoMaxOrder α :=
  ⟨fun _ => NoTopOrder.to_noMaxOrder α, fun _ => inferInstance⟩

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

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

Разделы

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

Аффилиация

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