IsAtomic.of_isChain_bounded
theorem IsAtomic.of_isChain_bounded :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α],
(∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊥ ∉ c → ∃ x, x ≠ ⊥ ∧ x ∈ lowerBounds c) →
IsAtomic α
**Zorn's Lemma**: In the context of a partial order with a minimum element, a partial order is considered atomic if for every nonempty chain of elements `c` that does not include the minimum element, there exists a lower bound within the set of lower bounds of `c` that is not equal to the minimum element. This theorem states that if such a lower bound exists for every such chain, then the partial order is atomic.
More concisely: If every nonempty chain in a partial order lacking a minimum element has a least upper bound not equal to the minimum element, then the partial order is atomic.
|
IsCoatomic.of_isChain_bounded
theorem IsCoatomic.of_isChain_bounded :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α],
(∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c) →
IsCoatomic α
**Zorn's Lemma:** In the context of a partially ordered set (also known as poset), which also has a greatest element denoted by `⊤`, the poset is said to be coatomic if for every nonempty chain `c` that does not include `⊤`, there exists an upper bound within the set of upper bounds of `c` that is not equal to `⊤`. A chain is a subset of the poset where for any two elements, one must be less than or equal to the other. An upper bound of a set is an element that is greater than or equal to every element in the set.
More concisely: In a partially ordered set with a greatest element, if every non-empty chain lacking the greatest element has an upper bound that is not the greatest element, then the set is coatomic.
|