Zorn lemma for (co)atoms #
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
IsCoatomic.of_isChain_bounded
{α : Type u_1}
[PartialOrder α]
[OrderTop α]
(h :
∀ (c : Set α),
IsChain (fun (x1 x2 : α) => LE.le x1 x2) c →
c.Nonempty →
Not (Membership.mem c Top.top) → Exists fun (x : α) => And (Ne x Top.top) (Membership.mem (upperBounds c) x))
:
Zorn's lemma: A partial order is coatomic if every nonempty chain c, ⊤ ∉ c, has an upper
bound not equal to ⊤.
theorem
IsAtomic.of_isChain_bounded
{α : Type u_1}
[PartialOrder α]
[OrderBot α]
(h :
∀ (c : Set α),
IsChain (fun (x1 x2 : α) => LE.le x1 x2) c →
c.Nonempty →
Not (Membership.mem c Bot.bot) → Exists fun (x : α) => And (Ne x Bot.bot) (Membership.mem (lowerBounds c) x))
:
IsAtomic α
Zorn's lemma: A partial order is atomic if every nonempty chain c, ⊥ ∉ c, has a lower
bound not equal to ⊥.