isSimpleOrder_iff_isAtom_top — Mathlib

English

In a bounded order, the order is simple if and only if the top element is an atom.

Русский

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

LaTeX

$$$\text{IsSimpleOrder}(\alpha) \iff \text{IsAtom}(\top_{\alpha})$$$

Lean4

theorem isSimpleOrder_iff_isAtom_top [PartialOrder α] [BoundedOrder α] : IsSimpleOrder α ↔ IsAtom (⊤ : α) :=
  ⟨fun h => @isAtom_top _ _ _ h, fun h =>
    { exists_pair_ne := ⟨⊤, ⊥, h.1⟩
      eq_bot_or_eq_top := fun a => ((eq_or_lt_of_le le_top).imp_right (h.2 a)).symm }⟩

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