to_noMinOrder

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#NoBotOrder.to_noMinOrder

← MathLib Explorer

English

In a linear order, NoBotOrder α implies NoMinOrder α.

Русский

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

LaTeX

$$$\text{NoBotOrder}(\alpha) \Rightarrow \text{NoMinOrder}(\alpha)$$$

Lean4

theorem to_noMinOrder (α : Type*) [LinearOrder α] [NoBotOrder α] : NoMinOrder α :=
  { exists_lt := fun a => by simpa [not_le] using exists_not_ge a }

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

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

Разделы

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

Аффилиация

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