isMax_of_noMin

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsPredPrelimit.isMax_of_noMin

English

If there is no maximum, then IsPredPrelimit a fails.

Русский

Если максимума нет, IsPredPrelimit a ложна.

LaTeX

$$[NoMaxOrder α] ⇒ ¬ IsPredPrelimit a$$

Lean4

theorem isMax_of_noMin (h : IsPredPrelimit a) : IsMax a :=
  h.dual.isMin_of_noMax

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

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

Разделы

Аффилиация

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