nyuuzyou/wikis huggingface dataset:
Equivalence of Definitions of Transitive Closure of Set

== Theorem ==
Let $x$ and $y$ be sets.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $x^t$ be the transitive closure of $x$ by Definition 2.
Let the mapping $G$ be defined as on that definition page.
=== $x \in x^t$ ===
$x \in \set x$ by the definition of singleton.
Since $\map G 0 = \set 0$:
:$\set x \in \map G \N$
Thus $x \in x^t$ by the definition of union.
=== $x^t$ is a Set ===
By Denumerable Class is Set, the image of $G$ is a set.
Thus $x^t$ is a set by the Axiom of Unions.
=== $x^t$ is a Transitive Set ===
Let $y \in x^t$ and let $z \in y$.
By the definition of $x^t$:
:$\exists n \in \N: y \in \map G n$
Then by definition of union:
:$\ds z \in \bigcup \map G n$
But by the definition of $G$:
:$z \in \map G {n^+}$
Thus by the definition of $x^t$:
:$z \in x^t$
As this holds for all such $y$ and $z$, $x^t$ is transitive.
=== $x^t$ is Smallest ===
Let $m$ be a transitive set such that $x \in m$.
We will show by induction that $\map G n \subseteq m$ for each $n \in \N$.
By Union is Smallest Superset, that will show that $x^t \subseteq m$.
Because $x \in m$:
:$\map G 0 = \set x \subseteq m$
Suppose that $\map G n \subseteq m$.
Then by Union is Increasing:
:$\ds \bigcup \map G n \subseteq \bigcup m$
Thus:
:$\ds \bigcup \map G n \subseteq m$
By Smallest Element is Unique, $x^t$ is the only set satisfying $(2)$.
Category:Set Theory
Equivalence of Definitions of Transitive Relation

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $\RR$ be a relation which fulfills the condition:
:$\tuple {x, y} \in \RR \land \tuple {y, z} \in \RR \implies \tuple {x, z} \in \RR$
Then:
Thus $\RR$ is transitive by definition 2.
=== Definition 2 implies Definition 1 ===
Let $\RR$ be a relation that fulfills the condition:
:$\RR \circ \RR \subseteq \RR$
 $\RR$ does not fulfill the condition:
:$\tuple {x, y} \in \RR \land \tuple {y, z} \in \RR \implies \tuple {x, z} \in \RR$
Then:
This contradicts our statement that $\RR \circ \RR \subseteq \RR$.
Hence by Proof by Contradiction $\RR$ does fulfills the condition:
:$\tuple {x, y} \in \RR \land \tuple {y, z} \in \RR \implies \tuple {x, z} \in \RR$
Thus $\RR$ is transitive by definition 1.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 10$: Equivalence Relations: Exercise $10.6 \ \text{(c)}$
* : Chapter $\text{I}$: Sets and Functions: Relations: Theorem $3$
Category:Transitive Relations
Equivalence of Definitions of Trapezium

== Theorem ==
=== Definition $1$ ===
=== Definition $2$ ===
== Proof ==
=== Definition $(1)$ implies Definition $(2)$ ===
Let $T$ be a trapezium by definition $1$.
Then by definition $T$ has exactly one pair of sides that are parallel.
 those parallel sides of $T$ were the same length.
Then by Quadrilateral is Parallelogram iff One Pair of Opposite Sides is Equal and Parallel, $T$ is a parallelogram.
But $T$ is a trapezium, and so not a parallelogram.
Hence the two parallel sides of $T$ are unequal.
That is, $T$ is a trapezium by definition $2$.
=== Definition $(2)$ implies Definition $(1)$ ===
Let $T$ be a trapezium by definition $2$.
Then by definition $T$ has a pair of parallel sides, $AB$ and $CD$ say, that are unequal.
 the other sides of $T$ were parallel.
Then by definition $T$ would be a parallelogram.
Hence by Opposite Sides and Angles of Parallelogram are Equal, $AB = CD$.
This contradicts our supposition that $AB$ and $CD$ are unequal.
Hence by Proof by Contradiction $T$ can have only one pair of parallel sides.
Hence $T$ is a trapezium by definition $1$.
Category:Trapezia
Equivalence of Definitions of Tree

== Theorem ==
=== Definition 1===
=== Definition 2===
== Proof ==
Let $G$ be a simple graph.
=== Definition 1 implies Definition 2 ===
Let $G$ have no circuits.
As by definition a cycle is a circuit, it follows that $G$ has no cycles.
=== Definition 2 implies Definition 1 ===
Let $G$ have no cycles.
 $G$ contains a circuit $C$.
From Circuit contains Cycle as Subgraph it follows that $G$ contains a cycle.
From that contradiction it follows that $G$ can have no circuits.
Category:Tree Theory
Equivalence of Definitions of Triangular Number

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $T_n$ be a triangular number by definition 1.
Let $n = 0$.
By definition:
:$T_0 = 0$
By vacuous summation:
:$\ds T_0 = \sum_{i \mathop = 1}^0 i = 0$
By definition of summation:
:$\ds T_{n - 1} = \sum_{i \mathop = 1}^{n - 1} i = 1 + 2 + \cdots + \paren {n - 1}$
and so:
Thus $T_n$ is a triangular number by definition 2.
=== Definition 2 implies Definition 1 ===
Let $T_n$ be a triangular number by definition 2.
:$\ds T_n = \sum_{i \mathop = 1}^n i = 1 + 2 + \cdots + \paren {n - 1} + n$
Thus:
:$\ds T_{n - 1} = \sum_{i \mathop = 1}^{n - 1} i = 1 + 2 + \cdots + \paren {n - 1}$
and so:
:$T_n = T_{n - 1} + n$
Then:
:$\ds T_0 = \sum_{i \mathop = 1}^0 i$
is a vacuous summation and so:
:$T_0 = 0$
Thus $T_n$ is a triangular number by definition 1.
=== Definition 1 equivalent to Definition 3 ===
We have by definition that $T_n = 0 = \map P {3, n}$.
Then:
Thus $\map P {3, n}$ and $T_n$ are generated by the same recurrence relation.
Category:Triangular Numbers
Equivalence of Definitions of Trigonometric Series

== Theorem ==
=== Conventional Form ===
=== Complex Form ===
== Proof ==
Let $\map S x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren {a_n \cos n x + b_n \sin n x}$.
Set:
Then:
Let $b_0 := 0$.
Then let:
:$\forall n \in \N: c_n = \dfrac {a_n - i b_n} 2$
Thus it follows that:
:$c_0 = \dfrac {a_0 - 0 \times i} 2 = \dfrac {a_0} 2$
Then let:
:$c_{-n} = \dfrac {a_n + i b_n} 2$
from which it follows that:
:$c_{-n} = \overline {\paren {\dfrac {a_n - i b_n} 2} }$
and again:
:$c_0 = \dfrac {a_0 + 0 \times i} 2 = \dfrac {a_0} 2$
Then it is noted that:
:$e^{i \times 0 \times x} = e^0 = 1$
and it follows that:
where it is noted that $c_{-n} = \overline {c_n}$ as required.
== Sources ==
* : Chapter One: $\S 1$. Trigonometrical Series
Category:Trigonometric Series
Equivalence of Definitions of Ultraconnected Space

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== $(1)$ iff $(2)$ ===
Let $T = \struct {S, \tau}$ be ultraconnected by Definition 1:
:no two non-empty closed sets of $T$ are disjoint.
Let $x, y \in S$.
By Topological Closure is Closed, both $\set x^-$ and $\set y^-$ are closed.
By hypothesis:
:$\set x^- \cap \set y^- \ne \O$
That is, $T = \struct {S, \tau}$ is ultraconnected by Definition 2.
Let $T = \struct {S, \tau}$ be ultraconnected by Definition 2:
:$\forall x, y \in S: \set x^- \cap \set y^- \ne \O$
Let $V_1, V_2$ be closed sets of $T$.
Let $x \in V_1, y \in V_2$.
Then:
:$\set x^- \cap \set y^- \ne \O$
But then from Topological Closure of Subset is Subset of Topological Closure we have that:
:$\set x^- \subseteq V_1^-$
:$\set y^- \subseteq V_2^-$
But from Closed Set Equals its Closure $V_1^- = V_1, V_2^- = V_2$.
So from Intersection is Subset:
:$\set x^- \cap \set y^- \subseteq V_1$
:$\set x^- \cap \set y^- \subseteq V_2$
from which:
:$V_1 \cap V_2 \ne \O$
As $V_1$ and $V_2$ are arbitrary, it follows that $T$ is ultraconnected by Definition 1.
=== $(1)$ iff $(3)$ ===
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Ultraconnected Spaces
Equivalence of Definitions of Ultraconnected Space/1 iff 3

== Theorem ==
=== Closed Sets Intersect ===
=== Closed Sets are Connected ===
== Proof ==
=== Closed Sets Intersect implies Closed Sets are Connected ===
Let $T = \struct {S, \tau}$ be ultraconnected in the sense that:
:no two non-empty closed sets of $T$ are disjoint.
Let $F \subseteq S$ be an arbitrary closed set of $T$.
 $F$ is not connected.
Then there exist non-empty closed set $G, H$ in $F$ that are disjoint (and whose union is $F$).
By Closed Set in Closed Subspace, $G$ and $H$ are closed in $T$.
Because $G \cap H = \O$, $T$ is not ultraconnected.
This is a contradiction.
Thus $F$ is connected.
As $F$ is arbitrary, this applies to all closed set of $T$.
Thus $T = \struct {S, \tau}$ is ultraconnected in the sense that:
:every closed set of $T$ is connected..
=== Closed Sets are Connected implies Closed Sets Intersect ===
Let $T = \struct {S, \tau}$ be ultraconnected in the sense that:
:every closed set of $T$ is connected.
Let $G$ and $H$ be closed sets of $T$.
Then their union $G \cup H$ is closed in $T$.
By assumption, $G \cup H$ is connected.
By Closed Set in Closed Subspace, $G$ and $H$ are closed sets of $G \cup H$.
Because $G \cup H$ is connected, $G \cap H$ is non-empty.
Because $G$ and $H$ were arbitrary, this applies to intersection of all such closed sets
Thus $T = \struct {S, \tau}$ is ultraconnected in the sense that:
:no two non-empty closed sets of $T$ are disjoint.
== Also see ==
* Closed Set of Ultraconnected Space is Ultraconnected
* Space is Irreducible iff Open Sets are Connected
Category:Ultraconnected Spaces
Category:Connected Spaces
Equivalence of Definitions of Ultrafilter on Set

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
=== Definition 4 ===
== Proof ==
Let $S$ be a set.
=== Equivalence of Definitions 1, 2 and 3 ===
:
=== Definition 1 implies Definition 4 ===
Let $\FF \subseteq \powerset S$ a filter on $S$ which fulfills the condition:
:whenever $\GG$ is a filter on $S$ and $\FF \subseteq \GG$ holds, then $\FF = \GG$
By definition of filter, $\FF$ satisfies the Finite Intersection Property and is a non-empty set of subsets of $S$.
Let $U \subseteq S$.
 $U \notin \FF$.
Let $V = U^c$, where $U^c$ denotes the relative complement of $U$ in $S$.
Suppose there exists $C \in \FF$ such that:
:$C \cap V = \O$
By Empty Intersection iff Subset of Complement, it follows that:
:$C \subset U$
Thus $U \in \FF$, which contradicts our hypothesis that $U \notin \FF$.
Hence the set $\Omega = \set {C \cap V: C \in \FF}$ is a non-empty set of non-empty set.
Note that $\Omega$ is downward directed, that is, $\Omega$ is a filter basis.
From Filter Basis Generates Filter, $\Omega$ generates a filter $\GG$ on $S$ that contains $\FF$ and $\set V$.
By hypothesis, we have:
:$\FF =\GG$
Hence $U^c = V \in \FF$.
Thus $\FF$ is an ultrafilter by Definition 2.
=== Definition 4 implies Definition 1 ===
Let $S$ be a non-empty set and $\FF$ a non-empty set of subsets on $S$ which fulfills the conditions:
:$\FF$ has the finite intersection property
:For all $U \subseteq S$, either $U \in \FF$ or $U^c \in \FF$.
Because $\FF$ has the finite intersection property, it follows that $\O \notin \FF$.
As $\O \notin \FF$, it follows that $\O^c = S \in \FF$.
Let $U, V \in \FF$.
Then either $U \cap V \in \FF$ or $\paren {U \cap V}^c \in \FF$.
However we observe that:
:$\paren {U \cap V}^c \cap U \cap V = \O$
By finite intersection property, it follows that $U \cap V \in \FF$.
Now let $U \in \FF$ and $V \in S$ such that $U \subseteq V \subseteq S$.
Then either $V \in \FF$ or $V^c \in \FF$.
However we observe that:
:$V^c \cap U \subseteq V^c \cap V = \O$
By finite intersection property, it follows that $V \in \FF$.
Therefore $\FF$ is a filter.
Let $\GG$ be a filter on $S$ such that $\FF \subseteq \GG$.
Assume that $\FF \subsetneq \GG$.
Then there exists $A \in \GG \setminus \FF$.
Since $\O \notin \GG$ this implies that $A^c \notin \GG$.
As $\FF \subsetneq \GG$, it follows that $A^c \notin \FF$.
Therefore neither $A \in \FF$ nor $A^c \in \FF$, a contradiction to our assumption.
Thus $\FF = \GG$, which implies that $\FF$ is an ultrafilter by definition 1.
Category:Equivalence of Definitions of Ultrafilter on Set
Category:Ultrafilters
Equivalence of Definitions of Ultrafilter on Set/Definition 1 iff Definition 3

== Theorem ==
=== Definition 1 ===
=== Definition 3 ===
== Proof ==
Let $S$ be a set.
=== Definition 1 implies Definition 3 ===
Let $\FF$ be an ultrafilter on $S$ by definition 1.
Thus $\FF \subseteq \powerset S$ is a filter on $S$ which fulfills the condition:
:whenever $\GG$ is a filter on $S$ and $\FF \subseteq \GG$ holds, then $\FF = \GG$.
Let $A \subseteq S$.
 $A \notin \FF$ and $\relcomp S A \notin \FF$.
Consider the set $\BB := \set {A \cap V: V \in \FF}$.
This is a basis of a filter $\GG$ on $S$, for which $\FF \subseteq \GG$ holds.
Let $U \in \FF$.
But we have:
:$A \notin \FF$
and so:
:$\FF \subsetneq \GG$
Thus $\FF$ is not an ultrafilter by Definition 1.
This contradicts our initial hypothesis.
Hence either:
:$A \in \FF$
or:
:$\relcomp S A \in \FF$
and so $\FF$ fulfills the conditions to be an ultrafilter by Definition 3.
=== Definition 3 implies Definition 1 ===
Let $\FF$ be an ultrafilter on $S$ by definition 3.
That is, $\FF \subseteq \powerset S$ is a filter on $S$ which fulfills the condition:
:for any $A \subseteq S$ either $A \in \FF$ or $\relcomp S A \in \FF$ holds.
Let $\GG$ be a filter on $X$ such that $\FF \subseteq \GG$.
 $\FF \subsetneq GG$.
Then there exists $A \in \GG \setminus \FF$.
By definition of filter, $\O \notin \GG$.
But from Intersection with Relative Complement is Empty:
:$A \cap \relcomp S A$
and so:
:$\relcomp S A \notin \GG$
By hypothesis:
:$\FF \subsetneq \GG$
and so:
:$\relcomp S A \notin \FF$
Therefore neither $A \in \FF$ nor $\relcomp S A \in \FF$.
This contradicts our assumption:
:for any $A \subseteq S$ either $A \in \FF$ or $\relcomp S A \in \FF$ holds.
Thus:
:$\FF = \GG$
and so $\FF$ fulfills the conditions to be an ultrafilter by Definition 1.
Category:Equivalence of Definitions of Ultrafilter on Set
Equivalence of Definitions of Ultrafilter on Set/Equivalence of Definitions 1, 2 and 3

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
Let $S$ be a set.
=== Definition 1 implies Definition 2 ===
Let $\FF$ be an ultrafilter on $S$ by definition 1.
Thus $\FF \subseteq \powerset S$ is a filter on $S$ which fulfills the condition:
:whenever $\GG$ is a filter on $S$ and $\FF \subseteq \GG$ holds, then $\FF = \GG$.
Let $A \subseteq S$ and $B \subseteq S$ such that:
:$A \cap B = \O$
:$A \cup B \in \FF$
 $A \notin \FF$ and $B \notin \FF$.
Consider the set $\BB := \set {V \cap A: V \in \FF} \cup \set {V \cap B: V \in \FF}$.
This is a basis of a filter $\GG$ on $S$, for which $\FF \subseteq \GG$ holds.
Let $U \in \FF$.
But by definition of a filter:
:$U, V \in \FF \implies U \cap V \in \FF$
But $\O \notin \FF$.
This contradicts our initial hypothesis.
Hence either:
:$A \in \FF$
or:
:$B \in \FF$
and so $\FF$ fulfills the conditions to be an ultrafilter by Definition 2.
=== Definition 2 implies Definition 3 ===
Let $\FF$ be an ultrafilter on $S$ by definition 2.
That is, $\FF \subseteq \powerset S$ is a filter on $S$ which fulfills the condition:
: for every $A \subseteq S$ and $B \subseteq S$ such that $A \cap B = \O$ and $A \cup B \in \FF$, either $A \in \FF$ or $B \in \FF$.
Let $A \subseteq S$.
We have:
So $\FF$ fulfills the conditions to be an ultrafilter by Definition 3.
=== Definition 3 implies Definition 1 ===
Let $\FF$ be an ultrafilter on $S$ by definition 3.
That is, $\FF \subseteq \powerset S$ is a filter on $S$ which fulfills the condition:
:for any $A \subseteq S$ either $A \in \FF$ or $\relcomp S A \in \FF$ holds.
Let $\GG$ be a filter on $X$ such that $\FF \subseteq \GG$.
 $\FF \subsetneq \GG$.
Then there exists $A \in \GG \setminus \FF$.
By definition of filter, $\O \notin \GG$.
But from Intersection with Relative Complement is Empty:
:$A \cap \relcomp S A$
and so:
:$\relcomp S A \notin \GG$
By hypothesis:
:$\FF \subsetneq \GG$
and so:
:$\relcomp S A \notin \FF$
Therefore neither $A \in \FF$ nor $\relcomp S A \in \FF$.
This contradicts our assumption:
:for any $A \subseteq S$ either $A \in \FF$ or $\relcomp S A \in \FF$ holds.
Thus:
:$\FF = \GG$
and so $\FF$ fulfills the conditions to be an ultrafilter by Definition 1.
Category:Equivalence of Definitions of Ultrafilter on Set
Equivalence of Definitions of Uniform Absolute Convergence of Product of Complex Functions

== Definition ==
Let $X$ be a set.
Let $\sequence {f_n}$ be a sequence of bounded mappings $f_n: X \to \C$.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== 1 implies 2 ===
=== 2 implies 1 ===
By Terms in Uniformly Convergent Series Converge Uniformly to Zero
By the Monotone Convergence Theorem:
:The sequence of partial products of $\ds \prod_{n \mathop = n_0}^\infty \paren {1 + \size {f_n} }$ converges uniformly if ...
Use Bounds for Finite Product of Real Numbers.
=== 2 implies 3 ===
By Terms in Uniformly Convergent Series Converge Uniformly to Zero, there exists $n_0 \in \N$ such that $\size {\map {f_n} x} \le \dfrac 1 2$ for $n \ge n_0$.
Then $\map {f_n} x \ne -1$ for all $n \ge n_0$ and $x \in X$.
By Bounds for Complex Logarithm:
:$\size {\map \ln {1 + \map {f_n} x} } \le \dfrac 3 2 \size {\map {f_n} x}$
for $n \ge n_0$.
By Comparison Test for Uniformly Convergent Series,
:$\ds \sum_{n \mathop = n_0}^\infty \ln {1 + \map {f_n} x}$
converges uniformly absolutely.
=== 3 implies 1 ===
By Terms in Uniformly Convergent Series Converge Uniformly to Zero there exists $n_0 > 0$ such that $\ln {1 + \map {f_n} x} \le \dfrac 1 {100}$ for $n \ge n_0$ and $x \in X$.
By Bounds for Complex Exponential:
:$\size {\map {f_n} x} \le \dfrac 3 2 \size {\ln {1 + \map {f_n} x} } \le \dfrac 1 2$
By Bounds for Complex Logarithm:
:$\size {\map \ln {1 + \size {\map {f_n} x} } } \le \dfrac 3 2 \size {\map {f_n} x}$
Thus:
:$\size {\map \ln {1 + \size {\map {f_n} x} } } \le \dfrac 9 4 \size {\ln {1 + \map {f_n} x} }$
By Comparison Test for Uniformly Convergent Series:
:$\ds \sum_{n \mathop = n_0}^\infty \map \ln {1 + \size {\map {f_n} x} }$ and $\ds \sum_{n \mathop = n_0}^\infty \size {\map {f_n} x}$
converge uniformly.
By Bounds for Finite Product of Real Numbers the sequence of partial products of $\ds \prod_{n \mathop = n_0}^\infty \paren {1 + \size {f_n} }$ is bounded.
By Complex Exponential is Uniformly Continuous on Half-Planes, the sequence of partial products of $\ds \prod_{n \mathop = n_0}^\infty \paren {1 + \size {f_n} }$ converges uniformly.
By:
:Uniformly Convergent Sequence Multiplied with Function
:$f_1, \ldots, f_{n_0 - 1}$ are bounded
the sequence of partial products of $\ds \prod_{n \mathop = 1}^\infty \paren {1 + \size {f_n} }$ converges uniformly.
=== 3 implies 2 ===
By Terms in Uniformly Convergent Series Converge Uniformly to Zero there exists $n_0 > 0$ such that $\size {\ln {1 + \map {f_n} x} } \le \dfrac 1 2$ for $n \ge n_0$ and $x \in X$.
By Bounds for Complex Exponential:
:$\size {\map {f_n} x} \le \dfrac 3 2 \size {\ln {1 + \map {f_n} x} }$
By Comparison Test for Uniformly Convergent Series:
:$\ds \sum_{n \mathop = n_0}^\infty f_n$
converges uniformly absolutely.
== Sources ==
* $\text {VII}$: Compact and Convergence in the Space of Analytic Functions: $\S 5$: Weierstrass Factorization Theorem: Lemma $5.8$
Category:Infinite Products
Equivalence of Definitions of Unique Existential Quantifier

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== Definition 1 iff Definition 2 ===
=== Definition 2 iff Definition 3 ===
=== Definition 1 iff Definition 3 ===
Category:Unique Existential Quantifier
Category:Equivalence of Definitions of Unique Existential Quantifier
Equivalence of Definitions of Unique Existential Quantifier/Definition 1 iff Definition 2

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Suppose Definition 1, that for some $x$, both:
:$(1): \quad \map P x$
and:
:$(2): \quad \forall y : \paren {\map P y \implies x = y}$
From $(1)$:
:$x = y \implies \map P y$
From this and $(2)$, we conclude:
:$\exists x : \forall y : \paren {\map P y \iff x = y}$
Suppose Definition 2, that for some $x$ and every $y$:
:$\map P y \iff x = y$
Taking $y = x$ yields:
:$x = x \implies \map P x$
implying that $\map P x$.
Thus we conclude:
:$\exists x : \paren {\map P x \land \forall y : \paren {\map P y \implies x = y} }$
Category:Equivalence of Definitions of Unique Existential Quantifier
Equivalence of Definitions of Unique Existential Quantifier/Definition 1 iff Definition 3

== Theorem ==
=== Definition 1 ===
=== Definition 3 ===
== Proof ==
Suppose Definition 1, that for some $x$:
:$(1): \quad \map P x$
and:
:$(2): \quad \forall y : \paren {\map P y \implies x = y}$
Suppose that $\map P y$ and $\map P z$ for arbitrary $y$ and $z$.
From $(2)$, there is an $x$ such that $x = y$ and $x = z$.
Thus, for arbitrary $y$ and $z$:
:$\paren {\map P y \land \map P z} \implies y = z$
and from $(1)$:
:$\exists x : \map P x$
Suppose Definition 3, that there is an $x$ such that:
:$(1): \quad \map P x$
and that for arbitrary $y$ and $z$:
:$(2): \quad \paren {\map P y \land \map P z} \implies y = z$
Taking $z = x$, we have from $(2)$:
:$\paren {\map P y \land \map P x} \implies y = x$
Thus, from $\map P x$ in $(1)$:
:$\forall y : \paren {\map P y \implies x = y}$
Thus:
:$\exists x : \paren {\map P x \land \forall y : \paren {\map P y \implies x = y} }$
Category:Equivalence of Definitions of Unique Existential Quantifier
Equivalence of Definitions of Unique Existential Quantifier/Definition 2 iff Definition 3

== Theorem ==
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
Suppose Definition 2, that for some $x$:
:$(1): \quad \forall y : \paren {\map P y \iff x = y}$
Taking $y = x$ yields:
:$x = x \implies \map P x$
implying that $\exists x : \map P x$.
Suppose $\map P y$ and $\map P z$ for arbitrary $y$ and $z$.
Then from $(1)$, $y = x$ and $z = x$, giving:
:$\forall y : \forall z : \paren {\paren {\map P y \land \map P z} \implies y = z}$
Suppose Definition 3, that:
:$(1): \quad \exists x : \map P x$
and for arbitrary $y$ and $z$:
:$(2): \quad \paren { \map P y \land \map P z } \implies y = z$
From $(2)$, take $z = x$:
:$\paren {\map P y \land \map P x} \implies y = x$
Thus, by $(1)$:
:$\map P y \implies x = y$
Suppose $x = y$.
From $(1)$, $\map P x$, yielding:
:$x = y \implies \map P y$
Thus:
:$\exists x : \forall y : \paren {\map P y \iff x = y}$
Category:Equivalence of Definitions of Unique Existential Quantifier
Equivalence of Definitions of Unit of Ring

== Theorem ==
Let $\struct {R, +, \circ}$ be a ring with unity whose unity is $1_R$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\struct {R, +, \circ}$ be a ring with unity.
=== $(1)$ implies $(2)$ ===
Let $x \in R$ be a unit of $\struct {R, +, \circ}$ by definition 1.
Then by definition:
:$\exists y \in R: x \circ y = 1_R = y \circ x$
That is, by definition of divisor:
:$x \divides 1_R$
Thus $x$ is a unit of $\struct {R, +, \circ}$ by definition 2.
=== $(2)$ implies $(1)$ ===
Let $x \in R$ be a unit of $\struct {R, +, \circ}$ by definition 2.
Then by definition:
:$x \divides 1_R$
By definition of divisor:
:$\exists t \in R: 1_R = t \circ x$
Thus $x$ is a unit of $\struct {R, +, \circ}$ by definition 1.
Category:Units of Rings
Equivalence of Definitions of Unital Associative Commutative Algebra

== Theorem ==
Let $A$ be a commutative ring with unity.
=== Correspondence ===
=== Homomorphisms ===
=== Isomorphism of categories ===
Let $A-\operatorname{Alg}$ be the full subcategory of the category of unital algebras over $A$ consisting of commutative associative algebras.
Let $A / \mathbf{Ring}$ be the coslice category of rings under $A$.
Then the covariant functors:
$F : A-\operatorname{Alg} \to A/\mathbf{Ring}$ with:
$G : A/\mathbf{Ring} \to A-\operatorname{Alg}$ with:
are inverse functors.
In particular, $A-\operatorname{Alg}$ and $A/\mathbf{Ring}$ are isomorphic.
Category:Equivalence of Definitions of Unital Associative Commutative Algebra
Category:Unital Associative Commutative Algebras