isPredPrelimit

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#IsMax.isPredPrelimit

English

If a is maximal, then a is a predecessor-prelimit.

Русский

Если a максимален, то a является предпредлимитом.

LaTeX

$$$IsMax(a) \Rightarrow IsPredPrelimit(a)$$$

Lean4

protected theorem _root_.IsMax.isPredPrelimit : IsMax a → IsPredPrelimit a := fun h _ hab => not_isMax_of_lt hab.lt h

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

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

Разделы

Аффилиация

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