isBot_or_exists_lt — Mathlib

English

In a directed poset, every element is either bottom or has a smaller element.

Русский

В направленном частично упорядоченном множестве каждый элемент либо нижний, либо имеет меньший элемент.

LaTeX

$$$IsDirected(\alpha, \ge) \rightarrow (a) \Rightarrow IsBot(a) \lor \exists b, b < a$$$

Lean4

theorem isBot_or_exists_lt [IsDirected α (· ≥ ·)] (a : α) : IsBot a ∨ ∃ b, b < a :=
  @isTop_or_exists_gt αᵒᵈ _ _ a

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