isTop

Mathlib.Order.Directed

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

English

If a is maximal in a directed poset, then it is a top element.

Русский

Если a максимум в направленном частично упорядоченном множестве, то он является верхней гранью.

LaTeX

$$[IsDirected α (≤)] ∧ IsMax a → IsTop a$$

Lean4

protected theorem isTop [IsDirected α (· ≤ ·)] (h : IsMax a) : IsTop a :=
  h.toDual.isBot

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

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

Разделы

Аффилиация

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