nyuuzyou/wikis huggingface dataset:
Order-Extension Principle/Proof 1

== Theorem ==
== Proof ==
Let $\preceq$ be an ordering on the set $S$.
If $\preceq$ is a total ordering, the result is complete.
Suppose, then, that $\preceq$ is not a total ordering.
Let $\TT$ be the set of orderings on $S$ that extend $\preceq$, ordered by inclusion.
Let $C$ be a chain in $T$.
By Union of Chain of Orderings is Ordering, $\bigcup C$ is an ordering.
Thus every chain in $\TT$ has an upper bound in $\TT$.
By Zorn's Lemma, $\TT$ has a maximal element, $\RR$.
$\RR$ is seen to be the total ordering whose existence is to be demonstrated, as follows:
Suppose that:
:$\exists a, b \in S: \tuple {a, b} \notin \RR \land \tuple {b, a} \notin \RR$
Let $\RR'$ be the relation defined as:
:$\RR' := \RR \cup \set {\tuple {a, b} }$
Let $\RR'^-$ be the transitive closure of $\RR'$.
Then by Partial Ordering can be Expanded to compare Additional Pair, $\RR'^-$ is an ordering.
But $\RR'^- \supsetneq \RR$, contradicting the maximality of $\RR$.
Thus, $\RR$ is a total ordering.
Category:Order-Extension Principle
Order-Extension Principle/Proof 2

== Theorem ==
== Proof ==
Let $\prec$ be the reflexive reduction of $\preceq$.
By Reflexive Reduction of Ordering is Strict Ordering, $\prec$ is a strict ordering.
By the strict form of the Order-Extension Principle, there exists a strict total ordering $<$ on $S$ such that:
:$\forall a, b \in S: \paren {a \prec b \implies a < b}$
Let $\le$ be the reflexive closure of $<$.
Let $a, b \in S$.
If $a \preceq b$, then by Law of Excluded Middle either $a \prec b$ or $a = b$.
If $a = b$, then by the definition of reflexive closure, $a \le b$.
If $a \prec b$, then by the choice of $<$, $a < b$ so $a \le b$.
Thus for all $a, b \in S$, $a \preceq b \implies a < b$.
By Reflexive Closure of Strict Total Ordering is Total Ordering, $\le$ is a total ordering.
Category:Order-Extension Principle
Order-Extension Principle/Strict

== Theorem ==
Let $S$ be a set.
Let $\prec$ be a strict ordering on $S$.
Then there exists a strict total ordering $<$ on $S$ such that:
:$\forall a, b \in S: a \prec b \implies a < b$
=== Finite Set ===
== Proof 1 ==
== Proof 2 ==
Category:Set Theory
Category:Order Theory
Order-Extension Principle/Strict/Finite Set

== Theorem ==
Let $T$ be a finite set.
Let $\prec$ be a strict ordering on $T$.
Then there exists a strict total ordering $<$ on $T$ such that:
:$\forall a, b \in T: \paren {a \prec b \implies a < b}$
== Proof ==
Category:Set Theory
Category:Order Theory
Order-Extension Principle/Strict/Proof 1

== Theorem ==
== Proof ==
Let $\AA$ be the set of relations $A$ on $S$ with the property that the transitive closure $A^+$ of $A$ is a strict ordering of $S$.
For each $\tuple {x, y} \in S \times S$, let $\tuple {x, y}' = \tuple {y, x}$.
Let $A \in \AA$.
Let $\tuple {x, y} \in S \times S$.
Let $\tuple {x, y} \in A^+$.
Then:
:$\paren {A \cup \set {\tuple {x, y} } }^+ = A^+$
so:
:$A \cup \set {\tuple {x, y} } \in \AA$
Let $\tuple {y, x} \in A^+$.
Then:
:$\paren {A \cup \set {\tuple {y, x} } }^+ = A^+$
so:
:$A \cup \set {\tuple {x, y}'} = A \cup \set {\tuple {y, x} } \in \AA$
Otherwise, $x$ and $y$ are non-comparable by $A^+$.
So by Strict Ordering can be Expanded to Compare Additional Pair:
:$A \cup \set {\tuple {x, y} } \in \AA$
Thus it has been shown that for each $A \in \AA$ and each $\tuple {x, y} \in S$, either:
:$A \cup \set {\tuple {x, y} } \in \AA$
or:
:$A \cup \set {\tuple {x, y}'} \in \AA$
Let $A \subseteq S \times S$.
Let $A \in \AA$.
Let $F$ be a finite subset of $A$.
Since $A^+$ is a strict ordering, it is asymmetric.
Since Transitive Closure is Closure Operator, $F^+ \subseteq A^+$.
So $F^+$ is also asymmetric.
Since $F^+$ is also transitive, it is a strict ordering.
So $F \in \AA$.
Suppose instead that each finite subset of $A$ is in $\AA$.
We must show that $A^+$ is antireflexive.
 that for some $x \in S$, $\tuple {x, x} \in A^+$.
Then by the definition of transitive closure, there are elements $y_0, \dots, y_n$ such that $x = y_0 = y_n$ and:
:$\tuple {y_0, y_1}, \tuple {y_1, y_2}, \dotsc, \tuple {y_{n - 1}, y_n} \in A$
Let $F = \set {\tuple {y_0, y_1}, \tuple {y_1, y_2}, \dotsc, \tuple {y_{n - 1}, y_n} }$.
Then $F$ is a finite subset of $A$.
But $\tuple {x, x} \in F^+$, contradicting the fact that $F \in \AA$.
Thus we see that $A^+$ is antireflexive, and thus a strict ordering of $S$.
Therefore, $\AA$ has finite character.
Note that ${\prec} = {\prec^+}$, so ${\prec} \in \AA$.
By the Restricted Tukey's Theorem (Strong Form), there exists an $R \in \AA$ such that:
:${\prec} \subseteq R$
:For each $\tuple {m, n} \in S \times S$, either $\tuple {m, n} \in R$ or $\tuple {n, m} = \tuple {m, n}' \in R$.
Then:
:$R^+$ is a strict total ordering of $S$.
:$\forall a, b \in S: a \prec b \implies a < b$
Category:Set Theory
Category:Order Theory
Order-Preserving Bijection on Wosets is Order Isomorphism

== Theorem ==
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be well-ordered sets.
Let $\phi: S \to T$ be a bijection such that $\phi: S \to T$ is order-preserving:
:$\forall x, y \in S: x \preceq_1 y \implies \map \phi x \preceq_2 \map \phi y$
Then:
:$\forall x, y \in S: \map \phi x \preceq_2 \map \phi y \implies x \preceq_1 y$
That is, $\phi: S \to T$ is an order isomorphism.
== Proof ==
A well-ordered set is a totally ordered set by definition.
A bijection is a surjection by definition.
The result follows from Order Isomorphism iff Strictly Increasing Surjection.
Category:Well-Orderings
Category:Order Isomorphisms
Order-Preserving Identity Mapping between Ordered Structures not necessarily Isomorphism

== Theorem ==
Let $A$ be a set.
Let $\RR$ and $\SS$ be orderings on $A$ such that:
:$\forall a, b \in A: a \mathrel \RR b \implies a \mathrel \SS b$
Let $I_A$ denote the identity mapping on $A$.
Then it is not necessarily the case that $I_A$ is an order isomorphism from the ordered structures $\struct {A, \RR}$ and $\struct {A, \SS}$.
== Proof ==
Proof by Counterexample
Let $\RR: \N \to \N$ be the ordering on the natural numbers $\N$ defined as:
:$\forall a, b \in \N: a \mathrel \RR b \iff a \le b \text { and } \map P a = \map P b$
where $\map P x$ is the parity of $x$.
That is:
:$0 \mathrel \RR 2 \mathrel \RR 4 \mathrel \RR \cdots$
and:
:$1 \mathrel \RR 3 \mathrel \RR 5 \mathrel \RR \cdots$
and so on, but (for example):
:$\lnot \paren {0 \mathrel \RR 1}$
Let $\SS: \N \to \N$ be the ordering on the natural numbers $\N$ defined as:
:$\forall a, b \in \N: a \mathrel \SS b \iff a \le b$
We have that:
But note that:
while it is not the case that $0 \mathrel \RR 1$.
Hence while it is true that:
:$\forall a, b \in \N: a \mathrel \RR b \implies a \mathrel \SS b$
it is not the case that:
:$\forall a, b \in \N: a \mathrel \SS b \implies a \mathrel \RR b$
and so the identity mapping on $\NN$ is not an order isomorphism.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Exercise $14.9 \ \text{(d)}$
Category:Ordered Structures
Category:Order Isomorphisms
Order-Preserving Mapping Not Always Semilattice Homomorphism

== Theorem ==
Let $\struct {S, \circ}$ and $\struct {T, *}$ be semilattices.
Let $\preceq_1$ be the ordering on $S$ defined by:
:$a \preceq_1 b \iff \paren {a \circ b} = b$
Let $\preceq_2$ be the ordering on $T$ defined by:
:$x \preceq_2 y \iff \paren {x * y} = y$
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be an order-preserving mapping.
Then:
:$\phi: \struct {S, \circ} \to \struct {T, *}$ may not be a semilattice homomorphism
== Proof ==
Let $S = \set {a, b, c}$.
Let $\circ : S \times S \to S$ be defined by:
:$a \circ b = b \circ a = c$
:$a \circ c = c \circ a = c$
:$b \circ c = c \circ b = c$
:$a \circ a = a$
:$b \circ b = b$
:$c \circ c = c$
Then a manual check shows that $\circ$ is:
:closed
:associative
:commutative
:idempotent
So $\struct {S, \circ}$ is a semilattice with ordering:
:$\preceq_1 = \set {\tuple {a, a}, \tuple {b, b}, \tuple {c, c}, \tuple {a, c}, \tuple {b, c} }$
Let $T = \set{p, q, r, s}$.
Let $* : S \times S \to S$ be defined by:
:$p * q = q * p = r$
:$p * r = r * p = r$
:$q * r = r * q = r$
:$p * s = s * p = s$
:$q * s = s * q = s$
:$r * s = s * r = s$
:$p * p = p$
:$q * q = q$
:$r * r = r$
:$s * s = s$
Then a manual check shows that $*$ is:
:closed
:associative
:commutative
:idempotent
So $\struct {T, *}$ is a semilattice with ordering
:$\preceq_2 = \set {\tuple {p, p}, \tuple {q, q}, \tuple {r, r}, \tuple {s, s}, \tuple {p, r}, \tuple {q, r}, \tuple {p, s}, \tuple {q, s}, \tuple {r, s} }$
Let $\phi : S \to T$ be defined by:
:$\map \phi a = p$
:$\map \phi b = q$
:$\map \phi c = s$
Then a manual check shows that $\phi$ is [[order-preserving.
Now:
Hence $\phi$ is not a semilattice homomorphism by definition.
== Sources ==
* : Chapter $\text I$: Preliminaries, Definition $1.3$
Category:Semilattice Homomorphisms
Category:Increasing Mappings
Order 1 Simple Graph is Unique up to Isomorphism

== Theorem ==
Let $G_1 = \struct {\map V {G_1}, \map E {G_1} }$ and $G_2 = \struct {\map V {G_2}, \map E {G_2} }$ be simple graphs of order $1$.
Then $G_1$ and $G_2$ are isomorphic.
== Proof ==
There is only one bijection from $\map V {G_1}$ to $\map V {G_2}$.
There are no vertices adjacent to the sole vertex in $\map V {G_1}$
There are no vertices adjacent to the sole vertex in $\map V {G_2}$.
Hence the result, vacuously.
== Sources ==
* : Chapter $2$: Elementary Concepts of Graph Theory: $\S 2.2$: Isomorphic Graphs
Category:Graph Isomorphisms
Order 2 Square Matrices with Zero Diagonals do not form Ring

== Theorem ==
Let $S$ be the set of square matrices of order $2$ whose diagonal elements are zero.
Then the algebraic structure $\struct {S, +, \times}$ is not a ring.
Note that $\times$ denotes conventional matrix multiplication.
== Proof ==
For $\struct {S, +, \times}$ to be a ring, it is a necessary condition that $\struct {S, \times}$ is a semigroup.
For $\struct {S, \times}$ to be a semigroup, it is a necessary condition that $\struct {S, \times}$ is closed.
That is:
:$\forall x, y \in S: x \times y \in S$
Let $x = \begin {pmatrix} 0 & 1 \\ 1 & 0 \end {pmatrix}$ and $y = \begin {pmatrix} 0 & 2 \\ 2 & 0 \end {pmatrix}$.
Both $x$ and $y$ are in $S$, as both are square matrices of order $2$ whose diagonal elements are zero.
But then:
:$x y = \begin {pmatrix} 0 & 1 \\ 1 & 0 \end {pmatrix} \begin {pmatrix} 0 & 2 \\ 2 & 0 \end {pmatrix} = \begin {pmatrix} 2 & 0 \\ 0 & 2 \end {pmatrix}$
which is a square matrix of order $2$ whose diagonal elements are not zero.
Hence $x y \notin S$ and so $\struct {S, \times}$ is not closed.
The result follows.
== Sources ==
* : Chapter $1$: Rings - Definitions and Examples: $2$: Some examples of rings: Some 'non-examples': $\text {(c)}$
Category:Square Matrices
Category:Examples of Rings
Order Automorphism on Well-Ordered Class is Forward Moving

== Theorem ==
Let $\struct {A, \preccurlyeq}$ be a well-ordered class.
Let $\phi$ be an order isomorphism on $\struct {A, \preccurlyeq}$.
Then:
:$\forall a \in A: a \preccurlyeq \map \phi a$
== Proof ==
Let us define an element $a$ of $A$ such that:
:$\map \phi a \prec a$
as moving backwards.
 there exists an element $a$ of $A$ that moves backwards:
:$\map \phi a \prec a$
for some $a \in A$.
Then applying $\phi$ to both sides:
:$\map \phi {\map \phi a} \prec \map \phi a$
That is:
:$\map \phi a$ also moves backwards
Thus if some $a \in A$ moves backwards, there is another predecessor element that also moves backwards.
Hence there is no smallest element of the set of all elements of $A$ that move backwards.
But this contradicts the properties of a well-ordered class:
:every non-empty subclass of $A$ has a smallest element under $\preccurlyeq$.
Hence there can be no elements of $A$ that move backwards.
That is:
:$\forall a \in A: a \preccurlyeq \map \phi a$
== Linguistic Note ==
== Sources ==
* : Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 2$ Isomorphisms of well orderings: Theorem $2.1$
Category:Order Isomorphisms
Category:Well-Orderings
Order Automorphism on Well-Ordered Class is Forward Moving/Linguistic Note

== Linguistic Note on Order Automorphism on Well-Ordered Class is Forward Moving ==
The concept is introduced by and briefly in their of $2010$ as a stepping-stone to the stronger result Order Automorphism on Well-Ordered Class is Identity Mapping.
They do not actually give a name to the concept, but merely characterise it as a class mapping under which no element moves backwards.
It is worth comparing with the concept of a progressing mapping.
== Sources ==
* : Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 2$ Isomorphisms of well orderings: Theorem $2.1$
Category:Linguistic Notes
Order Automorphism on Well-Ordered Class is Identity Mapping

== Theorem ==
Let $\struct {A, \preccurlyeq}$ be a well-ordered class.
Let $\phi$ be an order isomorphism on $\struct {A, \preccurlyeq}$.
Then $\phi$ is the identity mapping:
:$\forall a \in A: \map \phi a = a$
== Proof ==
Let $\phi$ be an order isomorphism.
Then from Inverse of Order Isomorphism is Order Isomorphism, the inverse mapping $\phi^{-1}$ is also an order isomorphism.
From Order Automorphism on Well-Ordered Class is Forward Moving:
:$\forall a \in A: a \preccurlyeq \map \phi a$
and:
:$\forall a \in A: a \preccurlyeq \map {\phi^{-1} } a$
from which:
:$\forall a \in A: \map \phi a \preccurlyeq \map \phi {\map {\phi^{-1} } a} = a$
Hence:
:$\forall a \in A: \map \phi a = a$
== Sources ==
* : Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 2$ Isomorphisms of well orderings: Corollary $2.2$
Category:Order Isomorphisms
Category:Well-Orderings
Order Completion is Unique up to Isomorphism

== Theorem ==
Let $\struct {S, \preceq_S}$ be an ordered set.
Suppose that both $\struct {T, \preceq_T}$ and $\struct {T', \preceq_{T'} }$ are order completions for $\struct {S, \preceq_S}$.
Then there exists a unique order isomorphism $\psi: T \to T'$.
In particular, $\struct {T, \preceq_T}$ and $\struct {T', \preceq_{T'} }$ are isomorphic.
== Proof ==
Both $\struct {T, \preceq_T}$ and $\struct {T', \preceq_{T'} }$ are order completions for $\struct {S, \preceq_S}$.
Hence they both satisfy condition $(4)$ (and also $(1)$, $(2)$ and $(3)$).
Thus, applying condition $(4)$ to $\struct {T, \preceq_T}$ (with respect to $\struct {T', \preceq_{T'} }$), obtain a unique increasing mapping $\phi: T' \to T$.
Applying $(4)$ to $\struct {T', \preceq_{T'} }$ (with respect to $\struct {T, \preceq_T}$) gives also a unique increasing mapping $\psi: T \to T'$.
By Composite of Increasing Mappings is Increasing, their composites $\psi \circ \phi: T' \to T'$ and $\phi \circ \psi: T \to T$ are also increasing.
Now applying $(4)$ to $\struct {T, \preceq_T}$ (with respect to itself), it follows that $\phi \circ \psi$ is unique.
Now from Identity Mapping is Order Isomorphism, the identity mapping $I_T: T \to T$ is also increasing.
Thus, uniqueness of $\phi \circ \psi$ implies that $\phi \circ \psi = I_T$.
Similarly, it follows that $\psi \circ \phi = I_{T'}$.
It follows that $\psi: T \to T'$ is a bijection from Bijection iff Left and Right Inverse.
Thus, $\psi$ is an order-preserving bijection whose inverse is also increasing.
That is, $\psi$ is an order isomorphism.
Its uniqueness was already remarked above.
Category:Order Theory
Order Embedding/Examples/Finite Subsets of Natural Numbers in Divisibility Structure

== Example of Order Embedding ==
Consider the relational structures:
:$\struct {\Z_{>0}, \divides}$, where $\Z_{>0}$ denotes the strictly positive integers and $\divides$ denotes the divisor relation
:$\struct {\FF, \subseteq}$, where $\FF$ denotes the finite subsets of the natural numbers without zero $\N_{\ne 0}$ and $\subseteq$ denotes the subset relation.
Let $\pi: \FF \to \Z_{>0}$ be the mapping defined as:
:$\forall S \in \FF: \map \pi S = \ds \prod_{n \mathop \in S} \map p n$
where $\map p n$ denotes the $n$th prime number:
:$\map p 1 = 2, \map p 2 = 3, \map p 3 = 5, \ldots$
Then $\pi$ is an order embedding of $\FF$ into $\Z_{>0}$.
== Proof ==
Let $S \subseteq T$ where $S, T \in \F$.
Then:
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $21 \ \text {(a)}$
Category:Examples of Order Embeddings
Order Embedding between Quotient Fields is Unique

== Theorem ==
Let $\struct {R_1, +_1, \circ_1, \le_1}$ and $\struct {S, +_2, \circ_2, \le_2}$ be totally ordered integral domains.
Let $K, L$ be totally ordered fields of quotients of $\struct {R_1, +_1, \circ_1, \le_1}$ and $\struct {S, +_2, \circ_2, \le_2}$ respectively.
Let $\phi: R \to S$ be a order embedding.
Then there exists exactly one order embedding $\psi: K \to L$ extending $\phi$.
Also:
:$\forall x \in R, y \in R_{\ne 0}: \map \psi {\dfrac x y} = \dfrac {\map \phi x} {\map \phi y}$
If $\phi: R \to S$ is an order isomorphism, then so is $\psi$.
== Proof ==
By Field of Quotients is Unique, all we need to show is:
:$\forall x_1, x_2 \in R, y_1, y_2 \in R_{> 0}: \dfrac {x_1} {y_1} \le \dfrac {x_2} {y_2} \iff \dfrac {\map \phi {x_1}} {\map \phi {y_1} } \le \dfrac {\map \phi {x_2} } {\map \phi {y_2} }$
Let $x_1 / y_1 \le x_2 / y_2$, where $y_1, y_2 \in R_{> 0}$.
As $y_1, y_2 \in R_{> 0}$, it follows that $0 < y_1 \circ_1 y_2$ and $0 < 1 / \paren {y_1 \circ_1 y_2}$.
We also have:
:$0 < \map \phi {y_1} \circ_2 \map \phi {y_2} = \map \phi {y_1 \circ_1 y_2}$
Therefore:
:$x_1 \circ_1 y_2 = \frac {x_1} {y_1} \circ_1 \paren {y_1 \circ y_2} \le \dfrac {x_2} {y_2} \circ_1 \paren {y_1 \circ_1 y_2} = x_2 \circ_1 y_1$
Conversely, let $x_1 \circ_1 y_2 \le x_2 \circ_1 y_1$.
Then:
:$\dfrac {x_1} {y_1} = x_1 \circ_1 y_2 \circ_1 \paren {\dfrac 1 {y_1 \circ_1 y_2} } \le x_2 \circ_1 y_1 \circ_1 \paren {\dfrac 1 {y_1 \circ_1 y_2} } = \dfrac {x_2} {y_2}$
That is, we have:
:$\dfrac {x_1} {y_1} \le \dfrac {x_2} {y_2} \iff x_1 \circ_1 y_2 \le x_2 \circ_1 y_1$
Similarly:
:$\dfrac {\map \phi {x_1} } {\map \phi {y_1} } \le \dfrac {\map \phi {x_2} } {\map \phi {y_2} } \iff \map \phi {x_1} \circ_2 \map \phi {y_2} \le \map \phi {x_2} \circ_2 \map \phi {y_1}$
Now $\phi: R \to S$ is an order embedding.
Therefore:
:$x_1 \circ_1 y_2 \le x_2 \circ_1 y_1 \iff \map \phi {x_1 \circ_1 y_2} \le \map \phi {x_2 \circ_1 y_1}$
The result follows.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $23$. The Field of Rational Numbers: Theorem $23.14$
Category:Ordered Rings
Category:Fields of Quotients
Category:Total Orderings
Category:Order Embeddings
Order Embedding into Image is Isomorphism

== Theorem ==
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $S'$ be the image of a mapping $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$.
Then:
:$\phi$ is an order embedding from $\struct {S, \preceq_1}$ into $\struct {T, \preceq_2}$
:
:$\phi$ is an order isomorphism from $\struct {S, \preceq_1}$ into $\struct {S', \preceq_2 \restriction_{S'} }$.
== Proof ==
Let $\phi$ be an order embedding from $\struct {S, \preceq_1}$ into $\struct {T, \preceq_2}$.
Then $\phi$ is an injection into $\struct {T, \preceq_2}$ by definition.
From Restriction of Mapping to Image is Surjection, a mapping from a set to the image of that mapping is a surjection.
Thus the surjective restriction of $\phi$ onto $S'$ is an order embedding which is also a surjection.
Hence the result from Order Isomorphism is Surjective Order Embedding.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings
Category:Order Embeddings
Category:Order Isomorphisms
Order Embedding is Increasing Mapping

== Theorem ==
Let $\left({S_1, \preceq_1}\right)$, $\left({S_2, \preceq_2}\right)$ be ordered sets.
Let $f:S_1 \to S_2$ be an order embedding.
Then $f$ is increasing mapping.
== Proof ==
By definition of order embedding:
:$\forall x, y \in S_1: x \preceq_1 y \implies f\left({x}\right) \preceq_2 f\left({y}\right)$
Hence $f$ is an increasing mapping.
Category:Order Embeddings
Category:Increasing Mappings
Order Embedding is Injection

== Theorem ==
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi: S \to T$ be an order embedding.
That is:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
Then $\phi$ is an injection.
== Proof ==
Suppose $\phi: S \to T$ is a mapping such that:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
Then, for all $x, y \in S$:
So $\phi$ is an injection.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $19$
Category:Order Embeddings
Category:Injections
Order Generating Subset Includes Completely Irreducible Elements

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $X \subseteq S$ be an order generating subset of $S$.
Let $x \in S$ be a completely irreducible element of $S$.
Then $x \in X$.
== Proof ==
By definition of order generating:
:$x^\succeq \cap X$ admits an infimum and $x = \map \inf {x^\succeq \cap X}$
By Completely Irreducible and Subset Admits Infimum Equals Element implies Element Belongs to Subset:
:$x \in x^\succeq \cap X$
Thus by definition of intersection:
:$x \in X$
== Sources ==
* 
* 
Category:Meet Irreducible Elements
Category:Order Generating Subsets
Order Generating iff Every Element is Infimum

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is order generating
:$\forall x \in S: \exists Y \subseteq X: x = \inf Y$
== Proof ==
=== Sufficient Condition ===
Let $X$ be order generating.
Let $x \in S$.
By definition of order generating:
:$x = \map \inf {x^\succeq \cap X}$
Thus
:$\exists Y \subseteq X: x = \inf Y$
=== Necessary Condition ===
Let:
:$\forall x \in S: \exists Y \subseteq X: x = \inf Y$
Let $x \in S$.
By assumption:
:$\exists Y \subseteq X: x = \inf Y$
Define $Z := x^\succeq \cap X$.
We will prove that
:$\forall b \in S: b$ is lower bound for $Z \implies b \preceq x$
Let $b \in S$ such that
:$b$ is lower bound for $Z$.
Let $c \in Y$.
By definition of infimum:
:$x$ is lower bound for $Y$.
By definition of lower bound:
:$x \preceq c$
By definition of upper closure of element:
:$c \in x^\succeq$
By definition of subset:
:$c \in X$
By definition of intersection:
:$c \in Z$
Thus by definition of lower bound:
:$b \preceq c$
By definition of lower bound:
:$b$ is lower bound for $Y$
Thus by definition of infimum:
:$b \preceq x$
We will prove that
:$x$ is lower bound for $Z$
Let $a \in Z$
By definition of intersection:
:$a \in x^\succeq$
Thus by definition of upper closure of element:
:$x \preceq a$
Thus by definitions of complete lattice and infimum:
:$x^\succeq \cap X$ admits an infimum and $x = \map \inf {x^\succeq \cap X}$
== Sources ==
* 
* 
Category:Complete Lattices
Category:Order Generating Subsets