nyuuzyou/wikis huggingface dataset:
Equivalence of Definitions of Exterior Point (Complex Analysis)

== Theorem ==
Let $S \subseteq \C$ be a subset of the complex plane.
Let $z_0 \in \C$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $S \subseteq \C$.
=== Definition 1 implies Definition 2 ===
Let $z_0$ be an exterior point of $S$ by definition 1.
Let $\map {N_\epsilon} {z_0}$ be an $\epsilon$-neighborhood of $z_0$ such that $\map {N_\epsilon} {z_0} \cap S = \O$.
That is, $\map {N_\epsilon} {z_0}$ has no points which are also in $S$.
By definition, it follows that $z_0$ is not a boundary point of $S$.
 $z_0$ is an interior point of $S$.
Let $\map {N_{\epsilon'} } {z_0}$ be an $\epsilon'$-neighborhood such that $\map {N_{\epsilon'} } {z_0} \subseteq S$.
By Empty Intersection iff Subset of Complement:
: $\map {N_\epsilon} {z_0} \subseteq \relcomp \C S$
Thus $z_0$ is an exterior point of $S$ by definition 2.
=== Definition 2 implies Definition 1 ===
Let $z_0$ be an exterior point of $S$ by definition 2.
As $z_0$ is not an interior point of $S$ there exists no $\epsilon$-neighborhood of $z_0$ which is disjoint from $\relcomp \C S$.
That is, every $\epsilon$-neighborhood of $z_0$ contains points which are not in $S$.
As $z_0$ is not a boundary point of $S$, there exists at least one $\epsilon$-neighborhood of $z_0$ which does not contain both points in $S$ and points not in $S$.
But as every $\epsilon$-neighborhood of $z_0$ contains points which are not in $S$, it follows there must be at least one $\epsilon$-neighborhood of $z_0$ disjoint from $S$.
Thus $z_0$ is an exterior point of $S$ by definition 1.
Category:Complex Analysis
Equivalence of Definitions of Extremally Disconnected Space

== Theorem ==
=== Definition 1: using Closures of Open Sets ===
=== Definition 2: using Interiors of Closed Sets ===
=== Definition 3: using Disjoint Open Sets ===
== Proof ==
=== $(1)$ iff $(2)$ ===
;Extremally Disconnected by Interior of Closed Sets:
=== $(1)$ iff $(3)$ ===
;Extremally Disconnected by Disjoint Open Sets:
Category:Extremally Disconnected Spaces
Category:Equivalence of Definitions of Extremally Disconnected Space
Equivalence of Definitions of Extreme Point of Convex Set

== Theorem ==
Let $X$ be a vector space over $\R$. 
Let $K$ be a convex subset of $X$. 
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Suppose that: 
:whenever $a = t x + \paren {1 - t} y$ for $t \in \openint 0 1$, we have $x = y = a$.
Then, if $x, y \in K \setminus \set a$ and $t \in \openint 0 1$, we have: 
:$t x + \paren {1 - t} y \ne a$ 
If $t = 0$, then we have: 
:$t x + \paren {1 - t} y = y \ne a$
and if $t = 1$ we have: 
:$t x + \paren {1 - t} y = x \ne a$ 
So if $x, y \in K \setminus \set a$ and $t \in \closedint 0 1$ we have:
:$t x + \paren {1 - t} y \ne a$ 
Since $K$ is convex, we have: 
:$t x + \paren {1 - t} y \in K$
so we have: 
:$t x + \paren {1 - t} y \in K \setminus \set a$
so:
:$K \setminus \set a$ is convex.
 
=== Definition 2 implies Definition 1 ===
Suppose:
:$K \setminus \set a$ is convex.
Then for all $x, y \in K \setminus \set a$ and $t \in \closedint 0 1$ we have: 
:$t x + \paren {1 - t} y \in K \setminus \set a$
In particular, if $t \in \openint 0 1$ and $x, y \in K \setminus \set a$, we have: 
:$t x + \paren {1 - t} y \ne a$
We also have that: 
:$t a + \paren {1 - t} a = a$
Hence, if $x, y \in K$ and $t \in \openint 0 1$ have: 
:$t x + \paren {1 - t} y = a$
then: 
:$x = y = a$
Category:Convex Sets (Vector Spaces)
Category:Extreme Points of Convex Sets
Equivalence of Definitions of Factorial

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\begin {cases} 1 & : n = 0 \\ n \paren {n - 1}! & : n > 0 \end {cases} \equiv \ds \prod_{k \mathop = 1}^n k$
=== Basis for the Induction ===
$\map P 0$ is the case:
:$\ds \prod_{k \mathop = 1}^0 k = 1$
which holds by definition of vacuous product.
Thus $\map P 0$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P r$ is true, where $r \ge 0$, then it logically follows that $\map P {r + 1}$ is true.
So this is the induction hypothesis:
:$\begin {cases} 1 & : r = 0 \\ r \paren {r - 1}! & : r > 0 \end {cases} \equiv \ds \prod_{k \mathop = 1}^r k$
from which it is to be shown that:
:$\begin {cases} 1 & : r = 0 \\ \paren {r + 1} r! & : r > 0 \end {cases} \equiv \ds \prod_{k \mathop = 1}^{r + 1} k$
=== Induction Step ===
This is the induction step:
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\begin {cases} 1 & : n = 0 \\ n \paren {n - 1}! & : n > 0 \end{cases} \equiv \ds \prod_{k \mathop = 1}^n k$
Category:Factorials
Equivalence of Definitions of Field (Abstract Algebra)

== Theorem ==
=== Definition $1$ ===
=== Definition $2$ ===
=== Definition $3$ ===
=== Definition $4$ ===
=== Definition $5$ ===
== Proof ==
=== Definition $(1)$ implies Definition $(5)$ ===
Let $\struct {F, +, \times}$ be a field by definition $1$.
By the definition of abelian group:
:$(\text A 0): \quad \struct {F, +}$ is closed
:$(\text A 1): \quad +$ is associative on $F$
:$(\text A 2): \quad +$ is commutative on $F$
:$(\text A 3): \quad$ there exists an identity element $0_F$ for $+$
:$(\text A 4): \quad$ for every $a \in F$ there exists an inverse element $-a$ for $+$
Then:
:$(\text M 0): \quad \struct {F, \times}$ is closed under addition
:$(\text M 1): \quad \times$ is associative on $F$
:$(\text M 2): \quad \times$ is commutative on $F$
:$(\text M 3): \quad$ there exists an identity element $1_F$ for $\times$
:$(\text M 4): \quad$ for every $a \in F$ there exists an inverse element $a^{-1}$ for $\times$
Finally we are given:
:$(\text D): \quad \times$ is distributive over $+$ in $\struct {F, +, \times}$.
Thus $\struct {F, +, \times}$ is a field by definition $5$.
=== Definition $(5)$ implies Definition $(1)$ ===
Let $\struct {F, +, \times}$ be a field by definition $5$.
From $(\text A 0)$ to $(\text A 4)$, $\struct {F, +}$ is an abelian group.
From $(\text M 0)$ to $(\text M 4)$, $\struct {F \setminus \set 0_F, \times}$ is an abelian group.
Finally from $D$, $\times$ is distributive over $+$.
Thus $\struct {F, +, \times}$ is a field by definition $1$.
Category:Fields (Abstract Algebra)
Equivalence of Definitions of Filter Basis

== Theorem ==
Let $S$ be a set.
Let $\FF$ be a filter on $S$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== $(1)$ implies $(2)$ ===
Let $\BB$ be a filter basis of $\FF$ by definition $1$.
Then by definition:
:$\BB \subset \powerset S$ such that $\O \notin \BB$ and $\BB \ne \O$
and $\FF := \set {V \subseteq S: \exists U \in \BB: U \subseteq V}$ is a filter on $S$ :
:$\forall V_1, V_2 \in \BB: \exists U \in \BB: U \subseteq V_1 \cap V_2$
Let $U \in \FF$.
Then by definition of $\FF$:
:$\exists V \in \BB: V \subseteq U$
Thus $\BB$ is a filter basis of $\FF$ by definition $2$.
=== $(2)$ implies $(1)$ ===
Let $\BB$ be a filter basis of $\FF$ by definition $2$.
By definition, $\BB$ is a filter basis of $\FF$ :
:$\forall U \in \FF: \exists V \in \BB: V \subseteq U$
Let $V_1, V_2 \in \BB$.
Then:
:$V_1, V_2 \in \FF$
By definition of filter:
:$V_1 \cap V_2 \in \FF$
and so:
:$\exists U \in \BB: U \subseteq V_1 \cap V_2$
Thus $\BB$ is a filter basis of $\FF$ by definition $1$.
Category:Filter Bases
Equivalence of Definitions of Filter on Set

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Conditions $(\text F 1)$, $(\text F 2)$ and $(\text F 4)$ are the same for both definitions.
It remains to establish that $(\text F 3)$ in Definition 1 is equivalent to $(\text F 3)$ in Definition 2.
=== $(1)$ implies $(2)$ ===
Let $\FF$ be a filter on $S$ by definition $1$.
Then by definition:
:$U_1, U_2 \in \FF \implies U_1 \cap U_2 \in \FF$
Suppose that for some $k \in \N$:
:$(\text F 3): U_1, \ldots, U_k \in \FF \implies \ds \bigcap_{i \mathop = 1}^k U_i \in \FF$
Then we have:
:$\ds \paren {\bigcap_{i \mathop = 1}^k U_i} \cap U_{k + 1} = \bigcap_{i \mathop = 1}^{k + 1} U_i$
by hypothesis.
Hence by induction:
:$U_1, \ldots, U_k, U_{k + 1} \in \FF \implies \ds \bigcap_{i \mathop = 1}^{k + 1} U_i \in \FF$
Thus $\FF$ is a filter on $S$ by definition $2$.
=== $(2)$ implies $(1)$ ===
Let $\FF$ be a filter on $S$ by definition $2$.
Then by definition:
:$(\text F 3): \forall n \in \N: U_1, \ldots, U_n \in \FF \implies \ds \bigcap_{i \mathop = 1}^n U_i \in \FF$
In particular when $n = 2$:
:$U_1, U_2 \in \FF \implies U_1 \cap U_2 \in \FF$
Thus $\FF$ is a filter on $S$ by definition $1$.
Category:Filter Theory
Equivalence of Definitions of Final Topology

== Theorem ==
Let $X$ be a set.
Let $I$ be an indexing set.
Let $\family {\struct {Y_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces indexed by $I$.
Let $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 Implies Definition 2 ===
=== Definition 2 Implies Definition 1 ===
Category:Final Topology
Equivalence of Definitions of Final Topology/Definition 1 Implies Definition 2

== Theorem ==
Let $X$ be a set.
Let $I$ be an indexing set.
Let $\family {\struct {Y_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces indexed by $I$.
Let $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
Let:
:$\tau = \set{U \subseteq X: \forall i \in I: \map {f_i^{-1}} U \in \tau_i} \subseteq \powerset X$
Then:
:$\tau$ is the finest topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple{\tau_i, \tau}$-continuous.
== Proof ==
From Final Topology is Topology, $\tau$ is a topology.
==== Mappings are continuous ====
Let $U \in \tau$.
Let $i \in I$.
Then $\map {f_i^{-1}} {U} \in \tau_i$ by definition of $\tau$.
It follows that for each $i \in I$, $f_i: Y_i \to X$ is $\tuple {\tau_i, \tau}$-continuous.
==== $\tau$ is the finest such topology ====
Let $\struct{X, \vartheta}$ be a topological space.
Let the mappings $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be $\tuple {\tau_i, \vartheta}$-continuous.
Let $U \in \vartheta$.
By definition of continuity, for every $i \in I$:
:$\map {f_i^{-1} } U \in \tau_i$
Then by definition of $\tau$:
:$U \in \tau$
It follows that:
:$\vartheta \subseteq \tau$
That is, $\tau$ is finer than $\vartheta$.
Category:Final Topology
Equivalence of Definitions of Final Topology/Definition 2 Implies Definition 1

== Theorem ==
Let $X$ be a set.
Let $I$ be an indexing set.
Let $\family {\struct{Y_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces indexed by $I$.
Let $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
Let $\tau$ be the finest topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple{\tau_i, \tau}$-continuous.
Then:
:$\tau = \set{U \subseteq X: \forall i \in I: \map {f_i^{-1} } U \in \tau_i}$
== Proof ==
Let $\tau' = \set{U \subseteq X: \forall i \in I: \map {f_i^{-1} } U \in \tau_i}$.
==== $\tau'$ contains $\tau$ ====
Let $U \in \tau$.
By definition of $\tuple {\tau_i, \tau}$-continuity for each $i \in I$:
:$\forall i \in I : \map {f_i^{-1} } U \in \tau_i$
So:
:$U \in \tau'$
Since $U$ was arbitrary:
:$\tau \subseteq \tau'$
==== $\tau$ contains $\tau'$ ====
From Final Topology is Topology then $\tau'$ is a topology.
Let $U \in \tau'$.
Let $i \in I$.
Then $\map {f_i^{-1}} {U} \in \tau_i$ by definition of $\tau'$.
It follows that for each $i \in I$, $f_i: Y_i \to X$ is $\tuple{\tau_i, \tau'}$-continuous.
So $\tau'$ is a topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple {\tau_i, \tau'}$-continuous.
Since $\tau$ is the finest topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple {\tau_i, \tau}$-continuous then:
:$\tau' \subseteq \tau$
By definition of set equality:
:$\tau = \tau'$
Category:Final Topology
Equivalence of Definitions of Finer Topology

== Theorem ==
Let $S$ be a set.
Let $\tau_1$ and $\tau_2$ be topologies on $S$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $I_S: \struct {S, \tau_1} \to \struct {S, \tau_2}$ be the identity mapping on $S$.
Then:
$\quad \; \leadstoandfrom \: \: I_S$ is continuous, by definition of a continuous mapping, which is .
Category:Topology
Equivalence of Definitions of Finite Cyclic Group

== Theorem ==
=== Definition $1$ ===
=== Definition $2$ ===
== Proof ==
=== Definition $(1)$ implies Definition $(2)$ ===
Let $\struct {G, \circ}$ be a finite cyclic group by definition $1$.
Then by definition, $\struct {G, \circ}$ is both cyclic and finite.
By definition of cyclic group:
:$G = \gen a$
for some $a \in G$.
Hence by definition of group generator:
:$\forall n \in \N: a^n \in G$
As $G$ is finite:
:$\exists r, s \in \N: a^r = a^s$
such that $r \ne s$.
, suppose $r > s$.
Then:
Thus $\struct {G, \circ}$ is a finite cyclic group by definition $2$.
=== Definition $(2)$ implies Definition $(1)$ ===
Let $\struct {G, \circ}$ be a finite cyclic group by definition $2$.
Then, by definition:
:$\exists n \in \N: a^n = e$
Again, by definition of cyclic group and group generator:
:$\forall g \in G: \exists m \in \N: g = a^m$
By the Division Theorem:
:$m = q n + r$
for some $q \in \N$ and $0 \le r < n$.
Thus:
That is, every element of $G$ is in the form $a^r$ where $0 \le r < n$.
That is, there exist no more than $n$ elements in $G$.
Thus $\struct {G, \circ}$ is a finite cyclic group by definition $1$.
Category:Finite Cyclic Groups
Equivalence of Definitions of Finite Galois Extension

== Theorem ==
Let $L / K$ be a finite field extension.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== 1 implies 2 ===
Note that by Finite Field Extension has Finite Galois Group, $G = \Aut {L / K}$ is finite.
Let $\alpha \in L$.
Then its orbit under $G$ is finite.
By:
:Minimal Polynomial of Element with Finite Orbit under Group of Automorphisms over Fixed Field in terms of Orbit
its minimal polynomial over $K$ splits completely in $L$.
Thus $L / K$ is normal.
By:
:Finite Orbit under Group of Automorphisms of Field implies Separable over Fixed Field
$L / K$ is separable.
=== 2 implies 3 ===
Since $L / K$ is Galois, it is separable.
Thus, by the Primitive Element Theorem, there exists an $\alpha \in L$ such that $L = \map K \alpha$.
Let $m_\alpha \in K \sqbrk x$ be the minimal polynomial of $\alpha$ over $K$.
Then:
:$\index L K = \map \deg {m_\alpha}$
Suppose $\sigma \in \Gal {L / K}$.
Then:
:$\map {m_\alpha} {\map \sigma \alpha} = \map \sigma {\map {m_\alpha} \alpha} = \map \sigma 0 = 0$
since $m_\alpha$ has coefficients in $K$.
Therefore $\map \sigma \alpha$ must be a root of $m_\alpha$.
Every element of $\Gal {L / K}$ is determined by its value at $\alpha$ by our assumption that $L = \map K \alpha$. 
Therefore:
:$\order {\Gal {L / K} } \le \map \deg {m_\alpha} = \index L K$
Next, suppose $\beta$ is a root of $m_\alpha$.
By the normality of $L / K$, we must have $\beta \in L$.
Then, by Abstract Model of Algebraic Extensions:
:$\map K \alpha \cong K \sqbrk x / \gen {m_\alpha} \cong \map K \beta$
Composing isomorphisms we have an automorphism of $L$ for each $\beta$.
Thus:
:$\order {\Gal {L / K} } \ge \map \deg {m_\alpha} = \index L K$
from which our result follows.
Category:Finite Galois Extensions
Equivalence of Definitions of Finite Order Element

== Theorem ==
Let $G$ be a group whose identity is $e_G$.
Let $x \in G$ be an element of $G$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== $(1)$ implies $(2)$ ===
Let $x$ be a finite order element of $G$ by definition 1.
Then by definition there exists $k \in \Z_{>0}$ such that $x^k = e_G$.
Consider some $m, n \in \Z_{>0}$ such that $m = n + k$.
Thus $x$ is a finite order element of $G$ by definition 2.
=== $(2)$ implies $(1)$ ===
Let $x$ be a finite order element of $G$ by definition 2.
That is, there exists $m, n \in \Z_{>0}$ such that $x^m = x^n$ but $m \ne n$.
, suppose that $m > n$.
Let $k = m - n$.
From $x^m = x^n$ it follows from Powers of Group Elements that:
Thus there exists $k \in \Z_{>0}$ such that $x^k = e_G$.
Thus $x$ is a finite order element of $G$ by definition 1.
Category:Order of Group Elements
Equivalence of Definitions of Floor Function

== Theorem ==
Let $x$ be a real number.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== Definition 1 equals Definition 2 ===
Follows from Supremum of Set of Integers equals Greatest Element.
=== Definition 1 equals Definition 3 ===
Let $S$ be the set:
:$S = \set {m \in \Z: m \le x}$
Let $n = \sup S$.
By Supremum of Set of Integers is Integer, $n \in \Z$.
By Supremum of Set of Integers equals Greatest Element, $n\in S$.
Because $n \in S$, we have $n \le x$.
Because $n + 1 > n$, we have by definition of supremum:
:$n + 1 \notin S$
Thus $n + 1 > x$.
Thus $n$ is an integer such that:
:$n \le x < n + 1$
So $n$ is the floor function by definition 3.
=== Definition 3 equals Definition 2 ===
Let $n$ be an integer such that:
:$n \le x < n + 1$
We show that $n$ is the greatest element of the set:
:$S = \set {m \in \Z: m \le x}$
Let $m \in \Z$ such that $m \le x$.
We show that $n \ge m$.
 $m > n$.
By Weak Inequality of Integers iff Strict Inequality with Integer plus One:
:$m \ge n + 1$
and so from the definition of $g$ it follows that $m > x$.
By Proof by Contradiction it follows that $m \le n$.
Because $m \in S$ was arbitrary, $n$ is the greatest element of $S$.
Thus $n$ is the floor function by definition 2.
== Sources ==
* : $\S 10$: The well-ordering principle
Category:Floor Function
Equivalence of Definitions of Folium of Descartes

== Theorem ==
=== Cartesian Form ===
=== Parametric Form ===
== Proof ==
Let $F$ be a folium of Descartes expressed in parametric form.
Then by definition:
Hence:
Thus $F$ is a folium of Descartes expressed in Cartesian form.
Category:Folium of Descartes
Equivalence of Definitions of Gamma Function

== Theorem ==
=== Integral Form ===
=== Weierstrass Form ===
=== Hankel Form ===
=== Euler Form ===
== Proof ==
=== Weierstrass Form equivalent to Euler Form ===
First it is shown that the Weierstrass form is equivalent to the Euler form.
Combining the limits:
 
But:
:$(1): \quad m = \dfrac {m!} {\paren {m - 1}!} = \dfrac 2 1 \cdot \dfrac 3 2 \cdots \dfrac {x + 1} x \cdots \dfrac m {m - 1}$
Each term in $(1)$ is just $\dfrac {x + 1} x = 1 + \dfrac 1 x$, so:
:$\ds m = \prod_{n \mathop = 1}^{m - 1} \paren {1 + \frac 1 n}$
Thus the expression for $\dfrac 1 {\map \Gamma z}$ becomes:
 
Hence:
:$\ds \map \Gamma z = \frac 1 z \prod_{n \mathop = 1}^\infty \paren {1 + \frac 1 n}^z \paren {1 + \frac z n}^{-1}$
which is the Euler form of the Gamma function.
=== Integral Form equivalent to Euler Form ===
This is proved in the page:
:Integral Form of Gamma Function equivalent to Euler Form
== Sources ==
* : $\S 1.2.7$: Harmonic Numbers: Exercise $24$
Category:Gamma Function
Category:Equivalence of Definitions of Gamma Function
Equivalence of Definitions of Gaussian Prime

== Theorem ==
=== Definition $1$ ===
=== Definition $2$ ===
== Proof ==
Let $x = a + b i$ be a Gaussian integer.
We have:
Thus it is seen that every Gaussian integer has $8$ divisors which are themselves Gaussian integers.
=== Definition $(1)$ implies Definition $(2)$ ===
Let $x$ be a Gaussian prime by definition $1$.
Then by definition:
:$x$ cannot be expressed as the product of two Gaussian integers, neither of which is a unit (that is, $\pm 1$ or $\pm i$).
That is, the only divisors of $x$ are those $8$ which have been identified above.
Thus $p$ is a Gaussian prime by definition $2$.
=== Definition $(2)$ implies Definition $(1)$ ===
Let $p$ be a Gaussian prime by definition $2$.
Then by definition $p$ has exactly $8$ divisors which are Gaussian integers.
Those are the ones given above.
As those are the only ones, $p$ cannot be the product of two Gaussian integers such that both of them are not a unit.
Thus $p$ is a Gaussian prime by definition $1$.
Category:Gaussian Primes
Equivalence of Definitions of Generalized Ordered Space

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\tau$ be a topology for $S$.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== Definition $(1)$ implies Definition $(3)$ ===
=== Definition $(3)$ implies Definition $(1)$ ===
=== Definition $(2)$ implies Definition $(1)$ ===
=== Definition $(3)$ implies Definition $(2)$ ===
This follows from GO-Space Embeds Densely into Linearly Ordered Space.
Category:Generalized Ordered Spaces
Category:Equivalence of Definitions of Generalized Ordered Space
Equivalence of Definitions of Generalized Ordered Space/Definition 1 implies Definition 3

== Theorem ==
Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 1:
Then $\struct {S, \preceq, \tau}$ is a generalized ordered space by Definition 3:
== Proof ==
Let $\BB$ be a basis for $\tau$ consisting of 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 Convex Set Characterization (Order Theory), each element of $\BB$ is the intersection of its upper closure with its lower closure.
Thus each element of $\BB$ is generated by $\SS$.
Thus $\SS$ is a sub-basis for $\tau$.
Category:Equivalence of Definitions of Generalized Ordered Space
Equivalence of Definitions of Generalized Ordered Space/Definition 2 implies Definition 1

== Theorem ==
Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 2:
Then $\struct {S, \preceq, \tau}$ is a generalized ordered space by Definition 1:
== Proof ==
Let $x \in U \in \tau$.
Then by the definition of topological embedding:
:$\map \phi U$ is an open neighborhood of $\map \phi x$ in $\map \phi S$ with the subspace topology.
Thus by Basis for Topological Subspace and the definition of the order topology, there is an open interval or open ray $I' \in \tau'$ such that:
:$\map \phi x \in I' \cap \map \phi S \subseteq \map \phi U$
Since $I'$ is an interval or ray, it is convex in $S'$ by Interval of Ordered Set is Convex or Ray is Convex, respectively.
Then:
Because $\phi$ is a topological embedding, it is injective by definition.
So:
:$\phi^{-1} \sqbrk {\phi \sqbrk U} = U$
Thus:
:$x \in \phi^{-1} \sqbrk {I'} \subseteq U$
By Inverse Image of Convex Set under Monotone Mapping is Convex:
:$\phi^{-1} \sqbrk {I'}$ is convex.
Thus $\tau$ has a basis consisting of convex sets.
Category:Equivalence of Definitions of Generalized Ordered Space
Equivalence of Definitions of Generalized Ordered Space/Definition 3 implies Definition 1

== Theorem ==
Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 3:
Then $\struct {S, \preceq, \tau}$ is a generalized ordered space by Definition 1:
== Proof ==
Let $\SS$ be a sub-basis for $\tau$ consisting of upper sections and lower sections.
Let $\BB$ be the set of intersections of finite subsets of $\SS$.
By Upper Section is Convex, Lower Section is Convex and Intersection of Convex Sets is Convex Set (Order Theory) :
:the elements of $\BB$ are convex.
But $\BB$ is a basis for $\tau$.
Therefore $\tau$ has a basis consisting of convex sets.
Category:Equivalence of Definitions of Generalized Ordered Space