mathlib documentation

order.zorn_atoms

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 .