English
Dually, a poset is atomic if every nonempty chain not containing bottom has a lower bound above bottom.
Русский
Дуально, частичный порядок атомарен, если любая непустая цепь, не содержащая низа, имеет нижнюю границу над нулем.
LaTeX
$$$$\text{IsAtomic } \alpha \iff \text{IsCoatomic } (\text{dual}(\alpha))$$$$
Lean4
/-- **Zorn's lemma**: A partial order is atomic if every nonempty chain `c`, `⊥ ∉ c`, has a lower
bound not equal to `⊥`. -/
theorem of_isChain_bounded {α : Type*} [PartialOrder α] [OrderBot α]
(h : ∀ c : Set α, IsChain (· ≤ ·) c → c.Nonempty → ⊥ ∉ c → ∃ x ≠ ⊥, x ∈ lowerBounds c) : IsAtomic α :=
isCoatomic_dual_iff_isAtomic.mp <| IsCoatomic.of_isChain_bounded fun c hc => h c hc.symm
