isTop_or_exists_gt — Mathlib

English

In a directed poset, every element is either top or has a greater element.

Русский

В направленной позиции каждый элемент либо верхний, либо имеет больший элемент.

LaTeX

$$$IsDirected(\alpha, \le) \rightarrow \forall a, IsTop(a) \lor \exists b, a < b$$$

Lean4

theorem isTop_or_exists_gt [IsDirected α (· ≤ ·)] (a : α) : IsTop a ∨ ∃ b, a < b :=
  (em (IsMax a)).imp IsMax.isTop not_isMax_iff.mp

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