exists_atom — Mathlib

English

In any nontrivial order with a bottom element that is atomic, there exists an atom.

Русский

В любой ненулевой частично упорядоченной множестве с нулём, которая атомарна, существует атом.

LaTeX

$$$ \exists a : \alpha, IsAtom a $$$

Lean4

theorem exists_atom [OrderBot α] [Nontrivial α] [IsAtomic α] : ∃ a : α, IsAtom a :=
  have ⟨b, hb⟩ := exists_ne (⊥ : α)
  have ⟨a, ha⟩ := (eq_bot_or_exists_atom_le b).resolve_left hb
  ⟨a, ha.1⟩

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