avewright/proofwiki-math huggingface dataset:
Theorem: Upper and Lower Closures of Open Set in GO-Space are Open

Let $\struct {X, \preceq, \tau}$ be a Generalized Ordered Space/Definition 1.
Let $A$ be open in $X$.
Then the upper and lower closures of $A$ are open.

Proof:
We will show that the upper closure $U$ of $A$ is open.
The lower closure can be proven open by the same method.
By the definition of upper closure:
:$U = \set {u \in X: \exists a \in A: a \preceq u}$
But then:
{{begin-eqn}}
{{eqn | l = U
      | r = \set {u \in X: \paren {u \in A} \lor \paren {\exists a \in A: a \prec u} }
}}
{{eqn | r = A \cup \bigcup \set {a^\succeq: a \in A}
}}
{{end-eqn}}
where $a^\preceq$ denotes the upper closure of $a$.
By Open Ray is Open in GO-Space/Definition 1, each $a^\succeq$ is open.
Thus $U$ is a union of open sets.
Thus $U$ is open by the definition of a topology.
{{qed}}
Category:Topology
Category:Total Orderings
34qx1knv00cciokrfj7mb0e712pxg20
Theorem: Equivalence of Definitions of Generalized Ordered Space/Definition 1 implies Definition 3

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 1:
{{:Definition:Generalized Ordered Space/Definition 1}}
Then $\struct {S, \preceq, \tau}$ is a generalized ordered space by Definition 3:
{{:Definition:Generalized Ordered Space/Definition 3}}

Proof:
Let $\BB$ be a basis for $\tau$ consisting of order-convex sets.
Let:
:$\SS = \set {U^\succeq: U \in \BB} \cup \set {U^\preceq: U \in \BB}$
where $U^\succeq$ and $U^\preceq$ denote the upper closure and lower closure respectively of $U$.
By Upper Closure is Upper Section and Lower Closure is Lower Section, the elements of $\SS$ are upper and lower sections.
It is to be shown that $\SS$ is a sub-basis for $\tau$.
By Upper and Lower Closures of Open Set in GO-Space are Open:
:$\SS \subseteq \tau$
By Order-Convex Set Characterization, each element of $\BB$ is the intersection of its upper closure with its lower closure.
Thus each element of $\BB$ is generated by $\SS$.
{{Disambiguate|Definition:Generated}}
Thus $\SS$ is a sub-basis for $\tau$.
Theorem: Upper Section is Order-Convex

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ be an upper section.
Then $T$ is order-convex in $S$.

Proof:
Let $a, c \in T$.
Let $b \in S$.
Let $a \preceq b \preceq c$.
Since:
:$a \in T$
:$a \preceq b$
:$T$ is an upper section
it follows that:
:$b \in T$
This holds for all such $a$, $b$, and $c$.
Therefore, by definition, $T$ is order-convex in $S$.
{{qed}}
Theorem: Lower Section is Order-Convex

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ be a lower section.
Then $T$ is order-convex in $S$.

Proof:
Let $a, c \in T$.
Let $b \in S$.
Let $a \preceq b \preceq c$.
Since:
:$c \in T$
:$b \preceq c$
:$T$ is a lower section
it follows that:
:$b \in T$
This holds for all such $a$, $b$, and $c$.
Hence, by definition, $T$ is order-convex in $S$.
{{qed}}
Theorem: GO-Space Embeds Densely into Linearly Ordered Space

Let $\struct {Y, \preceq, \tau}$ be a generalized ordered space (GO-space) by Definition 3.
That is:
:let $\struct {Y, \tau}$ be a Hausdorff space
and:
:let $\tau$ have a sub-basis consisting of upper sections and lower sections relative to $\preceq$.
Then $\struct {Y, \preceq, \tau}$ is a GO-space by Definition 2.
That is, there is a linearly ordered space $\struct {X, \preceq', \tau'}$ and a mapping from $Y$ to $X$ which is a order embedding and a topological embedding.

Proof:
<section  notitle="True" name="proof">
Let $X$ be the disjoint union of $Y$ with the set of all lower sections $L$ in $Y$ such that $L$ and $Y \setminus L$ are open and nonempty and either:
:$L$ has a maximum, and $Y\setminus L$ does not have a minimum, or
:$Y \setminus L$ has a minimum, and $L$ does not have a maximum.
Let $\phi: Y \to X$ be the inclusion mapping.
In the following, let $y$, $y_1$, $y_2$, and $y_3$ represent elements of $Y$, and let $L$, $L_1$, $L_2$, and $L_3$ represent lower sections of $Y$ that are members of $X$.
Define a relation $\preceq'$ extending $\preceq$ by letting:
:$y_1 \preceq' y_2 \iff y_1 \preceq y_2$
:$y \preceq' L \iff y \in L$
:$L_1 \preceq' L_2 \iff L_1 \subseteq L_2$
:$L \preceq' y \iff y \in Y \setminus L$
By Union of Total Ordering with Lower Sections is Total Ordering and Restriction of Total Ordering is Total Ordering, $\preceq'$ is a total ordering.
Because $y_1 \preceq' y_2$ iff $y_1 \preceq y_2$, $\phi$ is an order embedding.
Let $\tau'$ be the $\preceq'$ order topology on $X$.
Theorem: Upper Section with no Minimal Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $U \subseteq S$.
Then:
:$U$ is an upper section in $S$ with no minimal element
{{iff}}:
:$\ds U = \bigcup \set {u^\succ: u \in U}$
where $u^\succ$ is the strict upper closure of $u$.

Proof:
=== Forward implication ===
Let $U$ be an upper section in $S$ with no minimal element.
Then by the definition of upper section:
:$\ds \bigcup \set {u^\succ: u \in U} \subseteq U$
Let $x \in U$.
Since $U$ has no minimal element, $x$ is not minimal.
Thus there is a $u \in U$ such that $u \prec x$.
Then $x \in u^\succ$, so:
:$\ds x \in \bigcup \set {u^\succ: u \in U }$
Since this holds for all $x \in U$:
:$\ds U \subseteq \bigcup \set {u^\succ: u \in U}$
Thus the theorem holds by definition of set equality.
{{qed|lemma}}
Theorem: Lower Sections in Totally Ordered Set form Chain

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\LL$ be a set of lower sections in $S$.
Then $\LL$ is a chain.
That is, $\LL$ is totally ordered by $\subseteq$.

Proof:
Let $L, M \in \LL$.
Suppose that $M \nsubseteq L$.
Then:
:$\exists x \in M: x \notin L$
Let $y \in L$.
Then since $\preceq$ is a total ordering, $x \preceq y$ or $y \preceq x$.
If $x \preceq y$, then since $L$ is a lower section: $x \in L$, a contradiction.
Thus $y \preceq x$.
Since $M$ is a lower section, $y \in M$.
Since this holds for all $y \in L$, $L \subseteq M$.
Hence, for all $L, M \in \LL$:
:$M \subseteq L$ or $L \subseteq M$
That is, $\LL$ is a chain.
{{qed}}
Category:Lower Sections
Category:Total Orderings
Category:Chains (Order Theory)
p0lvgr31a7fwgnyhcfsf6rculo5e1h5
Theorem: Exclusive Or is Self-Inverse

:$\paren {p \oplus q} \oplus q \dashv \vdash p$
where $\oplus$ denotes the exclusive or operator.

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective on the {{LHS}} match those for $p$ on the {{RHS}} for all boolean interpretations:
$\begin{array}{|ccccc||c|} \hline
(p & \oplus & q) & \oplus & q & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \T & \T & \F & \T & \F \\
\T & \T & \F & \T & \F & \T \\
\T & \F & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Conjunction has no Inverse

Let $\land$ denote the conjunction operation of propositional logic.
Then there exists no binary logical connective $\circ$ such that:
:$(1): \quad \forall p, q \in \set {T, F}: \left({p \land q}\right) \circ q = p$

Proof:
This will be proven by contradiction.
Let such an operation $\circ$ exist.
Let $f^\circ: \mathbb B^2 \to \mathbb B$ be the associated truth function.
Suppose now that $q = F$, while $p$ remains unspecified.
Then:
:$p \land q = \map {f^\land} {p, F} = F$
where $f^\land$ is the truth function of conjunction.
It does not matter what $p$ is, for:
:$\map {f^\land} {T, F} = \map {f^\land} {F, F} = F$
Hence, for $\paren {p \land q} \circ q = p$ to hold, $f^\circ$ must satisfy:
:$\map {f^\circ} {F, F} = p$
However, because $p$ could still be either $T$ or $F$, this identity cannot always hold.
Therefore, $\circ$ cannot exist.
{{qed}}
Category:Conjunction
5qyy8yux2chdychodv15re87n8t5dnf
Theorem: Disjunction has no Inverse

Let $\lor$ denote the disjunction operation of propositional logic.
Then there exists no binary logical connective $\circ$ such that:
:$(1): \quad \forall p, q \in \left\{{T, F}\right\}: \left({p \lor q}\right) \circ q = p$

Proof:
Let $q$ be true.
Then $p \lor q = T$, whatever truth value $p$ holds.
In this case $(1)$ simplifies to:
:$(2): \quad \forall p \in \left\{{T, F}\right\}: T \circ T = p$
Either $T \circ T = T$ or $T \circ T = F$, but not both.
If $p = F$, then it must be that $T \circ T = F$.
If $p = T$, then it must be that $T \circ T = T$.
Hence there can be no such $\circ$.
{{qed}}
Category:Disjunction
tb3ceoqw69l5lkdsmtgm1jwo2ehz2mc
Theorem: Biconditional is Self-Inverse

:$\paren {p \iff q} \iff q \dashv \vdash p$
where $\iff$ denotes the biconditional operator.

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective on the {{LHS}} match those for $p$ on the {{RHS}} for all boolean interpretations:
:<nowiki>$\begin{array}{|ccccc||c|} \hline
(p & \iff & q) & \iff & q & p \\
\hline
\F & \T & \F & \F & \F & \F \\
\F & \F & \T & \F & \T & \F \\
\T & \F & \F & \T & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Category:Biconditional
Category:Truth Table Proofs
6iuc73mpi7a0ocn4eodsuacmzjp3b5y
Theorem: Finite Chain is Order-Isomorphic to Finite Ordinal

Let $\struct {S, \preceq}$ be an ordered set.
Let $C$ be a finite chain in $S$.
Then for some finite ordinal $\mathbf n$:
:$\struct {C, {\preceq \restriction_C} }$ is order-isomorphic to $\mathbf n$.
That is:
:$\struct {C, {\preceq \restriction_C} }$ is order-isomorphic to $\N_n$
where $\N_n$ is the initial segment of $\N$ determined by $n$:
:$\N_n = \set {k \in \N: k < n} = \set {0, 1, \ldots, n - 1}$

Proof:
By the definition of finite set:
:there exists an $n \in \N$ such that there exists a bijection $f: C \to \N_n$.
This $n$ is unique by Equality of Natural Numbers and Set Equivalence behaves like Equivalence Relation.
Define a mapping $g: \N_n \to C$ recursively as:
:$\map g 0 = \min C$
:$\map g {k + 1} = \map \min {C \setminus \map g {N_k} }$
{{explain|How is $\min C$ is defined?}}
{{finish}}
Theorem: Complete Linearly Ordered Space is Compact

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $\struct {X, \preceq}$ be a complete lattice.
Then $\struct {X, \tau}$ is compact.

Proof:
By Space is Compact iff exists Basis such that Every Cover has Finite Subcover, it is sufficient to prove that an open cover of $X$ consisting of open intervals and rays has a finite subcover.
Let $\AA$ be an open cover of $X$ consisting of open rays and open intervals.
Let $m = \inf X$.
This infimum exists because $\struct {X, \preceq}$ is complete.
Let $C$ be the set of all $x \in X$ such that a finite subset of $\AA$ covers $\closedint m x$.
$C$ is non-empty because $m \in C$.
Let $s = \sup C$.
Since $\AA$ covers $X$, there is a $U \in \AA$ such that $s \in U$.
Then we must have $U = \openint a b$, $U = {\dot\uparrow} a$, or $U = {\dot\downarrow} b$.
Suppose that $U = \openint a b$.
Let $V \in \UU$ contain $b$.
Then by the definition of supremum, there is an $x \succ a$ such that there is a finite $\FF \subseteq \AA$ that covers $\closedint m x$.
Then $\FF \cup \set {U, V}$ covers $\closedint m b$, contradicting the fact that $s$ is an upper bound of $C$.
Suppose next that $U = \dot\downarrow b$.
Then for some $V \in \AA$, $b \in V$.
Then $\closedint m b$ is covered by $\set {U, V}$, contradicting the fact that $s$ is the supremum of $C$.
Thus $U = \dot\uparrow a$.
By the definition of supremum, $a$ is not an upper bound of $C$.
So there is an $x \succ a$ such that there is a finite subset $\FF$ of $\AA$ that covers $\closedint m x$.
Thus $\FF \cup \set U$ is a finite subcover of $A$.
{{qed}}
Theorem: Infinite Sequence Property of Well-Founded Relation/Reverse Implication

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be such that there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
Then $\RR$ is a well-founded relation.

Proof:
Suppose $\RR$ is not a well-founded relation.
So by definition there exists a non-empty subset $T$ of $S$ which has no minimal element.
Let $a \in T$.
Since $a$ is not minimal in $T$, we can find $b \in T: \paren {b \mathrel \RR a} \text { and } \paren {b \ne a}$.
This holds for all $a \in T$.
Hence the restriction $\RR \restriction_{T \times T}$ of $\RR$ to $T \times T$ is a right-total endorelation on $T$.
So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
then $\RR$ is a well-founded relation.
Theorem: Infinite Sequence Property of Well-Founded Relation/Reverse Implication

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be such that there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
Then $\RR$ is a well-founded relation.

Proof:
Suppose $\RR$ is not a well-founded relation.
Hence there exists $T \subseteq S$ such that $T$ has no minimal element under $\RR$.
Let $a_0 \in T$.
We have that $a_0$ is not minimal in $T$.
So:
:$\exists a_1 \in T: \paren {a_1 \mathrel \RR a_0} \text { and } a_1 \ne a_0$
Similarly, $a_1$ is not minimal in $T$.
So:
:$\exists a_2 \in T: \paren {a_2 \mathrel \RR a_1} \text { and } a_2 \ne a_1$
Let $a_{k + 1}$ be an arbitrary element for which $a_{k + 1} \mathrel \RR a_k$ and $a_{k + 1} \ne a_k$.
In order to allow this to be possible in the infinite case, it is necessary to invoke the Axiom of Dependent Choice as follows:
Let $a_k \in T$.
Then as $a_k$ is not minimal in $T$:
:$\exists a_{k + 1} \in T: \paren {a_{k + 1} \mathrel \RR a_k} \text { and } \paren {a_{k + 1} \ne a_k}$
Hence by definition $\RR$ is a right-total relation.
So, by the Axiom of Dependent Choice, it follows that:
:$\forall n \in \N: \exists a_n \in T: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } a_{n + 1} \ne a_n$
Thus we have been able to construct an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } a_{n + 1} \ne a_n$
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } a_{n + 1} \ne a_n$
then $\RR$ is a well-founded relation.
Theorem: Inversion Mapping on Ordered Group is Dual Order-Isomorphism

Let $\struct {G, \circ, \preceq}$ be an ordered group.
Let $\iota: G \to G$ be the inversion mapping, defined by $\map \phi x = x^{-1}$.
Then $\iota$ is a dual order-isomorphism.

Proof:
By Inversion Mapping is Involution and Involution is Permutation, $\iota$ is a permutation and so by definition bijective.
Let $x, y \in G$ such that $x \prec y$.
Then $y^{-1} \prec x^{-1}$ by Inversion Mapping Reverses Ordering in Ordered Group.
Thus $\map \iota y \prec \map \iota x$.
Since this holds for all $x$ and $y$ with $x \prec y$, $\iota$ is strictly decreasing.
If $\map \iota x \prec \map \iota y$, then $\map \iota {\map \iota y} \prec \map \iota {\map \iota x}$ by the above.
Thus by Inverse of Group Inverse: $y \prec x$.
Therefore, $\iota$ reverses ordering in both directions, and is thus a dual isomorphism.
{{qed}}
Category:Ordered Groups
Category:Inversion Mappings
r4yxtzyk6j10d5wzp88nv29h4wf9ga9
Theorem: Ordering Compatible with Group Operation is Strongly Compatible/Corollary/Proof 1

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group with identity $e$.
Let $\prec$ be the reflexive reduction of $\preceq$.
Let $x, y \in G$.
Then the following equivalences hold:
{{:Ordering Compatible with Group Operation is Strongly Compatible/Corollary}}

Proof:
By the definition of an ordered group, $\preccurlyeq$ is a relation compatible with $\circ$.
Thus by {{Corollary|Relation Compatible with Group Operation is Strongly Compatible}}, we obtain the first four results.
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is compatible with $\circ$.
Again by {{Corollary|Relation Compatible with Group Operation is Strongly Compatible}}, we obtain the remaining results.
{{qed}}
Theorem: Ordering Compatible with Group Operation is Strongly Compatible/Corollary/Proof 2

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group with identity $e$.
Let $\prec$ be the reflexive reduction of $\preccurlyeq$.
Let $x, y \in G$.
Then the following equivalences hold:
{{:Ordering Compatible with Group Operation is Strongly Compatible/Corollary}}

Proof:
Each result follows from Ordering Compatible with Group Operation is Strongly Compatible.
For example, by Ordering Compatible with Group Operation is Strongly Compatible:
:$x \preccurlyeq y \iff x \circ x^{-1} \preccurlyeq y \circ x^{-1}$
Since $x \circ x^{-1} = e$:
:$x \preccurlyeq y \iff e \preccurlyeq y \circ x^{-1}$
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group/Corollary/Proof 1

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group with identity $e$.
Let $x \in G$.
Then the following equivalences hold:
{{:Inversion Mapping Reverses Ordering in Ordered Group/Corollary}}

Proof:
By Inversion Mapping Reverses Ordering in Ordered Group:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e^{-1} \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e^{-1}
}}
{{eqn | l = x \prec e
      | o = \iff
      | r = e^{-1} \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e^{-1}
}}
{{end-eqn}}
Since $e^{-1} = e$, the theorem holds.
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group/Corollary/Proof 2

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group with identity $e$.
Let $x \in G$.
Then the following equivalences hold:
{{:Inversion Mapping Reverses Ordering in Ordered Group/Corollary}}

Proof:
By the definition of an ordered group, $\preccurlyeq$ is a relation compatible with $\circ$.
Thus by Inverses of Elements Related by Compatible Relation: Corollary:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e
}}
{{end-eqn}}
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is also compatible with $\circ$.
Thus again by Inverses of Elements Related by Compatible Relation: Corollary:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \prec e
      | o = \iff
      | r = e \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e
}}
{{end-eqn}}
{{qed}}
Theorem: Mapping from Totally Ordered Set is Dual Order Embedding iff Strictly Decreasing

Let $\left({S, \preceq_1}\right)$ be a totally ordered set.
Let $\left({T, \preceq_2}\right)$ be an ordered set.
Let $\phi: S \to T$ be a mapping.
Then $\phi$ is a dual order embedding {{iff}} $\phi$ is strictly decreasing.
That is:
:$\forall x, y \in S: x \preceq_1 y \iff \phi \left({y}\right) \preceq_2 \phi \left({x}\right)$
{{iff}}
:$\forall x, y \in S: x \prec_1 y \implies \phi \left({y}\right) \prec_2 \phi \left({x}\right)$

Proof:
=== Forward Implication ===
Let $\phi$ be a dual order embedding.
Then $\phi$ is an order embedding of $\left({S, \preceq_1}\right)$ into $\left({T, \succeq_2}\right)$, where $\succeq_2$ is the dual of $\preceq_2$.
Thus by Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing:
:$\phi: \left({S, \preceq_1}\right) \to \left({T, \succeq_2}\right)$ is strictly increasing.
Thus:
:$\forall x, y \in S: x \prec_1 y \implies \phi \left({x}\right) \succ_2 \phi \left({y}\right)$
so:
:$\forall x, y \in S: x \prec_1 y \implies \phi \left({y}\right) \prec_2 \phi \left({x}\right)$ 
Thus $\phi: \left({S, \preceq_1}\right) \to \left({T, \preceq_2}\right)$ is strictly decreasing.
{{qed|lemma}}
Theorem: Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing/Reverse Implication

Let $\struct {S, \preceq_1}$ be a totally ordered set.
Let $\struct {T, \preceq_2}$ be an ordered set.
Let $\phi: S \to T$ be a strictly increasing mapping.
Then $\phi$ is an order embedding.

Proof:
Let $x \preceq_1 y$.
Then $x = y$ or $x \prec_1 y$.
Let $x = y$.
Then
:$\map \phi x = \map \phi y$
so:
:$\map \phi x \preceq_2 \map \phi y$
Let $x \prec_1 y$.
Then by the definition of strictly increasing mapping:
:$\map \phi x \prec_2 \map \phi y$
so by the definition of $\prec_2$:
:$\map \phi x \preceq_2 \map \phi y$
Thus:
:$x \preceq_1 y \implies \map \phi x \preceq_2 \map \phi y$
It remains to be shown that:
:$\map \phi x \preceq_2 \map \phi y \implies x \preceq_1 y$
Suppose that $x \npreceq_1 y$.
Since $\preceq_1$ is a total ordering:
:$y \prec_1 x$
Thus since $\phi$ is strictly increasing:
:$\map \phi y \prec_1 \map \phi x$
Thus:
:$\map \phi x \npreceq_1 \map \phi y$
Therefore:
:$x \npreceq_1 y \implies \map \phi x \npreceq_2 \map \phi y$
By the Rule of Transposition:
:$\map \phi x \preceq_2 \map \phi y \implies x \preceq y$
{{qed}}
Theorem: Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing/Reverse Implication

Let $\struct {S, \preceq_1}$ be a totally ordered set.
Let $\struct {T, \preceq_2}$ be an ordered set.
Let $\phi: S \to T$ be a strictly increasing mapping.
Then $\phi$ is an order embedding.

Proof:
Let $\phi$ be strictly increasing.
Let $\map \phi x \preceq_2 \map \phi y$.
As $\struct {S, \prec_1}$ is a strictly totally ordered set:
:Either $y \prec_1 x$, $y = x$, or $x \prec_1 y$.
{{AimForCont}} that $y \prec_1 x$.
By the definition of a strictly increasing mapping:
:$\map \phi y \prec_2 \map \phi x$
which contradicts the fact that $\map \phi x \preceq_2 \map \phi y$.
Therefore $y \nprec_1 x$.
Thus $y = x$, or $x \prec_1 y$, so $x \preceq_1 y$.
Hence:
:$\map \phi x \preceq_2 \map \phi y \iff x \preceq_1 y$
and $\phi$ has been proved to be an order embedding.
{{qed}}
Theorem: Strictly Well-Founded Relation is Antireflexive

Let $\RR$ be a strictly well-founded relation on a set or class $A$.
Then $\RR$ is antireflexive.

Proof:
Let $p \in A$.
Then $\set p \ne \O$ and $\set p \subseteq A$.
Thus, by the definition of strictly well-founded relation:
:$\exists x \in \set p: \forall y \in \set p: \neg \paren {y \mathrel \RR x}$
Since $x \in \set p$, it must be that $x = p$.
It follows that $p \not \mathrel \RR p$.
Since this holds for all $p \in A$, $\RR$ is antireflexive.
{{qed}}
Category:Well-Founded Relations
Category:Antireflexive Relations
5bah43tukit95d8y7quy4baixkh7193
Theorem: Strictly Well-Founded Relation is Asymmetric

Let $\struct {S, \RR}$ be a relational structure, where $S$ is a set or a proper class.
Let $\RR$ be a strictly well-founded relation.
Then $\RR$ is asymmetric.

Proof:
Let $p, q \in S$ and suppose that $p \mathrel \RR q$.
Then $\set {p, q} \ne \O$ and $\set {p, q} \subseteq S$.
By the definition of strictly well-founded relation, $\set {p, q}$ has a strictly minimal element under $\RR$.
Since $p \mathrel \RR q$, $q$ is not an $\RR$-minimal element of $\set {p, q}$.
Thus $p$ is a strictly minimal element under $\RR$ of $\set {p, q}$.
Thus $q \not \mathrel \RR p$.
Since for all $p, q \in S$, $p \mathrel \RR q \implies q \not \mathrel \RR p$, $\RR$ is asymmetric.
{{qed}}
Category:Well-Founded Relations
Category:Asymmetric Relations
427mez2guabna3iuw1emlvhl0cdgz71
Theorem: Upper Section with no Smallest Element is Open in GO-Space

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space.
Let $U$ be an upper section in $S$ with no smallest element.
Then $U$ is open in $\struct {S, \preceq, \tau}$.

Proof:
By Minimal Element in Toset is Unique and Smallest, $U$ has no minimal element.
By Upper Section with no Minimal Element:
:$U = \bigcup \set {u^\succ: u \in U}$
where $u^\succ$ is the strict upper closure of $u$.
By Open Ray is Open in GO-Space and the fact that a union of open sets is open, $U$ is open.
{{qed}}