isTop_iff_isMax

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#isTop_iff_isMax

English

Top is equivalent to maximal element in a directed poset.

Русский

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

LaTeX

$$$IsTop a \leftrightarrow IsMax a$$$

Lean4

theorem isTop_iff_isMax [IsDirected α (· ≤ ·)] : IsTop a ↔ IsMax a :=
  ⟨IsTop.isMax, IsMax.isTop⟩

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

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

Разделы

Аффилиация

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