exists_maximal_of_chains_bounded
theorem exists_maximal_of_chains_bounded :
∀ {α : Type u_1} {r : α → α → Prop},
(∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub) →
(∀ {a b c : α}, r a b → r b c → r a c) → ∃ m, ∀ (a : α), r m a → r a m
**Zorn's Lemma**
Given a type `α` and a binary relation `r` on `α`, if every chain (a set `c` of elements from `α` where for any two elements `x` and `y` in the set, `x` is related to `y` or `y` is related to `x` via `r`) has an upper bound (an element `ub` such that for every element `a` in the chain, `a` is related to `ub` via `r`), and if `r` is transitive (for any three elements `a`, `b`, and `c` from `α`, if `a` is related to `b` and `b` is related to `c`, then `a` is related to `c`), then there exists a maximal element `m` (an element such that for any element `a` from `α`, if `m` is related to `a`, then `a` is also related to `m`).
More concisely: If every chain in a partially ordered set has an upper bound and the relation is transitive, then the set has a maximal element.
|
exists_maximal_of_nonempty_chains_bounded
theorem exists_maximal_of_nonempty_chains_bounded :
∀ {α : Type u_1} {r : α → α → Prop} [inst : Nonempty α],
(∀ (c : Set α), IsChain r c → c.Nonempty → ∃ ub, ∀ a ∈ c, r a ub) →
(∀ {a b c : α}, r a b → r b c → r a c) → ∃ m, ∀ (a : α), r m a → r a m
This theorem is a variant of Zorn's lemma. It states that for any nonempty type `α` with a relation `r`, if every nonempty chain of elements in `α` under this relation has an upper bound, and the relation `r` is transitive, then there exists a maximal element `m` in `α` under relation `r`. Here, an element `m` is considered maximal if for any element `a` in `α`, if `r m a` holds then `r a m` also holds. In other words, `m` is equal to or greater than every other element under the relation `r`.
More concisely: If every chain in a nonempty type, equipped with a transitive relation having an upper bound for each nonempty chain, has a greatest element.
|
zorn_nonempty_partialOrder₀
theorem zorn_nonempty_partialOrder₀ :
∀ {α : Type u_1} [inst : PartialOrder α] (s : Set α),
(∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) →
∀ x ∈ s, ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m
This theorem, known as Zorn's Lemma, states that for any type `α` equipped with a partial order, given a set `s` of elements of this type, if every chain in `s` (a chain being defined as a set where for all `x` and `y` in it, either `x` is less than or equal to `y` or `y` is less than or equal to `x`) has an upper bound in `s`, then for every element `x` in `s`, there exists a maximal element `m` in `s`. This maximal element `m` has two properties: `x` is less than or equal to `m`, and if there exists any `z` in `s` such that `m` is less than or equal to `z`, then `z` must equal `m`. In other words, there is no element in `s` strictly greater than `m`.
More concisely: If every chain in a partially ordered set has an upper bound, then the set has a maximal element.
|
IsChain.exists_maxChain
theorem IsChain.exists_maxChain :
∀ {α : Type u_1} {r : α → α → Prop} {c : Set α}, IsChain r c → ∃ M, IsMaxChain r M ∧ c ⊆ M
This theorem states that for any type `α` and for any relation `r` on `α`, given a chain `c` (a set of elements of `α` where for any two elements `x` and `y` in `c`, either `x` is related to `y`, `y` is related to `x`, or they are equal), there exists a maximal chain `M` (a chain that can't be strictly included in any other chain) such that `c` is a subset of `M`. This is a generalization of Hausdorff's maximality principle.
More concisely: For any type `α` and relation `r` on `α`, if `c` is a chain (a subset of `α` where every two elements are related or equal), then there exists a maximal chain `M` that contains `c`.
|
zorn_nonempty_partialOrder
theorem zorn_nonempty_partialOrder :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Nonempty α],
(∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → BddAbove c) → ∃ m, ∀ (a : α), m ≤ a → a = m
The theorem `zorn_nonempty_partialOrder` states that for any type `α`, given a partial order on `α` and the assumption that `α` is not empty, if every chain in `α` (a chain being a set where for any two elements `x` and `y`, either `x ≤ y` or `y ≤ x`) that is non-empty is bounded above, then there exists an element `m` in `α` such that for all other elements `a` in `α`, if `m ≤ a` then `a` must be equal to `m`. Essentially, this is a formulation of Zorn's Lemma, a foundational result in set theory and abstract algebra. It indicates that in certain structures, every chain has an upper bound.
More concisely: If every non-empty chain in a partially ordered set has an upper bound, then the set has a greatest element.
|