nyuuzyou/wikis huggingface dataset:
Equivalence of Definitions of Unital Associative Commutative Algebra/Correspondence

== Theorem ==
Let $A$ be a commutative ring with unity.
Let $B$ be a algebra over $A$ that is unital, associative and commutative.
Let $\struct {C, f}$ be a ring under $A$.
:$(1): \quad C$ is the underlying ring of $B$ and $f: A \to C$ is the canonical homomorphism to the unital algebra $B$.
:$(2): \quad B$ is the algebra defined by $f$.
== Proof ==
Let $\cdot: A \times B \to B$ the ring action of $B$.
=== $(1)$ implies $(2)$ ===
Let $C$ equal the underlying ring of $B$ and $f: A \to C$ equal the canonical mapping to the unital algebra $B$.
We show that $B$ is the algebra defined by $f$.
==== Addition ====
By definition of the underlying ring of $B$, the addition of $C$ is the addition of $B$, say $+$.
By definition of the module defined by $f$, the addition of the algebra defined by $f$ is also $+$.
==== Multiplication ====
By definition of the underlying ring of $B$, the multiplication of $C$ is the ring product of $B$, say $\times$.
By definition of the algebra defined by $f$, its multiplication is also $\times$.
==== Ring action ====
It remains to show that the ring action $\cdot$ of $B$ is the ring action $*$ of the module defined by $f$.
We have, for $a \in A$ and $b \in B$:
=== 2 implies 1 ===
Let $B$ equal the algebra defined by $f$.
==== Addition ====
By definition of the module defined by $f$, the addition of $B$ is the addition of $C$, say $+$.
By definition of the underlying ring of $B$, its addition is also $+$.
==== Multiplication ====
By definition of the algebra defined by $f$, the multiplication of $B$ is the ring product of $C$, say $\times$.
By definition of the underlying ring of $B$, its multiplication is also $\times$.
Thus $C$ is the underlying ring of $B$.
==== Homomorphism ====
By Identity is Unique, the unit $1_B$ of $B$ equals the unity $1_C$ of $C$.
Let $g: A \to B$ be the canonical mapping.
We show that $g = f$.
We have, for $a \in A$:
Category:Equivalence of Definitions of Unital Associative Commutative Algebra
Equivalence of Definitions of Unital Associative Commutative Algebra/Homomorphisms

== Definition ==
Let $A$ be a commutative ring with unity.
Let $\struct {B, f}$ and $\struct {C, g}$ be rings under $A$.
Let $h: B \to C$ be a mapping.
:$(1): \quad h$ is a morphism of rings under $A$.
:$(2): \quad h$ is a unital algebra homomorphism from the algebra defined by $f$ to the algebra defined by $g$.
== Proof ==
Category:Equivalence of Definitions of Unital Associative Commutative Algebra
Equivalence of Definitions of Unital Subalgebra

== Theorem ==
Let $R$ be a commutative ring.
Let $\struct {A_R, *}$ be an unital algebra over $R$ whose unit is $1_A$.
Let $\struct {B_R, *}$ be a subalgebra of $A_R$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Category:Unital Subalgebras
Equivalence of Definitions of Unsigned Stirling Numbers of the First Kind

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
in the sense that the coefficients of the powers in the summand are uniquely defined by the given recurrence relation.
== Proof ==
The proof proceeds by induction.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:the coefficients of the powers in the expression $\ds x^{\underline n} = \sum_k \paren {-1}^{n - k} {n \brack k} x^k$ are uniquely defined by $\ds {n \brack k} = {n - 1 \brack k - 1} + \paren {n - 1} {n - 1 \brack k}$
where $\ds {n \brack k} = \delta_{n k}$ where $k = 0$ or $n = 0$.
First the case where $n = 0$ is attended to.
From Unsigned Stirling Number of the First Kind of 0 we have:
:$\ds {0 \brack k} = \delta_{0 k}$
Hence the result holds for $n = 0$.
=== Basis for the Induction ===
$\map P 1$ is the case:
We have:
Then:
Thus, in the expression:
:$\ds x^{\underline k} = \sum_k \paren {-1}^{1 - k} {1 \brack k} x^1$
we have:
:$\ds \paren {-1}^{1 - k} {1 \brack k} = 1$
and for all $k \in \Z$ where $k \ne 1$:
:$\ds \paren {-1}^{1 - k} {1 \brack k} = 0$
That is:
:$\ds \paren {-1}^{1 - k} {1 \brack k} = \delta_{1 k}$
Thus $\map P 1$ 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 1$, then it logically follows that $\map P {r + 1}$ is true.
So this is the induction hypothesis:
:The coefficients in the expression $\ds x^{\underline r} = \sum_k \paren {-1}^{r - k} {r \brack k} x^k$ are uniquely defined by $\ds {r \brack k} = {r - 1 \brack k - 1} + \paren {r - 1} {r - 1 \brack k}$
from which it is to be shown that:
:The coefficients in the expression $\ds x^{\underline {r + 1} } = \sum_k \paren {-1}^{r + 1 - k} {r + 1 \brack k} x^k$ are uniquely defined by $\ds {r + 1 \brack k} = {r \brack k - 1} + r {r \brack k}$
=== Induction Step ===
This is the induction step:
Thus the coefficients of the falling factorial powers are defined by the recurrence relation:
:$\ds {r + 1 \brack k} = {r \brack k - 1} + r {r \brack k}$
as required.
So $\map P r \implies \map P {r + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:for all $n \in \Z_{\ge 0}$, the coefficients of the powers in the expression $\ds x^{\underline n} = \sum_k \paren {-1}^{n - k} {n \brack k} x^k$ are uniquely defined by:
::$\ds {n \brack k} = {n - 1 \brack k - 1} + \paren {n - 1} {n - 1 \brack k}$
:where $\ds {n \brack k} = \delta_{n k}$ when $k = 0$ or $n = 0$.
== Also see ==
* Equivalence of Definitions of Signed Stirling Numbers of the First Kind
* Equivalence of Definitions of Stirling Numbers of the Second Kind
== Sources ==
* : $\S 1.2.6$: Binomial Coefficients: Exercise $35$
Category:Stirling Numbers
Equivalence of Definitions of Upper Section

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $U \subseteq S$.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Suppose that:
:$\forall u \in U: \forall s \in S: u \preceq s \implies s \in U$
Let $k \in U^\succeq$.
Then by the definition of upper closure, there is some $u \in U$ such that $u \preceq k$.
Since $k \in U^\succeq \subseteq S$, the premise proves that $k \in U$.
Since this holds for all $k \in U^\succeq$, it follows that:
: $U^\succeq \subseteq U$
=== Definition 2 implies Definition 3 ===
Suppose that $U^\succeq \subseteq U$.
Let $u \in U$.
Then since $U \subseteq S$, $u \in S$ by the definition of subset.
Since $\preceq$ is reflexive:
:$u \preceq u$
Thus by the definition of upper closure:
:$u \in U^\succeq$.
Since this holds for all $u \in U$:
:$U \subseteq U^\succeq$
Thus by definition of set equality:
:$U^\succeq = U$
=== Definition 3 implies Definition 1 ===
Suppose that $U^\succeq = U$.
Let $u \in U$.
Let $s \in S$.
Let $u \preceq s$.
Then by the definition of upper closure, $s \in U$.
Thus we have shown that:
:$\forall u \in U: \forall s \in S: u \preceq s \implies s \in U$
Category:Upper Sections
Equivalence of Definitions of Upper Wythoff Sequence

== Theorem ==
The following definitions of the upper Wythoff sequence are equivalent:
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
From Beatty's Theorem, the Beatty sequences $\BB_r$ and $\BB_s$ are complementary :
:$\dfrac 1 r + \dfrac 1 s = 1$
It remains to be demonstrated that this holds for $r = \phi$ and $s = \phi^2$.
Thus:
Hence the result.
Category:Beatty Sequences
Equivalence of Definitions of Variance of Discrete Random Variable

== Theorem ==
Let $X$ be a discrete random variable.
Let $\mu = \expect X$ be the expectation of $X$.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== Definition 1 equivalent to Definition 2 ===
Let $\var X$ be defined as:
:$\var X := \expect {\paren {X - \expect X}^2}$
Let $\mu = \expect X$.
Let $\map f X = \paren {X - \mu}^2$ be considered as a function of $X$.
Then by applying Expectation of Function of Discrete Random Variable:
:$\ds \expect {\map f X} = \sum_{x \mathop \in \Omega_X} \map f x \, \map \Pr {X = x}$
which leads to:
:$\ds \expect {\paren {X - \mu}^2} = \sum_{x \mathop \in \Omega_X} \paren {\paren {X - \mu}^2} \map \Pr {X = x}$
thus demonstrating the equality of Definition 1 to Definition 2.
=== Definition 2 equivalent to Definition 3 ===
Let $\mu = \expect X$, and take the expression for variance:
:$\ds \var X := \sum_{x \mathop \in \Img X} \paren {x - \mu}^2 \map \Pr {X = x}$
Then from Variance as Expectation of Square minus Square of Expectation:
:$\var X = \expect {X^2} - \paren {\expect X}^2$
== Sources ==
* : $\S 2.4$: Expectation
Category:Variance
Equivalence of Definitions of Variation of Signed Measure

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
We aim to prove that for each $A \in \Sigma$, we have: 
:$\ds \map {\mu^+} A + \map {\mu^-} A = \sup \set {\sum_{j \mathop = 1}^n \cmod {\map \mu {A_j} } : \set {A_1, A_2, \ldots, A_n} \in \map P A}$
Let $\tuple {P, N}$ be a Hahn decomposition for $\mu$.
Then $\set {P \cap A, N \cap A}$ is a finite partition of $A$ into $\Sigma$-measurable sets.
Then, we have from the definition of Jordan decomposition:
:$\map \mu {P \cap A} = \map {\mu^+} A \ge 0$
and:
:$\map \mu {N \cap A} = -\map {\mu^-} A \le 0$
Then: 
:$\cmod {\map \mu {P \cap A} } = \map {\mu^+} A$
and:
:$\cmod {\map \mu {N \cap A} } = \map {\mu^-} A$
so:
Conversely, for each $\set {A_1, A_2, \ldots, A_n} \in \map P A$, we have:
so:
:$\ds \sup \set {\sum_{j \mathop = 1}^n \cmod {\map \mu {A_j} } : \set {A_1, A_2, \ldots, A_n} \in \map P A} \le \map {\mu^+} A + \map {\mu^-} A$
so:
:$\ds \map {\mu^+} A + \map {\mu^-} A = \sup \set {\sum_{j \mathop = 1}^n \cmod {\map \mu {A_j} } : \set {A_1, A_2, \ldots, A_n} \in \map P A}$
Category:Variation of Signed Measure
Equivalence of Definitions of Vector Cross Product

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\mathbf a \times \mathbf b$ be a vector cross product by definition $2$.
Then by definition:
:$(1): \quad \mathbf a \times \mathbf b = \norm {\mathbf a} \norm {\mathbf b} \sin \theta \, \mathbf {\hat n}$
By Angle Between Vectors in Terms of Dot Product:
:$\cos \theta = \ds \frac {\mathbf a \cdot \mathbf b} {\norm {\mathbf a} \norm {\mathbf b} }$
:
Note that $\theta$ is measured from $0$ to $\pi$.
If $\dfrac \pi 2 < \theta < \pi$, the dot product is negative and it exists in quadrant $2$.
The sine ratio is unaltered.
This gives:
Next we have:
Then:
Hence:
To simplify subsequent algebra, let us define $u$:
Let $\mathbf {\hat n} = \begin {bmatrix} n_i \\ n_j \\ n_k \end {bmatrix}$
Now, by definition $2$ of the cross product:
Hence by definition of dot product:
Then:
Substituting from $(12)$ into $(11)$:
and from $(12)$ into $(10)$:
Hence from $(12)$, $(13)$ and $(14)$ we have the components of $\mathbf {\hat n}$:
Substituting back into $(5)$:
Hence the result.
== Sources ==
* : Chapter $\text {II}$: The Products of Vectors: $6$. Application to Vector Products
* : Chapter $\text I$: Vector Algebra: $\S 3$: $(9)$
Category:Vector Cross Product
Equivalence of Definitions of Vector Projection

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== $(2) \iff (3)$ ===
=== $(1) \iff (3)$ ===
By definition $1$ of vector projection:
:$\proj_\mathbf v \mathbf u$ is a like vector to $\mathbf v$ whose length is $\norm {\mathbf u} \cos \theta$
This is obtained by creating a vector quantity:
:$\paren {\norm {\mathbf u} \cos \theta} \mathbf {\hat v}$
where $\mathbf {\hat v}$ is the unit vector in the direction of $\mathbf v$.
But by :
:$u_{\parallel \mathbf v} = \norm {\mathbf u} \cos \theta$
Category:Vector Projections
Equivalence of Definitions of Vector Sum

== Theorem ==
=== Component Definition ===
=== Triangle Law ===
== Proof ==
Let the Cartesian coordinate system be selected such that $\mathbf u$ and $\mathbf v$ are embedded in the $x$-$y$ plane.
Then:
and all other components, if there are any, are then zero.
Thus by the component definition:
:$\mathbf u + \mathbf v = \tuple {u_1 + v_1, u_2 + v_2}$
Now we use the triangle law:
:
Let:
Thus we have:
It is seen that $\mathbf u + \mathbf v$ calculated using the triangle law is the same as $\mathbf u + \mathbf v$ calculated using the component definition.
Category:Vector Addition
Equivalence of Definitions of Weak Convergence on Topological Vector Space

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $X$ be a topological vector space over $\GF$. 
Let $X^\ast$ be the topological dual space of $X$.
Suppose that: 
:for each $x, y \in X$ with $x \ne y$, there exists $f \in X^\ast$ such that $\map f x \ne \map f y$. 
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $X$. 
Let $x \in X$. 
=== Definition 1 ===
 
=== Definition 2 ===
 
== Proof ==
=== Definition 1 implies Definition 2 ===
Suppose that $\sequence {x_n}_{n \mathop \in \N}$ converges in $\struct {X, w}$.
Let $f \in X^\ast$ and $\epsilon > 0$. 
We want to show that: 
:$\map f {x_n} \to \map f x$ in $\GF$. 
Let $\map {B_r} {\lambda, \GF}$ be the open ball in $\GF$ of radius $r$ and Centre $\lambda$.
From Characterization of Continuity of Linear Functional in Weak Topology, we have that $f$ is continuous in $\struct {X, w}$.
From the definition of the initial topology, we then have: 
:$f^{-1} \sqbrk {\map {B_r} {\map f x, \GF} }$ is weakly open for each $r > 0$ and $x \in X$.
So by the definition of convergence in $\struct {X, w}$, there exists $N \in \N$ such that: 
:$x_n \in f^{-1} \sqbrk {\map {B_r} {\map f x, \GF} }$ for $n \ge N$. 
Then: 
:$\map f {x_n} \in \map {B_r} {\map f x, \GF}$ for $n \ge N$
so that: 
:$\cmod {\map f {x_n} - \map f x} < \epsilon$
Since $\epsilon$ was arbitrary, we have: 
:$\map f {x_n} \to \map f x$ in $\GF$.
=== Definition 2 implies Definition 1 ===
Suppose that:
:for each $f \in X^\ast$ we have $\map f {x_n} \to \map f x$ in $\GF$. 
Let $U$ be a weak open neighborhood of $x$. 
We aim to show that there exists $N \in \N$ such that $x_n \in U$ for $n \ge N$. 
From Initial Topology on Vector Space Generated by Linear Functionals is Locally Convex, the initial topology $w$ is induced as a locally convex space by: 
:$\set {p_f : f \in X^\ast}$
where $p_f : X \to \hointr 0 \infty$ is defined by: 
:$\map {p_f} x = \cmod {\map f x}$ 
for each $x \in X$.
From Open Sets in Standard Topology of Locally Convex Space, there exists $f_1, f_2, \ldots, f_n \in X^\ast$ and $\epsilon > 0$ such that: 
:$\set {y \in X : \cmod {\map {f_i} y - \map {f_i} x} < \epsilon \text { for each } 1 \le i \le n} \subseteq U$
Since $\map {f_i} {x_n} \to \map {f_i} x$ for each $1 \le i \le n$, for each $1 \le i \le n$ there exists $N_i \in \N$ such that: 
:$\cmod {\map {f_i} {x_n} - \map {f_i} x} < \epsilon$ 
Set:
:$\ds N = \max_{1 \le i \le n} N_i$ 
Then, for $n \ge N$ we have: 
:$\cmod {\map {f_i} {x_n} - \map {f_i} x} < \epsilon$ for each $1 \le i \le n$. 
That is, for $n \ge N$ we have: 
:$x_n \in \set {y \in X : \cmod {\map {f_i} y - \map {f_i} x} < \epsilon \text { for each } 1 \le i \le n}$
and so $x_n \in U$, as required.
Category:Weak Convergence (Topological Vector Spaces)
Category:Weak Topologies on Topological Vector Spaces
Equivalence of Definitions of Weakly Locally Connected at Point

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x \in S$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
=== Definition 2 implies Definition 1 ===
Category:Locally Connected Spaces
Category:Equivalence of Definitions of Weakly Locally Connected at Point
Equivalence of Definitions of Weakly Locally Connected at Point/Definition 1 implies Definition 2

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x \in S$.
Let $x$ have a neighborhood basis consisting of connected sets.
Then:
:Every open neighborhood $U$ of $x$ contains an open neighborhood $V$ of $x$ such that every two points of $V$ lie in some connected subset of $U$.
== Proof ==
Let $U$ be an open neighborhood of $x$.
By assumption there exists a connected neighborhood $C$ of $x$ such that $C \subseteq U$.
By definition of a neighborhood, there exists an open neighborhood $V$ of $x$ such that $V \subseteq C$.
From Subset Relation is Transitive, $V \subseteq U$.
By definition of a subset:
:$\forall y, z \in V: y, z \in C$
The result follows.
Category:Equivalence of Definitions of Weakly Locally Connected at Point
Equivalence of Definitions of Weakly Locally Connected at Point/Definition 2 implies Definition 1

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x \in S$.
Let every open neighborhood $U$ of $x$ contain an open neighborhood $V$ of $x$ such that every two points of $V$ lie in some connected subset of $U$.
Then:
:$x$ has a neighborhood basis consisting of connected sets.
== Proof ==
Let $\BB = \set {B \subseteq S: B \text{ is a connected neighborhood of } x}$
It will be shown that $\BB$ is a neighborhood basis consisting of connected sets.
Let $N$ be any neighborhood of $x$.
By definition of a neighborhood there exists an open neighborhood $U$ of $x$ such that $U \subseteq N$
By assumption there exists an open neighborhood $V$ of $x$ such that every two points of $V$ lie in some connected subset of $U$.
For each $y \in V, y \ne x$, let $C_y$ be a connected subset of $U$ such that $x, y \in C_y \subseteq U$.
Let $C = \set x \cup \bigcup \set {C_y:y \in V, y \ne x}$
From Singleton is Connected in Topological Space, $\set x$ is connected.
From Union of Connected Sets with Common Point is Connected, $C$ is a connected subset.
From Union is Smallest Superset, $C \subseteq U \subseteq N$.
Now $x \in C$ and for each $y \in V, y \ne x$ then $y \in C_y \subseteq C$.
Hence $V \subseteq C$.
By definition of a neighborhood, $C$ is a connected neighborhood of $x$.
That is, $C \in \BB$.
Since $N$ was an arbitrary neighborhood of $x$, it follows that $\BB$ is a neighborhood basis of $x$ consisting of connected sets.
Category:Equivalence of Definitions of Weakly Locally Connected at Point
Equivalence of Definitions of Weierstrass E-Function

== Theorem ==
Let $\mathbf y, \mathbf z, \mathbf w$ be $n$-dimensional vectors.
Let $\mathbf y$ be such that $\map{\mathbf y} a=A$ and $\map{\mathbf y} b=B$.
Let $J$ be a functional such that:
:$\ds J \sqbrk {\mathbf y} = \int_a^b \map F {x, \mathbf y, \mathbf y'} \rd x$
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
By Definition 1:
:$\map E {x, \mathbf y, \mathbf z, \mathbf w} = \map F {x, \mathbf y, \mathbf w} - \map F {x, \mathbf y, \mathbf z} + \paren {\mathbf w - \mathbf z} \map {F_{\mathbf y'} } {x, \mathbf y, \mathbf z}$
By Taylor's Theorem, where expansion is done around $\mathbf w = \mathbf z$ and Lagrange form of remainder is used:
:$\ds \map F {x, \mathbf y, \mathbf w} = \map F {x, \mathbf y, \mathbf z} + \frac {\partial \map F {x, \mathbf y, \mathbf z} } {\partial \mathbf y'} \paren {\mathbf w - \mathbf z} + \frac 1 2 \sum_{i, j \mathop = 1}^n \paren {w_i - z_i} \paren {w_j - z_j} \frac {\partial^2 \map F {x, \mathbf y, \mathbf z + \theta \paren {\mathbf z - \mathbf w} } } {\partial y_i'y_j'}$
where $\theta \in \R: 0 < \theta < 1$.
Insertion of this expansion into the definition for Weierstrass E-Function leads to the desired result.
=== Definition 2 implies Definition 1 ===
== Sources ==
* : $\S 6.34$: The Weierstrass E-Function. Sufficient Conditions for a Strong Extremum
Category:Calculus of Variations
Equivalence of Definitions of Weight of Topological Space

== Theorem ==
Let $T$ be a topological space.
Let $\mathbb B$ be the set of all bases of $T$.
The following definitions of the weight of $T$ are equivalent:
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
By Class of All Cardinals is Subclass of Class of All Ordinals, the set:
:$M = \set {\card \BB: \BB \in \mathbb B}$
is a subclass of the class of all ordinals.
By Class of All Ordinals is Well-Ordered by Subset Relation:
:$M$ is well ordered by the $\subseteq$ relation.
By Class of All Ordinals is Well-Ordered by Subset Relation there exists a smallest element $m_0 \in M$:
:$\forall m \in M: m_0 \subseteq m$
Hence by Smallest Element is Minimal there exists a basis $\BB_0$ of $T$ which has minimal cardinality:
:$m_0 = \map {w_2} T$.
Let:
:$\ds \map {w_1} T = \bigcap_{\BB \mathop \in \mathbb B} \card \BB$
By Intersection is Subset:
:$\ds \map {w_1} T = \bigcap M \subseteq m_0$
But by Intersection is Largest Subset:
:$\ds \mathfrak m_0 \subseteq \bigcap M$
By definition of set equality:
:$\map {w_1} T = \map {w_2} T$
and hence the result.
== Sources ==
* 
Category:Topology
Equivalence of Definitions of Well-Founded Relation

== Theorem ==
Let $\struct {S, \RR}$ be a Relational Structure.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
By definition of minimal element:
:$\forall y \in T: y \preceq x \implies x = y$
=== $(1)$ implies $(2)$ ===
Let $\RR$ be a well-founded relation by definition $1$.
Then by definition:
:$\forall T \subseteq S: T \ne \O: \exists z \in T: \forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
So, let $T \subseteq S: T \ne \O$.
That is, $T$ is a non-empty subset of $S$.
It is asserted that there exists $z \in T \setminus \set z$ such that:
:$\forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
This does not exclude the case that $\tuple {z, z} \in \RR$.
So if there exists $y \in T$ such that $\tuple {y, z} \in \RR$, then it must be the case that $y = z$
That is:
:$\forall y \in T: \tuple {y, z} \in \RR \implies y = z$
That is, $z$ is a minimal element of $T$ under $\RR$.
So we have shown that:
:for every non-empty subset $T$ of $S$, there exists an element $z$ in $T$ such that $z$ is a minimal element of $T$.
Thus $\RR$ is a well-founded relation by definition $2$.
=== $(2)$ implies $(1)$ ===
Let $\RR$ be a well-founded relation by definition $2$.
Then by definition:
:for every non-empty subset $T$ of $S$, $T$ has a minimal element.
That is, for every non-empty subset $T$ of $S$, there exists an element $z$ in $T$ such that:
:$\forall y \in T: \tuple {y, z} \in \RR \implies y = z$
Hence:
:$\forall y \in T \setminus \set z: \tuple {y, z} \in \RR \implies y = z$
But:
:$\not \exists y \in T \setminus \set z: y = z$
and so it follows that:
:$\forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
That is:
:$\forall T \subseteq S: T \ne \O: \exists z \in T: \forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$
Thus $\RR$ is a well-founded relation by definition $1$.
Category:Well-Founded Relations
Equivalence of Definitions of Well-Ordered Integral Domain

== Theorem ==
Let $\struct {D, +, \times \le}$ be an ordered integral domain whose zero is $0_D$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== $(1)$ implies $(2)$ ===
Let $\struct {D, +, \times \le}$ be a well-ordered integral domain by definition 1.
Then by definition the ordering $\le$ is a well-ordering on the set $P$ of (strictly) positive elements of $D$.
Let $S \subseteq P$.
Thus by definition of well-ordering, $S$ has a minimal element.
Thus $\struct {D, +, \times \le}$ is a well-ordered integral domain by definition 2.
=== $(2)$ implies $(1)$ ===
Let $\struct {D, +, \times \le}$ be a well-ordered integral domain by definition 2.
Then by definition every subset $S$ of the set $P$ of (strictly) positive elements of $D$ has a minimal element:
:$\forall S \subseteq D_{\ge 0_D}: \exists x \in S: \forall a \in S: x \le a$
where $D_{\ge 0_D}$ denotes all the elements $d \in D$ such that $\map P d$.
Thus by definition $\le$ is a well-ordering of $P$.
Thus $\struct {D, +, \times \le}$ is a well-ordered integral domain by definition 1.
Category:Well-Ordered Integral Domains
Equivalence of Definitions of Well-Ordering

== Theorem ==
Let $\struct {S, \preceq}$ be a ordered set.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
By hypothesis, every subset of $S$ has a smallest element.
By Smallest Element is Minimal it follows that every subset of $S$ has a minimal element.
Thus it follows that $\preceq$ is a well-ordering on $S$ by definition 2.
=== Definition 2 implies Definition 1 ===
Let $\preceq$ be a well-ordering on $S$ by definition 2.
That is:
:$\preceq$ is a well-founded total ordering.
By definition of well-founded, every $T \subseteq S$ has a minimal element.
By Minimal Element in Toset is Unique and Smallest, every $T \subseteq S$ has a smallest element.
The result follows.
Category:Well-Orderings
Category:Equivalence of Definitions of Well-Ordering