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 x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c) : IsCoatomic α

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 x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊥ ∈ c → ∃ x x_1, x ∈ lowerBounds c) : IsAtomic α

Zorn's lemma: A partial order is atomic if every nonempty chain c, ⊥ ∉ c, has a lower bound not equal to ⊥.