isMax

Mathlib.Order.SuccPred.Limit

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

English

If a is a predecessor-prelimit, then a is a maximum element.

Русский

Если a является предшественник-предпредельным, то это максимальный элемент.

LaTeX

$$$IsPredPrelimit\\ a \\to IsMax\\ a$$$

Lean4

protected theorem isMax (h : IsPredPrelimit a) : IsMax a :=
  h.dual.isMin

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

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

Разделы

Аффилиация

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