Zorn lemma for (co)atoms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we use Zorn's lemma to prove that a partial order is atomic if every nonempty chain
c, ⊥ ∉ c, has a lower bound not equal to ⊥. We also prove the order dual version of this
statement.
theorem
is_coatomic.of_is_chain_bounded
{α : Type u_1}
[partial_order α]
[order_top α]
(h : ∀ (c : set α), is_chain has_le.le c → c.nonempty → ⊤ ∉ c → (∃ (x : α) (H : x ≠ ⊤), x ∈ upper_bounds c)) :
Zorn's lemma: A partial order is coatomic if every nonempty chain c, ⊤ ∉ c, has an upper
bound not equal to ⊤.
theorem
is_atomic.of_is_chain_bounded
{α : Type u_1}
[partial_order α]
[order_bot α]
(h : ∀ (c : set α), is_chain has_le.le c → c.nonempty → ⊥ ∉ c → (∃ (x : α) (H : x ≠ ⊥), x ∈ lower_bounds c)) :
Zorn's lemma: A partial order is atomic if every nonempty chain c, ⊥ ∉ c, has an lower
bound not equal to ⊥.