exists_lt_of_directed_ge — Mathlib

English

In a directed poset with a partial order, there exist a,b with a < b.

Русский

В направленном множество с частичным порядком существуют элементы a,b такие что a < b.

LaTeX

$$$\exists a,b \in \beta: a < b$$$

Lean4

theorem exists_lt_of_directed_ge [IsDirected β (· ≥ ·)] : ∃ a b : β, a < b :=
  by
  rcases exists_pair_ne β with ⟨a, b, hne⟩
  rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
  exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]

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