nyuuzyou/wikis huggingface dataset:
Equivalence of Definitions of Image of Mapping

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $f: S \to T$ be a mapping.
Let:
:$Y = \set {t \in T: \exists s \in S: \map f s = t}$
Then by definition:
:$Y$ is the image of $f$ by definition 1.
But by definition of image of subset under mapping:
:$Y = f \sqbrk S$
Thus $Y$ is the image of $f$ by definition 2.
Hence the result.
Category:Mapping Theory
Category:Images
Equivalence of Definitions of Incomplete Elliptic Integral of the First Kind

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\map K {k, \phi}$ be the incomplete elliptic integral of the first kind by definition $1$.
Let $v := \sin \phi$.
Then we have:
So as $0 \le \phi \le \dfrac \pi 2$, we have that $0 \le v \le 1$.
Hence:
 
Thus $\map K {k, \phi}$ is the incomplete elliptic integral of the first kind by definition $2$.
Category:Incomplete Elliptic Integral of the First Kind
Equivalence of Definitions of Incomplete Elliptic Integral of the Second Kind

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\map E {k, \phi}$ be the incomplete elliptic integral of the second kind by definition $1$.
Let $v := \sin \phi$.
Then we have:
So as $0 \le \phi \le \dfrac \pi 2$, we have that $0 \le v \le 1$.
Hence:
 
Thus $\map E {k, \phi}$ is the incomplete elliptic integral of the second kind by definition $2$.
Category:Incomplete Elliptic Integral of the Second Kind
Equivalence of Definitions of Incomplete Elliptic Integral of the Third Kind

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\map \Pi {k, n, \phi}$ be the incomplete elliptic integral of the third kind by definition $1$.
Let $v := \sin \phi$.
Then we have:
So as $0 \le \phi \le \dfrac \pi 2$, we have that $0 \le v \le 1$.
Hence:
 
Thus $\map \Pi {k, n, \phi}$ is the incomplete elliptic integral of the third kind by definition $2$.
Category:Incomplete Elliptic Integral of the Third Kind
Equivalence of Definitions of Inconsistent (Logic)

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr P$ be a proof system for $\LL$.
=== Definition $1$ ===
=== Definition $2$ ===
== Proof ==
=== Definition $(1)$ implies Definition $(2)$ ===
Let $\FF$ be an inconsistent set of logical formulas by definition $1$.
Let $\phi$ be an arbitrary logical formula in $\FF$.
Then :
:$\phi \land \lnot \phi$
is a logical formula in $\FF$.
Thus $\FF$ is an inconsistent set of logical formulas by definition $2$.
=== Definition $(2)$ implies Definition $(1)$ ===
Let $\FF$ be an inconsistent set of logical formulas by definition $2$.
Then by definition:
:$\exists \phi \in \F: \FF \vdash_{\mathscr P} \paren {\phi \land \neg \phi}$
That is, $\phi \land \neg \phi$ is a logical formula in $\FF$.
Let $\psi$ be an arbitrary logical formula.
By the Rule of Explosion:
:$\forall \psi: \paren {\phi \land \neg \phi} \implies \psi$
That is:
:$\forall \psi: \FF \vdash_{\mathscr P} \psi$
That is:
:$\psi \in \FF$
As $\psi$ is arbitrary, it follows that every logical formula is a provable consequence of $\FF$.
Thus $\FF$ is an inconsistent set of logical formulas by definition $1$.
Category:Inconsistent (Logic)
Equivalence of Definitions of Independent Events

== Theorem ==
Let $\EE$ be an experiment with probability space $\struct {\Omega, \Sigma, \Pr}$.
Let $A, B \in \Sigma$ be events of $\EE$ such that $\map \Pr A > 0$ and $\map \Pr B > 0$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
== Sources ==
* : $\S 1.7$: Independent Events
Category:Independent Events
Equivalence of Definitions of Independent Subgroups

== Theorem ==
Let $G$ be a group whose identity is $e$.
Let $\sequence {H_n}$ be a sequence of independent subgroups of $G$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $H_1, H_2, \ldots, H_n$ be independent by definition 1:
:$\ds \prod_{k \mathop = 1}^n h_k = e \iff \forall k \in \closedint 1 n: h_k = e$
where $h_k \in H_k$ for all $k \in \closedint 1 n$.
Let $\ds u \in \paren {\prod_{j \mathop = 1}^{k - 1} H_j} \cap H_k$.
Then:
:$\ds \exists x_1, x_2, \ldots, x_{k - 1} \in H_1, \ldots, H_{k - 1}: u = \prod_{j \mathop = 1}^{k - 1} x_j$
We have that $u \in H_k$ and $H_k$ is a group.
Therefore let $x_k = u^{-1}$, the inverse of $u$.
For each $j \in \set {k + 1, k + 2, \ldots, n}$ let $x_j = e$.
Then:
Thus by hypothesis $u^{-1} = e$ and hence $u = e$.
Hence $H_1, H_2, \ldots, H_n$ are independent by definition 2:
:$\ds \forall k \in \set {2, 3, \ldots, n}: \paren {\prod_{j \mathop = 1}^{k - 1} H_j} \cap H_k = \set e$
=== Definition 2 implies Definition 1 ===
Let $H_1, H_2, \ldots, H_n$ be independent by definition 2:
:$\ds \forall k \in \set {2, 3, \ldots, n}: \paren {\prod_{j \mathop = 1}^{k - 1} H_j} \cap H_k = \set e$
 that:
:$\ds x_1, x_2, \ldots, x_n \in H_1, H_2, \ldots, H_n: \prod_{i \mathop = 1}^n x_i = e$
but that $x_j \ne e$ for some $j \in \set {1, 2, \ldots, n}$.
There is bound to be more than one of them, because otherwise that would mean:
:$\ds \prod_{i \mathop = 1}^n x_i = x_j e = e \implies x_j = e$
So let $m$ be the largest of the $j$ such that $x_j \ne e$.
Then $m > 1$, and:
Thus:
So:
:$x_m^{-1} \in H_m$
Therefore :
:$x_m^{-1} = e$
and therefore:
:$x_m = e$
But $m$ was defined to be the largest of the $j$ such that $x_j \ne e$.
Thus by Proof by Contradiction it follows that there can be no such $j$ so that:
:$\ds x_1, x_2, \ldots, x_n \in H_1, H_2, \ldots, H_n: \prod_{i \mathop = 1}^n x_i = e$
but that $x_j \ne e$ for some $j \in \set {1, 2, \ldots, n}$.
Hence $H_1, H_2, \ldots, H_n$ are independent by definition 1:
:$\ds \prod_{k \mathop = 1}^n h_k = e \iff \forall k \in \closedint 1 n: h_k = e$
where $h_k \in H_k$ for all $k \in \closedint 1 n$.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 18$: Induced $N$-ary Operations: Theorem $18.15$
Category:Subgroups
Equivalence of Definitions of Infimum of Real-Valued Function

== Theorem ==
Let $S \subseteq \R$ be a subset of the real numbers.
Let $f: S \to \R$ be a real function on $S$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $k \in \R$ be an infimum of $f$ by definition 1.
Then from the definition:
:$\text{(a)}: \quad k$ is a lower bound of $\map f x$ in $\R$.
:$\text{(b)}: \quad k \ge m$ for all lower bounds $m$ of $f \sqbrk S$ in $\R$.
As $k$ is a lower bound it follows that:
:$(1): \quad \forall x \in S: k \le \map f x$
Now let $\epsilon \in \R_{>0}$.
 $(2)$ were false:
:$\forall x \in S: k + \epsilon \le \map f x$
Then by definition, $k + \epsilon$ is a lower bound of $f$.
But by definition that means $k \ge k + \epsilon$.
So by Real Plus Epsilon:
:$k > k$
From this contradiction we conclude that:
:$(2): \quad \exists x \in S: \forall \epsilon \in \R_{>0}: \map f x < k + \epsilon$
Thus $k$ is an infimum of $f$ by definition 2.
=== Definition 2 implies Definition 1 ===
Let $k$ be an infimum of $f$ by definition 2:
:$(1): \quad \forall x \in S: k \le \map f x$
:$(2): \quad \exists x \in S: \forall \epsilon \in \R_{>0}: \map f x < k + \epsilon$
From $(1)$ we have that $k$ is a lower bound of $f$.
 that $k$ is not an infimum of $f$ by definition 1.
Then:
:$\exists m \in \R, m > k: \forall x \in S: \map f x \ge m$
Then:
:$\exists \epsilon \in \R_{>0}: m = k + \epsilon$
Hence:
:$\exists \epsilon \in \R_{>0}: \forall x \in S: k + \epsilon \le \map f x$
This contradicts $(2)$.
Thus $k$ is an infimum of $f$ by definition 1.
Category:Infima
Equivalence of Definitions of Infinite Cyclic Group

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== $(1)$ implies $(2)$ ===
Let $G = \gen g$ be an infinite cyclic group by definition 1.
Then by definition:
:$(1): \quad \forall n \in \Z_{> 0}: n > 0 \implies \nexists a \in G, a \ne e: a^n = e$
:
:$\exists a \in G: \exists m, n \in \Z, m \ne n: a^m = a^n$
Then by Equal Powers of Finite Order Element:
:$\exists k \in \Z_{> 0}: k \divides \paren {m - n}$
such that:
:$a^k = e$
As $m \ne n$, we have that $k \ge 1$.
This contradicts the condition $(1)$ for $G$ to be an infinite cyclic group.
From this contradiction we deduce that:
:$\forall a \in G: \forall m, n \in \Z: m \ne n \implies a^m \ne a^n$
Thus $G$ is an infinite cyclic group by definition 2.
=== $(2)$ implies $(1)$ ===
Let $G = \gen g$ be an infinite cyclic group by definition 2.
Then by definition:
:$\forall a \in G: \forall m, n \in \Z: m \ne n \implies a^m \ne a^n$
:
:$\exists a \in G, a \ne e: \exists n \in \Z: a^n = e$
Then:
:$a^{2 n} = a^n \circ a^n = e^2 = e = a^n$
That is:
:$\exists n, 2 n \in \Z: n \ne 2 n: a^n = a^{2 n}$
and so it is not the case that:
:$\forall a \in G: \forall m, n \in \Z: m \ne n \implies a^m \ne a^n$
From this contradiction we deduce that:
:$\forall n \in \Z_{> 0}: n > 0 \implies \nexists a \in G, a \ne e: a^n = e$
Thus $G$ is an infinite cyclic group by definition 1.
== Sources ==
* : $\S 1.7$: Theorem $8$
Category:Infinite Cyclic Group
Equivalence of Definitions of Infinite 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 ===
=== Definition 3 ===
== Proof ==
=== $(1)$ implies $(2)$ ===
Let $x$ be an infinite order element of $G$ by definition 1.
Then by definition there exists no $k \in \Z_{>0}$ such that $x^k = e_G$.
 not all $x^r$ are distinct for all $r \in \Z_{>0}$.
Then $x^m = x^n$ for some $m, n \in \Z$ where $m \ne n$.
, let $m > n$.
Then:
: $x^{m - n} = e^G$
As $m > n$ we have that $m - n \in \Z_{>0}$.
Let $k = m - n$.
and so:
:$\exists k \in \Z_{>0}$ such that $x^k = e_G$.
But this contradicts the statement that no such $k$ exists.
Hence no such distinct $m$ and $n$ exist.
Thus $x$ is an infinite order element of $G$ by definition 2.
=== $(2)$ implies $(1)$ ===
Let $x$ be an infinite order element of $G$ by definition 2.
Then by definition the powers $x^r$ of $x$ are distinct for all $r \in \Z_{>0}$.
That is, there exist no $x^m = x^n$ for some $m, n \in \Z$ where $m \ne n$.
 there exists $k \in \Z_{>0}$ such that $x^k = e^G$.
Consider some $n \in \Z_{>0}$ such that $m = n + k$.
But this contradicts the statement that no such $m, n \in \Z_{>0}$ exist.
Thus there can be no $k \in \Z_{>0}$ such that $x^k = e_G$.
Thus $x$ is an infinite order element of $G$ by definition 1.
=== $(2)$ implies $(3)$ ===
Let $x$ be an infinite order element of $G$ by definition 2.
Then by definition the powers $x^r$ of $x$ are distinct for all $r \in \Z_{>0}$.
 not all $\gen x = r$ for some $r \in \Z_{>0}$.
Let $s > r + 1$.
Then by the Pigeonhole Principle at least two of the elements of $\gen x$ are such that $x^m = x^n$ for some $m, n \in \closedint 0 r$
But this contradicts the statement that all $x^k$ are different for all $k \in \Z_{>0}$.
Thus $x$ is an infinite order element of $G$ by definition 3.
=== $(3)$ implies $(1)$ ===
Let $x$ be an infinite order element of $G$ by definition 3.
Then by definition the group $\gen x$ generated by $x$ is of infinite order:
:$\order {\gen x} = \infty$
 there exists $k \in \Z_{>0}$ such that $x^k = e^G$.
Then by Order of Cyclic Group equals Order of Generator, $\gen x$ has order $k$
But this contradicts the statement that $\order {\gen x} = \infty$.
Thus there can be no $k \in \Z_{>0}$ such that $x^k = e_G$.
Thus $x$ is an infinite order element of $G$ by definition 1.
Category:Order of Group Elements
Equivalence of Definitions of Initial 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: X \to Y_i}_{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:Initial Topology
Equivalence of Definitions of Initial 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: X \to Y_i}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
Let:
:$\SS = \set{\map {f_i^{-1}} U: i \in I, U \in \tau_i} \subseteq \map \PP X$
where $\map {f_i^{-1}} U$ denotes the preimage of $U$ under $f_i$.
Let $\tau$ be the topology on $X$ generated by the subbase $\SS$.
Then:
:$\tau$ is the coarsest topology on $X$ such that each $f_i: X \to Y_i$ is $\tuple {\tau, \tau_i}$-continuous.
== Proof ==
==== Mappings are Continuous ====
Let $i \in I$.
Let $U \in \tau_i$.
Then $\map {f_i^{-1} } U$ is an element of the subbase $\SS$ of $X$, and is therefore trivially in $\tau$.
==== $\tau$ is the Coarsest such Topology ====
Let $\struct {X, \vartheta}$ be a topological space.
Let the mappings $\family {f_i: X \to Y_i}_{i \mathop \in I}$ be $\tuple {\vartheta, \tau_i}$-continuous.
Let $U \in \SS$.
Then for some $i \in I$ and some $V \in \tau_i$:
:$U = \map {f_i^{-1} } V$
By definition of the continuity of $f_i$:
:$U \in \vartheta$
From Equivalence of Definitions of Topology Generated by Synthetic Sub-Basis:
:$\tau \in \vartheta$
That is, $\tau$ is coarser than $\vartheta$.
Category:Initial Topology
Equivalence of Definitions of Initial 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: X \to Y_i}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
Let $\tau$ be the coarsest topology on $X$ such that each $f_i: X \to Y_i$ is $\tuple{\tau, \tau_i}$-continuous.
Let:
:$\SS = \set {\map {f_i^{-1} } U: i \in I, U \in \tau_i} \subseteq \map \PP X$
where $\map {f_i^{-1} } U$ denotes the preimage of $U$ under $f_i$.
Then:
:$\tau$ is the topology on $X$ generated by the subbase $\SS$.
== Proof ==
Let $\map \tau \SS$ be the topology on $X$ generated by the subbase $\SS$.
==== $\tau$ contains Topology Generated by $\SS$ ====
Let $i \in I$ and $U \in \tau_i$.
By definition of $\tuple{\tau, \tau_i}$-continuity:
:$\map {f_i^{-1} } U \in \tau$
Since $i \in I$ and $U \in \tau_i$ were arbitrary, then $\SS \subseteq \tau$.
From Equivalence of Definitions of Topology Generated by Synthetic Sub-Basis:
:$\map \tau \SS \subseteq \tau$
==== Topology Generated by $\SS$ Contains $\tau$ ====
Let $i \in I$.
Let $U \in \tau_i$.
Then $\map {f_i^{-1} } U$ is an element of the subbase $\SS$ of $X$, and is therefore trivially in $\map \tau \SS$.
By definition of $\tuple{\map \tau \SS, \tau_i}$-continuity:
:each $f_i: X \to Y_i$ is $\tuple{\map \tau \SS, \tau_i}$-continuous
Because $\tau$ is the coarsest topology on $X$ such that each $f_i: X \to Y_i$ is $\tuple{\tau, \tau_i}$-continuous:
:$\tau \subseteq \map \tau \SS$
By definition of set equality:
:$\tau = \map \tau \SS$
Category:Initial Topology
Equivalence of Definitions of Injection

== Theorem ==
=== Definition 1 ===
=== Definition 1 a ===
=== Definition 2 ===
=== Definition 3 ===
=== Definition 4 ===
=== Definition 5 ===
=== Definition 6 ===
== Proof ==
=== Definition $1$ iff Definition $1 \ \text{a}$ ===
=== Definition $1$ iff Definition $2$ ===
=== Definition $1$ iff Definition $3$ ===
=== Definition $1$ iff Definition $4$ ===
=== Definition $1$ iff Definition $5$ ===
=== Definition $1$ iff Definition $6$ ===
Category:Injections
Category:Equivalence of Definitions of Injection
Equivalence of Definitions of Injection/Definition 1 iff Definition 1 a

== Theorem ==
=== Definition 1 ===
=== Definition 1 a ===
== Proof ==
Let $f: S \to T$ be an injection by definition 1.
Thus:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
Let $x_1 \ne x_2$.
 that:
:$\map f {x_1} = \map f {x_2}$
Then by definition 1:
:$x_1 = x_2$
This contradicts the assumption that $x_1 \ne x_2$.
Thus by Proof by Contradiction:
:$\forall x_1, x_2 \in S: x_1 \ne x_2 \implies \map f {x_1} \ne \map f {x_2}$
Thus $f$ is an injection by definition 1 a.
Let $f: S \to T$ be an injection by definition 1 a.
Thus:
:$\forall x_1, x_2 \in S: x_1 \ne x_2 \implies \map f {x_1} \ne \map f {x_2}$
Let $\map f {x_1} = \map f {x_2}$.
 that:
:$x_1 \ne x_2$
Then by definition 1 a:
:$\map f {x_1} \ne \map f {x_2}$
This contradicts the assumption that $\map f {x_1} = \map f {x_2}$.
Thus by Proof by Contradiction:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
Thus $f$ is an injection by definition 1.
== Sources ==
* : $\S 5$. Induced mappings; composition; injections; surjections; bijections
* : Appendix $\text{A}.4$: Functions
* : $\S 22$: Injections; bijections; inverse of a bijection
* : Chapter $2$: Maps and relations on sets: Definition $2.2$
Category:Equivalence of Definitions of Injection
Equivalence of Definitions of Injection/Definition 1 iff Definition 2

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $f: S \to T$ be an injection by definition 1.
Thus:
:$(1): \quad \forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
Let $y \in T: y = \map f {x_1} = \map f {x_2}$.
Thus $(1)$ can be rewritten in the language of relations as:
:$\forall x_1, x_2 \in S: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f \implies x_1 = x_2$
So, by definition, $f$ is a one-to-many relation.
By definition, $f$ is also mapping.
So, by definition, $f$ is a relation which is both many-to-one and left-total.
A relation which is both many-to-one and one-to-many is by definition a one-to-one relation.
Thus $f$ is a relation which is one-to-one and left-total.
So $f$ is an injection by definition 2.
Let $f: S \to T$ be an injection by definition 2.
That is, $f$ is a relation which is one-to-one and left-total.
A one-to-one relation is a relation which is both many-to-one and one-to-many.
So $f$ is a relation which is both many-to-one and left-total.
Thus $f$ is a mapping which is one-to-many:
:$\forall x_1, x_2 \in S: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f \implies x_1 = x_2$
Setting $y = \map f {x_1} = \map f {x_2}$:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
So $f$ is an injection by definition 1.
Category:Equivalence of Definitions of Injection
Equivalence of Definitions of Injection/Definition 1 iff Definition 3

== Theorem ==
=== Definition 1 ===
=== Definition 3 ===
== Proof ==
Let $f: S \to T$ be an injection by definition 1.
Thus:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
First we note that: 
:$t \in \Img f \implies \exists x \in \Dom f: \map f x = t$
thus fulfilling the condition for $f^{-1} {\restriction_{\Img f} }$ to be left-total.
Now let:
:$t \in \Img f: \tuple {t, y}, \tuple {t, z} \in f^{-1}$
Thus:
So by the definition of mapping, $f^{-1} {\restriction_{\Img f} }$ is a mapping.
So $f$ is an injection by definition 3.
Let $f: S \to T$ be an injection by definition 3.
Then:
:$f^{-1} {\restriction_{\Img f} }: \Img f \to \Dom f$ is a mapping
where $f^{-1} {\restriction_{\Img f} }$ is the restriction of the inverse of $f$ to the image set of $f$.
We need to show that:
:$\forall x, z \in \Dom f: \map f x = \map f z \implies x = z$
So, pick any $x, z \in \Dom f$ such that:
:$\map f x = \map f z$
Then:
So $f$ is an injection by definition 1.
== Sources ==
* : Chapter $\text I$: Algebraic Structures: $\S 5$: Composites and Inverses of Functions: Theorem $5.2$
* : Notation and Terminology
Category:Equivalence of Definitions of Injection
Equivalence of Definitions of Injection/Definition 1 iff Definition 4

== Theorem ==
=== Definition 1 ===
=== Definition 4 ===
== Proof ==
Let $f: S \to T$ be an injection by definition 1.
Thus:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
 $f^{-1} \sqbrk {\set y}$ has more than one element.
That is:
:$\exists y \in T: x_1, x_2 \in \map {f^{-1} } y, x_1 \ne x_2$
Then we have:
:$\map f {x_1} = \map f {x_2}$
but:
:$x_1 \ne x_2$
This contradicts our initial hypothesis that $f$ is an injection by definition 1.
From this contradiction it follows that $f^{-1} \sqbrk {\set y}$ has no more than one element.
That is, $f$ is an injection by definition 4.
Let $f: S \to T$ be an injection by definition 4.
That is, let $\map {f^{-1} } y$ be a singleton for all $y \in T$.
 it is not the case that:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
Then by definition:
:$\exists x_1, x_2 \in S, x_1 \ne x_2: \map f {x_1} = \map f {x_2} = y$
By definition of preimage of $y \in T$:
:$x_1 \in \map {f^{-1} } y, x_2 \in \map {f^{-1} } y$
and so:
$\set {x_1, x_2} \subseteq \map {f^{-1} } y$
Thus $\map {f^{-1} } y$ has more than one element for at least one $y \in T$.
This contradicts our initial hypothesis that $f$ is an injection by definition 4.
Thus:
:$\forall x_1, x_2 \in S: \map f {x_1} = \map f {x_2} \implies x_1 = x_2$
So $f$ is an injection by definition 1.
== Sources ==
* : $\S 10$: Inverses and Composites
* : Chapter $1$: Theory of Sets: $\S 6$: Functions
* : Appendix $\text{A}.5$: Identity, One-one, and Onto Functions: Proposition $\text{A}.5.1: 1 \ \text{(b)}$
Category:Equivalence of Definitions of Injection
Equivalence of Definitions of Integer Congruence

== Theorem ==
Let $m \in \Z_{> 0}$.
=== Definition by Remainder after Division ===
=== Definition by Modulo Operation ===
=== Definition by Integer Multiple ===
== Proof ==
Let $x_1, x_2, z \in \Z$.
Let $x_1 \equiv x_2 \pmod z$ as defined by the equal remainder after division:
:$\RR_z = \set {\tuple {x, y} \in \Z \times \Z: \exists k \in \Z: x = y + k z}$
Let $\tuple {x_1, x_2} \in \RR_z$.
Then by definition:
:$\exists k \in \Z: x_1 = x_2 + k z$
So, by definition of the modulo operation:
So:
:$x_1 \equiv x_2 \pmod z$
in the sense of definition by modulo operation.
Now let $x_1 \equiv x_2 \pmod z$ in the sense of definition by modulo operation.
That is:
:$x_1 \equiv x_2 \pmod z \iff x_1 \mod z = x_2 \mod z$
Let $z = 0$.
Then by definition, $x_1 \mod 0 = x_1$ and $x_2 \mod 0 = x_2$.
So as $x_1 \mod 0 = x_2 \mod 0$ we have that $x_1 = x_2$.
So:
:$x_1 - x_2 = 0 = 0.z$
and so $x_1 \equiv x_2 \pmod z$ in the sense of definition by integer multiple.
Now suppose $z \ne 0$.
Then from definition of the modulo operation:
:$x_1 \mod z = x_1 - z \floor {\dfrac {x_1} z}$
:$x_2 \mod z = x_2 - z \floor {\dfrac {x_2} z}$
Thus:
:$x_1 - z \floor {\dfrac {x_1} z} = x_2 - z \floor {\dfrac {x_2} z}$
and so:
:$x_1 - x_2 = z \paren {\floor {\dfrac {x_1} z} - \floor {\dfrac {x_2} z} }$
From the definition of the floor function, we see that both $\floor {\dfrac {x_1} z}$ and $\floor {\dfrac {x_2} z}$ are integers.
Therefore, so is $\floor {\dfrac {x_1} z} - \floor {\dfrac {x_2} z}$ an integer.
So $\exists k \in \Z: x_1 - x_2 = k z$.
Thus $x_1 - x_2 = k z$ and:
:$x_1 \equiv x_2 \pmod z$
in the sense of definition by integer multiple.
Now let $x_1 \equiv x_2 \pmod z$ in the sense of definition by integer multiple.
That is, $\exists k \in \Z: x_1 - x_2 = k z$.
Then $x_1 = x_2 + k z$ and so $\tuple {x_1, x_2} \in \RR_z$ where:
:$\RR_z = \set {\tuple {x, y} \in \R \times \R: \exists k \in \Z: x = y + k z}$
and so
:$x_1 \equiv x_2 \pmod z$
in the sense of definition by equivalence relation.
So all three definitions are equivalent: $(1) \implies (2) \implies (3) \implies (1)$.
== Sources ==
* : Appendix $1$: Some Results from the Elementary Theory of Numbers: Definition $4$
Category:Modulo Arithmetic