isSimpleOrder_iff_isCoatom_bot — Mathlib

English

A bounded order is simple if and only if the bottom is a coatom.

Русский

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

LaTeX

$$$\text{IsSimpleOrder}(\alpha) \iff \text{IsCoatom}(\bot) $$$

Lean4

theorem isSimpleOrder_iff_isCoatom_bot [PartialOrder α] [BoundedOrder α] : IsSimpleOrder α ↔ IsCoatom (⊥ : α) :=
  isSimpleOrder_iff_isSimpleOrder_orderDual.trans isSimpleOrder_iff_isAtom_top

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