nyuuzyou/wikis huggingface dataset:
Equivalence of Definitions of Limit of Vector-Valued Function

== Theorem ==
Let $D \subseteq \R$ be a subset and $f: D \to \R^n, \map f x = \tuple {\map {f_1} x, \ldots, \map {f_n} x}$ a vector valued function.
Let $x_0 \in \R$ be a limit point of $D$ and $L = (L_1,\ldots,L_n) \in \R^n$.
Then $\ds \lim_{x \mathop \to x_0} \map f x = L$ $\ds \lim_{x \mathop \to x_0} \map {f_j} x = L_j$
In particular the limit of $f$ exists the limit of each component exists.
== Proof ==
=== Sufficient Condition ===
First assume that $\ds \lim_{x \mathop \to x_0} \map f x = L$.
Let $\epsilon \in \R_{\gt 0}$.
Then there exists $\delta \in \R_{\gt 0}$ such that for all $x \in D$ with $\size {x - x_0} \lt \delta$ we have $\size {\map f x - L} \lt \epsilon$.
Then it follows for all $j = \set {1, \ldots, n}$, that
$\ds \size {\map {f_j} x - L_j} = \sqrt {\paren {\map {f_j} x - L_j}^2} \le \sqrt {\sum_{j \mathop = 1}^n \paren {\map {f_j} x - L_j}^2} = \size {\map f x - L} \lt \epsilon$
And therefore $\ds \lim_{x \mathop \to x_0} \map {f_j} x = L_j$ for all $j$.
=== Necessary Condition ===
Now assume for all $j$ that $\ds \lim_{x \mathop \to x_0} \map {f_j} x = L_j$.
Let $\epsilon \in \R_{\gt 0}$.
Then there exists $\delta_j \in \R_{\gt 0}$ such that for all $x \in D$ with $\size {x - x_0} \lt \delta_j$ we have $\size {\map {f_j} x - L_j} \lt \dfrac \epsilon n$ for $j \in \set {1, \ldots, n}$.
Set $\ds \delta := \min_{1 \mathop = 1}^n \delta_j$.
Then it follows for all $\size {x - x_0} \lt \delta$:
Therefore:
:$\ds \lim_{x \mathop \to x_0} \map f x = L$
== Sources ==
Category:Limits of Mappings
Equivalence of Definitions of Lipschitz Equivalent Metrics

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $M_1 = \struct {A, d_1}$ and $M_2 = \struct {A, d_2}$ be metric spaces on the same underlying set $A$.
=== Definition 1 implies Definition 2 ===
Let $d_1$ and $d_2$ be Lipschitz equivalent by definition 1:
Then by definition:
: $\exists h, k \in \R_{>0} \forall x, y \in A: h \map {d_2} {x, y} \le \map {d_1} {x, y} \le k \map {d_2} {x, y}$
Let $K_1 = \dfrac 1 h, K_2 = k$.
and:
Thus $d_1$ and $d_2$ are Lipschitz equivalent by definition 2.
=== Definition 2 implies Definition 1 ===
Let $d_1$ and $d_2$ be Lipschitz equivalent by definition 2.
Then by definition:
: $(1): \quad \exists K_1 \in \R_{>0}: \forall x, y \in A: \map {d_2} {x, y} \le K_1 \map {d_1} {x, y}$
: $(2): \quad \exists K_2 \in \R_{>0}: \forall x, y \in A: \map {d_1} {x, y} \le K_2 \map {d_2} {x, y}$
Let $h = \dfrac 1 {K_1}, k = K_2$.
and:
Thus $d_1$ and $d_2$ are Lipschitz equivalent by definition 1.
Category:Lipschitz Equivalence
Equivalence of Definitions of Local Basis

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x$ be an element of $S$.
=== Local Basis for Open Sets ===
=== Neighborhood Basis of Open Sets ===
== Proof ==
=== Local Basis for Open Sets Implies Neighborhood Basis of Open Sets ===
=== Neighborhood Basis of Open Sets Implies Local Basis for Open Sets ===
Category:Local Bases
Category:Equivalence of Definitions of Local Basis
Equivalence of Definitions of Local Basis/Local Basis for Open Sets Implies Neighborhood Basis of Open Sets

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x$ be an element of $S$.
Let $\BB$ be a set of open neighborhoods of $x$ such that:
:$\forall U \in \tau: x \in U \implies \exists H \in \BB: H \subseteq U$
Then $\BB$ satisfies: 
:every neighborhood of $x$ contains a set in $\BB$.
== Proof ==
Let $N$ be a neighborhood of $x$.
Then there exists $U \in \tau$ such that $x \in U$ and $U \subseteq N$ by definition.
By assumption, there exists $H \in \BB$ such that $H \subseteq U$.
From Subset Relation is Transitive, $H \subseteq N$.
The result follows.
Category:Equivalence of Definitions of Local Basis
Equivalence of Definitions of Local Basis/Neighborhood Basis of Open Sets Implies Local Basis for Open Sets

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x$ be an element of $S$.
Let $\BB$ be a set of open neighborhoods of $x$ such that:
:every neighborhood of $x$ contains a set in $\BB$.
Then $\BB$ satisfies: 
:$\forall U \in \tau: x \in U \implies \exists H \in \BB: H \subseteq U$
== Proof ==
Let $U \in \tau$ such that $x \in U$.
From Set is Open iff Neighborhood of all its Points then $U$ is a neighborhood of $x$.
By assumption, there exists $H \in \BB$ such that $H \subseteq U$.
The result follows.
Category:Equivalence of Definitions of Local Basis
Equivalence of Definitions of Local Ring Homomorphism

== Theorem ==
Let $\struct {A, \mathfrak m}$ and $\struct {B, \mathfrak n}$ be commutative local rings.
Let $f : A \to B$ be a unital ring homomorphism.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== 1 iff 2 ===
Follows from Image is Subset iff Subset of Preimage.
=== 2 implies 3 ===
Let $f^{-1} \sqbrk {\mathfrak n} \supseteq \mathfrak m$.
We have to show that $f^{-1} \sqbrk {\mathfrak n} \subseteq \mathfrak m$.
By Preimage of Proper Ideal of Ring is Proper Ideal, $f^{-1} \sqbrk {\mathfrak n}$ is a proper ideal.
By Proper Ideal of Ring is Contained in Maximal Ideal, $f^{-1} \sqbrk {\mathfrak n}$ is contained in some maximal ideal of $A$.
Because $A$ is a commutative local ring, $\mathfrak m$ is its only maximal ideal.
=== 3 implies 2 ===
Follows by definition of set equality.
Category:Local Ring Homomorphisms
Equivalence of Definitions of Locally Compact Hausdorff Space

== Theorem ==
Let $T = \struct {S, \tau}$ be a Hausdorff topological space.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== $1$ implies $2$ ===
Let $x \in S$.
Let $K$ be a compact neighborhood of $x$.
Let $\BB$ be the set of compact neighborhoods of $x$.
It is shown that $\BB$ is a neighborhood basis of $x$.
Let $U$ be a neighborhood of $x$.
We have to show that $U$ contains a compact neighborhood of $x$.
By Neighborhood in Topological Subspace, $U\cap K$ is a neighborhood of $x$ in $K$.
By Neighborhood in Compact Hausdorff Space Contains Compact Neighborhood, there is a compact neighborhood $V$ of $x$ in $K$ such that $V \subset U \cap K$.
From Neighborhood in Topological Subspace there exists a neighborhood $W$ of $x$ in $T$ such that $W \cap K = V$. 
From Intersection of Neighborhoods in Topological Space is Neighborhood we have $W \cap K = V$ is a neighborhood of $x$ in $T$.
From Compact in Subspace is Compact in Topological Space then $V$ is compact in $T$.
Hence $V \in \BB$.
The result follows.
=== $2$ implies $1$ ===
Follows from Locally Compact Space is Weakly Locally Compact.
Category:Locally Compact Hausdorff Spaces
Equivalence of Definitions of Locally Connected Space

== Theorem ==
=== Definition 1: using Local Bases ===
=== Definition 2: using Neighborhood Bases ===
=== Definition 3: using (Global) Basis ===
=== Definition 4: using Open Components ===
== Proof ==
=== Definition 1 implies Definition 2 ===
=== Definition 2 implies Definition 1 ===
=== Definition 1 implies Definition 3 ===
=== Definition 3 implies Definition 1 ===
=== Definition 3 implies Definition 4 ===
=== Definition 4 implies Definition 3 ===
== Also see ==
* Equivalence of Definitions of Locally Path-Connected Space, whose proof is almost the same
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Locally Connected Spaces
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Connected Space/Definition 1 implies Definition 2

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let each point of $T$ have a local basis consisting entirely of connected sets in $T$.
Then
:each point of $T$ has a neighborhood basis consisting of connected sets of $T$.
== Proof ==
From Local Basis for Open Sets Implies Neighborhood Basis of Open Sets, it follows directly that:
:each point of $T$ has a neighborhood basis consisting entirely of connected sets in $T$.
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Connected Space/Definition 1 implies Definition 3

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space. 
Let each point $x$ of $T$ have a local basis $\DD_x$ consisting entirely of connected sets in $T$.
Then
:$T$ has a basis consisting of connected sets in $T$.
== Proof ==
By definition of local basis, each of these connected sets in $\DD_x$ is open in $T$.
Consider the set $\ds \DD = \bigcup_{x \mathop \in S} \DD_x$.
From Union of Local Bases is Basis, $\DD$ is a basis for the topology $\tau$.
Since each $\DD_x$ consists entirely of connected sets, $\DD$ also consists entirely of connected sets.
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Connected Space/Definition 2 implies Definition 1

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $T$ be weakly locally connected at each point of $T$.
That is, each point of $T$ has a neighborhood basis consisting of connected sets of $T$.
Then:
:each point of $T$ has a local basis consisting entirely of connected sets in $T$.
== Proof ==
Let $x \in S$ and $x \in U \in \tau$.
Let $\BB_x = \set {W \in \tau : x \in W, W \text{ is connected in } T}$.
 
By definition of local basis, we have to show that there exists a connected open set $V \in \BB_x$ with $x \in V \subset U$.
Let $V = \map {\operatorname{Comp}_x} U$ denote the component of $x$ in $U$.
From Open Set in Open Subspace, it suffices to show that $V$ is open in $U$.
By Set is Open iff Neighborhood of all its Points, we may do this by showing that $V$ is a neighborhood in $U$ of all of its points.
Let $y \in V$.
By assumption, there exists a connected neighborhood $W$ of $y$ in $T$ with $W \subset U$.
By Neighborhood in Topological Subspace, $W$ is a neighborhood of $y$ in $U$.
By definition of component:
:$W \subseteq \map {\operatorname{Comp}_y} U = \map {\operatorname{Comp}_x} U = V$
By Neighborhood iff Contains Neighborhood, $V$ is a neighborhood of $y$ in $U$.
Because $y$ was arbitrary, $V$ is open in $U$.
From Open Set in Open Subspace, $V$ is open in $T$.
Hence $V \in \BB_x$.
Because $U$ was arbitrary, $\BB_x$ is a local basis of $x$ consisting of (open) connected sets.
Since $x$ was arbitrary, then each point of $T$ has a local basis consisting entirely of connected sets in $T$.
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Connected Space/Definition 3 implies Definition 1

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space. 
Let $T$ have a basis $\BB$ consisting of connected sets in $T$.
Then each point $x$ of $T$ has a local basis $\BB_x$ consisting entirely of connected sets in $T$.
== Proof ==
For each $x \in S$ we define:
:$\BB_x = \set {B \in \BB: x \in B}$
From Basis induces Local Basis, $\BB_x$ is a local basis.
As each element of $\BB_x$ is also an element of $\BB$, it follows that $\BB_x$ is also formed of connected sets.
Thus, for each point $x \in S$, there is a local basis which consists entirely of connected sets.
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Connected Space/Definition 3 implies Definition 4

== Theorem ==
== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space. 
Let $T$ have a basis consisting of connected sets in $T$.
Then the components of the open sets of $T$ are also open in $T$.
== Proof ==
Let $U$ be an open subset of $T$.
From Open Set is Union of Elements of Basis, $U$ is a union of open connected sets in $T$.
From Open Set in Open Subspace and Connected Set in Subspace, $U$ is a union of open connected sets in $U$.
From Components are Open iff Union of Open Connected Sets, the components of $U$ are open in $U$.
From Open Set in Open Subspace then the components of $U$ are open in $T$.
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Connected Space/Definition 4 implies Definition 3

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space. 
Let the components of the open sets of $T$ are also open in $T$.
Then
:$T$ has a basis consisting of connected sets in $T$.
== Proof ==
Let $\BB = \set {U \in \tau : U \text{ is connected in } T}$.
Let $U$ be open in $T$.
By assumption, the components of $U$ are open in $T$.
From Connected Set in Subspace, the components of $U$ are connected in $T$.
By the definition of the components of a topological space, $U$ is the union of its components.
Hence $U$ is the union of open connected sets in $T$.
By definition, $\BB$ is an basis for $T$.
Category:Equivalence of Definitions of Locally Connected Space
Equivalence of Definitions of Locally Path-Connected Space

== Theorem ==
=== Definition 1: using Local Bases ===
=== Definition 2: using Neighborhood Bases ===
=== Definition 3: using (Global) Basis ===
=== Definition 4: using Open Path Components ===
== Proof ==
=== Definition 1 implies Definition 2 ===
=== Definition 2 implies Definition 1 ===
=== Definition 1 implies Definition 3 ===
=== Definition 3 implies Definition 1 ===
=== Definition 3 implies Definition 4 ===
=== Definition 4 implies Definition 3 ===
== Also see ==
* Equivalence of Definitions of Locally Connected Space, whose proof is almost the same
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Locally Path-Connected Spaces
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Locally Path-Connected Space/Definition 1 implies Definition 2

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let each point of $T$ have a local basis consisting entirely of path-connected sets in $T$.
Then
:each point of $T$ has a neighborhood basis consisting of path-connected sets in $T$.
== Proof ==
From Local Basis for Open Sets Implies Neighborhood Basis of Open Sets, it follows directly that:
:each point of $T$ has a neighborhood basis consisting entirely of path-connected sets in $T$.
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Locally Path-Connected Space/Definition 1 implies Definition 3

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let each point $x$ of $T$ have a local basis $\DD_x$ consisting entirely of path-connected sets in $T$.
Then
:$T$ has a basis consisting of path-connected sets in $T$.
== Proof ==
By definition of local basis, each of these path-connected sets in $\DD_x$ is open in $T$.
Consider the set $\ds \DD = \bigcup_{x \mathop \in S} \DD_x$.
From Union of Local Bases is Basis, $\DD$ is a basis for the topology $\tau$.
Since each $\DD_x$ consists entirely of path-connected sets, $\DD$ also consists entirely of path-connected sets.
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Locally Path-Connected Space/Definition 2 implies Definition 1

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let each point of $T$ have a neighborhood basis consisting of path-connected sets in $T$.
Then
:each point of $T$ has a local basis consisting entirely of path-connected sets in $T$.
== Proof ==
Let $x \in S$ and $x \in U \in \tau$.
Let $\BB_x = \set {W \in \tau : x \in W, W \text { is path-connected in } T}$.
 
By definition of local basis, we have to show that there exists a path-connected open set $V \in \tau$ with $x \in V \subset U$.
Let $V = \map {\operatorname {PC}_x} U$ denote the path component of $x$ in $U$.
From Open Set in Open Subspace, it suffices to show that $V$ is open in $U$.
By Set is Open iff Neighborhood of all its Points, we may do this by showing that $V$ is a neighborhood in $U$ of all of its points.
Let $y \in V$.
By assumption, there exists a path-connected neighborhood $W$ of $y$ in $T$ with $W \subset U$.
By Neighborhood in Topological Subspace, $W$ is a neighborhood of $y$ in $U$.
By definition of path component:
:$W \subset \map {\operatorname {PC}_y} U = \map {\operatorname {PC}_x} U = V$
By Neighborhood iff Contains Neighborhood, $V$ is a neighborhood of $y$ in $U$.
Because $y$ was arbitrary, $V$ is open in $U$.
From Open Set in Open Subspace, $V$ is open in $T$.
Hence $V \in \BB_x$.
Because $U$ was arbitrary, $\BB_x$ is a local basis of $x$ consisting of (open) path-connected sets.
Since $x$ was arbitrary, then each point of $T$ has a local basis consisting entirely of path-connected sets in $T$.
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Locally Path-Connected Space/Definition 3 implies Definition 1

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $T$ have a basis $\BB$ consisting of path-connected sets in $T$.
Then
:each point of $T$ has a local basis consisting entirely of path-connected sets in $T$.
== Proof ==
For each $x \in S$ we define:
:$\BB_x = \set {B \in \BB: x \in B}$
From Basis induces Local Basis, $\BB_x$ is a local basis.
As each element of $\BB_x$ is also an element of $\BB$, it follows that $\BB_x$ is also formed of path-connected sets.
Thus, for each point $x \in S$, there is a local basis which consists entirely of path-connected sets.
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Locally Path-Connected Space/Definition 3 implies Definition 4

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $T$ have a basis consisting of path-connected sets in $T$.
Then
:the path components of open sets of $T$ are also open in $T$.
== Proof ==
Let $U$ be an open subset of $T$.
From Open Set is Union of Elements of Basis, $U$ is a union of open path-connected sets in $T$.
From Open Set in Open Subspace and Path-Connected Set in Subspace, $U$ is a union of open path-connected sets in $U$.
From Path Components are Open iff Union of Open Path-Connected Sets, the path components of $U$ are open in $U$.
From Open Set in Open Subspace then the path components of $U$ are open in $T$.
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Locally Path-Connected Space/Definition 4 implies Definition 3

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let the path components of open sets of $T$ be also open in $T$.
Then
:$T$ has a basis consisting of path-connected sets in $T$.
== Proof ==
Let $\BB = \set {U \in \tau : U \text{ is path-connected in } T}$.
Let $U$ be open in $T$.
By assumption, the path components of $U$ are open in $T$.
From Path-Connected Set in Subspace, the path components of $U$ are path-connected in $T$.
By the definition of the path components of a topological space, $U$ is the union of its path components.
Hence $U$ is the union of open path-connected sets in $T$.
By definition, $\BB$ is an basis for $T$.
Category:Equivalence of Definitions of Locally Path-Connected Space
Equivalence of Definitions of Logical Consistence

== Theorem ==
Let $\mathbf H$ be a countable set (either finite or infinite) of WFFs of propositional logic.
The following statements are logically equivalent:
:$(1): \quad$ $\mathbf H$ has a model.
:$(2): \quad$ $\mathbf H$ is consistent for the proof system of propositional tableaux.
:$(3): \quad$ $\mathbf H$ has no tableau confutation.
== Proof ==
== Sources ==
* : $\S 1.11$: Compactness: Corollary $1.11.7$
Category:Propositional Tableaux
Category:Definition Equivalences
Equivalence of Definitions of Lower Section

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $U \subseteq S$.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
We are required to show that the following are equivalent:
By the Duality Principle, it suffices to prove that:
:$(1^*)$, $(2^*)$ and $(3^*)$ are equivalent
where these are the dual statements of $(1)$, $(2)$ and $(3)$, respectively.
By Dual Pairs, it can be seen that these dual statements are as follows:
Their equivalence is proved on Equivalence of Definitions of Upper Section.
Category:Lower Sections
Equivalence of Definitions of Lucas Numbers

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $\sequence {L_n}$ be the sequence defined as in definition 1.
It follows from Lucas Number as Sum of Fibonacci Numbers that $\sequence {L_n}$ is the sequence defined as in definition 2.
=== Definition 2 implies Definition 1 ===
Let $\sequence {L_n}$ be the sequence defined as in definition 2.
It follows from Lucas Number as Element of Recursive Sequence that $\sequence {L_n}$ is the sequence defined as in definition 1.
Category:Lucas Numbers
Equivalence of Definitions of Mandelbrot Set

== Theorem ==
=== Definition $1$ ===
=== Definition $2$ ===
== Proof ==
By definition of the Julia set:
=== Definition $(1)$ implies Definition $(2)$ ===
Let $M$ be the Mandelbrot set by definition $1$.
Let $c \in M$.
Thus $M$ is the Mandelbrot set by definition $2$.
=== Definition $(2)$ implies Definition $(1)$ ===
Let $M$ be the Mandelbrot set by definition $2$.
Thus $M$ is the Mandelbrot set by definition $1$.
Category:Mandelbrot Set
Equivalence of Definitions of Mapping

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
=== Definition 4 ===
== Proof ==
In the following, let $f \subseteq S \times T$ be a relation on $S \times T$.
=== $(1)$ $(4)$ ===
$f$ is by definition left-total :
:$\forall s \in S: \exists t \in T: \tuple {s, t} \in f$
which means exactly the same thing as:
:each element of $S$ is associated with with at least one element of $T$.
$f$ is by definition many-to-one :
:$\forall x \in \Dom f: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
which means exactly the same thing as:
:each element of $S$ is associated with with at most one element of $T$.
Thus:
:$f$ is left-total and many-to-one
:
:each element of $S$ is associated by $f$ with with exactly one one element of $T$.
That is:
:$f$ is a mapping by definition 1
:
:$f$ is a mapping by definition 4.
=== $(2)$ $(4)$ ===
$f$ is by definition left-total :
:$\forall s \in S: \exists t \in T: \tuple {s, t} \in G$
and:
$f$ is by definition many-to-one :
:$\forall x \in \Dom f: \forall y_1, y_2 \in \Cdm f: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
which means exactly the same thing as:
:$\forall x \in S: \forall y_1, y_2 \in T: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
That is:
:$f$ is a mapping by definition 2
:
:$f$ is a mapping by definition 4.
=== $(2)$ $(3)$ ===
Both definition 2 and definition 3 carry the stipulation that:
:$\forall x \in S: \exists y \in T: \tuple {x, y} \in f$
Then we have that definition 2 carries the stipulation that
:$\forall x \in S: \forall y_1, y_2 \in T: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
By the Rule of Transposition, that means the same as:
:$\forall x \in S: \forall y_1, y_2 \in T: \neg \paren {y_1 = y_2} \implies \neg \paren {\tuple {x, y_1} \in f \land \tuple {x, y_2} \in f}$
which in turn is the same as:
:$\forall \tuple {x_1, y_1}, \tuple {x_2, y_2} \in f: y_1 \ne y_2 \implies x_1 \ne x_2$
which is the other stipulation of definition 3.
That is:
:$f$ is a mapping by definition 2
:
:$f$ is a mapping by definition 3.
Category:Mapping Theory