avewright/proofwiki-math huggingface dataset:
Theorem: Equal Images of Mappings to Hausdorff Space form Closed Set

Let $T_A = \struct {S_A, \tau_A}$ and $T_B = \struct {S_B, \tau_B}$ be topological spaces.
Let $T_B$ be a Hausdorff space.
Let $f, g: T_A \to T_B$ be continuous mappings.
Let $W$ be the set defined as:
:$W = \set {x \in T_A: \map f x = \map g x}$
Then $W$ is closed in $T_A$.

Proof:
Consider the set $V = S_A \setminus W$.
Hence:
:$V = \set {x \in T_A: \map f x \ne \map g x}$
Let $x \in V$.
Then:
:$\map f x \ne \map g x$
and as $T_B$ is Hausdorff:
:$\exists U_1, U_2 \in \tau_B: \map f x \in U_1, \map g x \in U_2, U_1 \cap U_2 = \O$
As $f$ and $g$ are continuous mappings:
:$f^{-1} \sqbrk {U_1}$ and $g^{-1} \sqbrk {U_2}$ are open in  $T_B$.
Because $f^{-1} \sqbrk {U_1}$ and $g^{-1} \sqbrk {U_2}$ are open in $T_A$, $f^{-1} \sqbrk U_1 \cap g^{-1} \sqbrk U_2$ is also open in $T_A$.
Then we have that:
:$x \in f^{-1} \sqbrk {U_1} \cap g^{-1} \sqbrk {U_2}$
such that:
:$f^{-1} \sqbrk {U_1} \cap g^{-1} \sqbrk {U_2} \subseteq V$
Hence $V$ is open in $T_A$.
Hence $W = T_A \setminus V$ is closed in $T_A$.
{{qed}}
Theorem: Fixed Point Set of Continuous Self-Map on Hausdorff Space is Closed

Let $T = \struct {S, \tau}$ be a Hausdorff space.
Let $f: T \to T$ be a continuous mapping on $T$.
Let $W$ be the set defined as:
:$W = \set {x \in T: \map f x = x}$
Then $W$ is closed in $T$.

Proof:
Let $g: T \to T$ be the identity mapping on $T$:
:$\forall x \in T: \map g x = x$
From Identity Mapping is Continuous, $g$ is a continuous mapping on $T$.
From Equal Images of Mappings to Hausdorff Space form Closed Set:
:$\set {x \in T: \map f x = \map g x}$ is closed in $T$.
and the result follows.
{{qed}}
Theorem: Continuous Real Function is Bounded on Neighborhood of Argument

Let $A \subseteq \R$ be a subset of the real number line $\R$.
Let $f: A \to \R$ be a continuous real function on $A$.
Let $a \in A$.
Then there exists a bound:
:$K_a = 1 + \size {\map f a}$ for $\size {\map f x}$
for all $x$ in some neighborhood:
:$\openint {a - \map \delta a} {a + \map \delta a}$ of $a$
where $\map \delta a$ is a positive real constant which depends on $a$.

Proof:
Let $a \in A$.
By definition of continuous real function, there exists $\delta \in \R_{>0}$ such that:
:$\forall x \in A: 0 < \size {x - a} < \delta \implies \size {\map f x - \map f a} < \epsilon$
for all $\epsilon \in \R_{>0}$.
Putting $\epsilon = 1$, say, gives us:
:$\forall x \in A: 0 < \size {x - a} < \delta \implies \size {\map f x - \map f a} < 1$
Hence:
:$\size {\map f x} < 1 + \size {\map f a}$
for all $x \in \openint {a - \delta} {a + \delta}$
Here it is important to note that $\delta$ is dependent upon both $a$ and $f$, as well as $\epsilon$ (chosen here to be $1$).
{{qed}}
Theorem: Continuous Real Function Bounded on Finite Subdivision

Let $A = \closedint a b$ be a closed real interval of the set $\R$ of real numbers.
Let $f: A \to \R$ be a continuous real function on $A$.
Let $P = \set {x_0, x_1, x_2, \ldots, x_{n - 1}, x_n}$ be a finite subdivision of $A$ such that:
:each $\closedint {x_j} {x_{j + 1} }$ is a neighborhood of some $a_j$ such that $f$ is bounded on $\closedint {x_j} {x_{j + 1} }$.
Then $f$ is bounded on $A$.

Proof:
Follows directly from:
:Continuous Real Function is Bounded on Neighborhood of Argument
and:
:Mapping is Bounded on Union iff Bounded on Each Component/Real-Valued Function.
{{qed}}
Theorem: Linear Transformation from Finite-Dimensional Vector Space is Injective iff Surjective

Let $K$ be a field. 
Let $V$ be a finite dimensional vector space over $K$.
Let $f: V \to V$ be a linear transformation on $V$.
Then $f$ is an injection {{iff}} $f$ is a surjection.

Proof:
Let $n = \dim V$. 
From Vector Space has Basis, there exists a basis: 
:$\BB = \set {e_1, \ldots, e_n}$ 
for $V$. 
Then from Image of Generating Set of Vector Space under Linear Transformation is Generating Set of Image, $f \sqbrk \BB$ is a generating set for $f \sqbrk V$.
Theorem: Closed and Bounded Subspace is not necessarily Compact

Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$ be a subset of $A$.
Let $M_H = \struct {H, d_H}$ be the subspace of $M$ induced by $d$.
Let $H$ be closed and bounded.
Then it is not necessarily the case that $M_H$ is compact.

Proof:
Proof by Counterexample:
Let $A = \openint 0 1$ be the open unit interval.
From Open Real Interval is not Compact, $\openint 0 1$ is not a compact space.
Let $H = \openint 0 1$.
Then $H \subseteq A$.
From Underlying Set of Topological Space is Clopen, $\openint 0 1$ is both closed and open in $\openint 0 1$.
Thus $H$ is closed and bounded but not compact.
{{qed}}
Theorem: Union of Two Compact Sets is Compact

Let $T = \struct {S, \tau}$ be a topological spaces.
Let $H$ and $K$ be compact subsets of $T$.
Then $H \cup K$ is compact in $T$.

Proof:
Let $\CC$ be an open cover of $H \cup K$.
Then $\CC$ is an open cover of both $H$ and $K$.
As $H$ and $K$ are both compact in $T$:
:$H$ has a finite subcover $C_H$ of $\CC$
:$K$ has a finite subcover $C_K$ of $\CC$.
Their union $C_H \cup C_K$ is a finite subcover of $\CC$ for $H \cup K$.
From Union of Finite Sets is Finite it follows that $C_H \cup C_K$ is finite.
As $\CC$ is arbitrary, it follows by definition that $H \cup K$ is compact in $T$.
Theorem: Coarser Topology than Compact Space is Compact

Let $S$ be a set.
Let $\tau_1$ and $\tau_2$ be topologies on $S$ such that $\tau_1$ is coarser than $\tau_2$:
:$\tau_1 \subseteq \tau_2$
Let $\struct {S, \tau_2}$ be a compact space.
Then $\struct {S, \tau_1}$ is also compact.

Proof:
Let $\struct {S, \tau_2}$ be a compact space as asserted.
Let $I_S: \struct {S, \tau_2} \to \struct {S, \tau_1}$ denote the identity mapping on $S$:
:$\forall x \in S: \map {I_S} x = x$
From Identity Mapping to Coarser Topology is Continuous, $I_S$ is continuous.
We also have the result Identity Mapping is Surjection.
Hence we apply Compactness is Preserved under Continuous Surjection.
The result follows.
{{qed}}
Theorem: Space of Almost-Zero Sequences is not Closed in 2-Sequence Space

Let $\struct {\ell^2, \norm {\, \cdot \,}_2}$ be the normed 2-sequence vector space.
Let $\struct {c_{00}, \norm {\, \cdot \,}_2}$ be the normed vector space of almost-zero sequences.
Then $\struct {c_{00}, \norm {\, \cdot \,}_2}$ is not closed in $\struct {\ell^2, \norm {\, \cdot \,}_2}$.

Proof:
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $c_{00}$ such that:
:$\ds x_n := \tuple {1, \frac 1 2, \ldots \frac 1 n, 0, \ldots}$
Let $\ds x := \tuple {1, \frac 1 2, \ldots, \frac 1 n, \ldots}$ with $n \in \N_{>0}$.
We have that $x \in \ell^2 \setminus c_{00}$ where $\setminus$ denotes set difference.
Then:
{{begin-eqn}}
{{eqn | l = \norm {x_n - x}_2^2
      | r = \sum_{k \mathop = n \mathop + 1}^\infty \frac 1 {k^2}
      | c = {{defof|P-Norm|$p$-Norm}}
}}
{{eqn | o = <
      | r = \sum_{k \mathop = n \mathop + 1}^\infty \frac 1 {k \paren {k - 1} }
}}
{{eqn | r = \sum_{k \mathop = n \mathop + 1}^\infty \paren {\frac 1 {k - 1} - \frac 1 k}
}}
{{eqn | r = \frac 1 n
      | c = {{defof|Telescoping Series}}
}}
{{end-eqn}}
Pass the limit $n \to \infty$
Then:
:$\ds \lim_{n \mathop \to \infty} \norm {x_n - x} = 0$
Hence, $\struct {c_{00}, \norm {\, \cdot \,}}$ does not contain its limit points.
By definition, it is not closed.
{{qed}}
Theorem: Equivalence of Definitions of Preimage of Subset under Mapping

Let $f: S \to T$ be a mapping from a set $S$ to a set $T$.
Let $Y \subseteq T$ be a subset of $T$.
{{TFAE|def = Preimage of Subset under Mapping}}

Proof:
The difference in definitions is no more than a difference in notations.
Let $X$ be a preimage by definition $2$.
Then by definition:
:$X := \map {f^\gets} Y$
By definition of inverse image mapping of mapping:
:$\forall Y \in \powerset T: \map {f^\gets} Y = \set {s \in S: \exists t \in Y: \map f s = t}$
Thus $X$ is a preimage by definition $1$.
{{qed}}
Category:Preimage of Subset under Mapping
lphwi84iple73xpkz71ukb0u70mv3ie
Theorem: 1-Sequence Space is Proper Subset of 2-Sequence Space

Let $\ell^1$ and $\ell^2$ be the $1$-sequence space and $2$-sequence space respectively.
Then $\ell^1$ is a proper subset of $\ell^2$.

Proof:
=== $\ell^1$ is a subset of $\ell^2$ ===
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $\ell^1$.
By definition of $1$-sequence space:
:$\ds \sum_{n \mathop = 0}^\infty \size {x_n} < \infty$
By Terms in Convergent Series Converge to Zero:
:$\ds \lim_{n \mathop \to \infty} \size {x_n} = 0$
By definition of convergent sequence:
:$\exists N \in \N : \forall n > N : \size {x_n} < 1$
Furthermore:
:$\forall \size {x_n} < 1 : \size {x_n}^2 < \size {x_n}$
By Comparison Test:
:$\ds \sum_{n \mathop = 0}^\infty \size {x_n}^2 < \infty$
Hence:
:$\sequence {x_n}_{n \mathop \in \N} \in \ell^2$
That is:
:$\ell^1 \subseteq \ell^2$
{{qed|lemma}}
Theorem: Cardinality of Set of Characteristic Functions on Finite Set

Let $I$ be a finite set.
The number of characteristic functions on $I$ is:
:$2^{\card I}$ 
where $\card I$ denotes the cardinality of $I$.

Proof:
Let $A = \set {0, 1}$.
A characteristic function of $I$ is a mapping from $I$ to $A$.
Hence the set of characteristic functions on $I$ is the indexed Cartesian space $A_I$:
:$A^I = \ds \prod_{i \mathop \in I} A := \set {f: \paren {f: I \to A} \land \paren {\forall i \in I: \paren {\map f i \in A} } }$
Hence from Cardinality of Set of All Mappings:
:$\card {A^I} = 2^{\card I}$
{{Qed}}
Theorem: Cartesian Product of Projections is Projection on Cartesian Product of Mappings

Let $I$ be an indexing set.
Let $\family {S_\alpha}_{\alpha \mathop \in I}$ and $\family {T_\alpha}_{\alpha \mathop \in I}$ be families of sets both indexed by $I$.
For each $\alpha \in I$, let $f_\alpha: S_\alpha \to T_\alpha$ be a mapping.
There exists a unique mapping:
:$\ds f: \prod_{\alpha \mathop \in I} S_\alpha \to \prod_{\alpha \mathop \in I} T_\alpha$
such that:
:$\forall \alpha \in I: \pr_\alpha \circ f = f_\alpha \circ \pr_\alpha$
where:
:$\circ$ denotes composition of mappings
:$\pr_\alpha$ denotes the $\alpha$th projection on either $\ds \prod_{\alpha \mathop \in I} S_\alpha$ or $\ds \prod_{\alpha \mathop \in I} T_\alpha$ as appropriate.

Proof:
=== Proof of Existence ===
Let $\mathbf x \in \ds \prod_{\alpha \mathop \in I} S_\alpha$ be arbitrary:
:$\mathbf x = \family {x_\alpha \in S_\alpha}_{\alpha \mathop \in I}$
Let $\ds f: \prod_{\alpha \mathop \in I} S_\alpha \to \prod_{\alpha \mathop \in I} T_\alpha$ be defined as:
:$\forall \mathbf x \in \ds \prod_{\alpha \mathop \in I} S_\alpha: \map f {\mathbf x} = \family {\map {f_\alpha} {x_\alpha} }_{\alpha \mathop \in I}$
We have:
{{begin-eqn}}
{{eqn | q = \forall \mathbf x \in \prod_{\alpha \mathop \in I} S_\alpha
      | l = \map {\paren {f_\alpha \circ \pr_\alpha} } {\mathbf x}
      | r = \map {f_\alpha} {\map {\pr_\alpha} {\mathbf x} }
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {f_\alpha} {x_\alpha}
      | c = {{Defof|Projection on Family of Sets|$\alpha$th Projection}} on $\ds \prod_{\alpha \mathop \in I} S_\alpha$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | q = \forall \mathbf x \in \prod_{\alpha \mathop \in I} S_\alpha
      | l = \map {\paren {\pr_\alpha \circ f} } {\mathbf x}
      | r = \map {\pr_\alpha} {\family {\map {f_\alpha} {x_\alpha} }_{\alpha \mathop \in I} }
      | c = Definition of $f$
}}
{{eqn | r = \map {f_\alpha} {x_\alpha}
      | c = {{Defof|Projection on Family of Sets|$\alpha$th Projection}} on $\ds \prod_{\alpha \mathop \in I} T_\alpha$
}}
{{end-eqn}}
and it is seen that $f$ is such that:
:$\forall \alpha \in I: \pr_\alpha \circ f = f_\alpha \circ \pr_\alpha$
as required.
Hence the existence of $f$ as specified.
{{qed|lemma}}
Theorem: Space of Zero-Limit Sequences with Supremum Norm forms Banach Space

Let $c_0$ be the space of zero-limit sequences.
Let $\norm {\, \cdot \,}_\infty$ be the supremum norm.
Then $\struct {c_0, \norm {\, \cdot \,}_\infty}$ is a Banach space.

Proof:
Let $\sequence {a_n}_{n \mathop \in \N}$ be a Cauchy sequence in $\struct {c_0, \norm {\, \cdot \,}_\infty}$.
Let $\struct {\ell^\infty, \norm {\, \cdot \,}_\infty}$ be the normed vector space of bounded sequences.
By Space of Zero-Limit Sequences with Supremum Norm forms Normed Vector Space, $\struct {c_0, \norm {\, \cdot \,}_\infty}$ is a subspace of $\struct {\ell^\infty, \norm {\, \cdot \,}_\infty}$.
Hence, $\sequence {a_n}_{n \mathop \in \N}$ is also a Cauchy sequence in $\struct {\ell^\infty, \norm {\, \cdot \,}_\infty}$.
By Space of Bounded Sequences with Supremum Norm forms Banach Space, $\sequence {a_n}_{n \mathop \in \N}$ converges to $a \in \ell^\infty$.
Denote $a_n = \sequence {a_n^{\paren m}}_{m \mathop \in \N}$ and $a = \sequence {a^{\paren m}}_{m \mathop \in \N}$.
By definition of convergent sequences:
:$\forall \epsilon \in \R_{> 0} : \exists N \in \N : \forall n \in \N : n > N \implies \norm {a_n - a}_\infty < \epsilon$
Then:
{{begin-eqn}}
{{eqn | q = \forall m \in \N
      | l = \size {a_n^{\paren m} - a^{\paren m} }
      | o = \le
      | r = \max_{m \mathop \in \N} \size {a_n^{\paren m} - a^{\paren m} }
}}
{{eqn | r = \norm {a_n - a}_\infty
      | c = {{defof|Supremum Norm}}
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
Since $a_n \in c_0$:
:$\forall \epsilon \in \R_{\mathop > 0} : \exists M \in \R_{\mathop > 0} : \forall m \in \N : m > M \implies \size {a_n^{\paren m}} < \epsilon$
For all $m > M$ we also have that:
{{begin-eqn}}
{{eqn | l =  \size {a^{\paren m} }
      | o = \le
      | r =  \size {a^{\paren m} - a_n^{\paren m} + a_n^{\paren m} }
}}
{{eqn | o = \le
      | r =  \size {a^{\paren m} - a_n^{\paren m} } + \size {a_n^{\paren m} }
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = < 
      | r = \epsilon + \epsilon
}}
{{eqn | r = 2 \epsilon
}}
{{end-eqn}}
In other words:
:$\forall \epsilon' \in \R_{>0} : \exists M' \in \R_{>0} : \forall m \in \N : m > M' \implies \size {a^{\paren m} } < \epsilon'$
where $\epsilon' = 2\epsilon$ and $M' = M$.
By definition of zero-limit sequences, $a \in c_0$.
Therefore, in $\struct {c_0, \norm {\, \cdot \,}_\infty}$ a Cauchy sequence is also convergent in $\struct {c_0, \norm {\, \cdot \,}_\infty}$.
By definition, $\struct {c_0, \norm {\, \cdot \,}_\infty}$ is a Banach space.
{{qed}}
Theorem: Composition of Cartesian Products of Mappings

Let $I$ be an indexing set.
Let $\family {S_\alpha}_{\alpha \mathop \in I}$, $\family {T_\alpha}_{\alpha \mathop \in I}$ and $\family {U_\alpha}_{\alpha \mathop \in I}$ be families of sets all indexed by $I$.
For each $\alpha \in I$, let:
:$f_\alpha: S_\alpha \to T_\alpha$ be a mapping
:$g_\alpha: T_\alpha \to U_\alpha$ be a mapping.
Let:
:$\ds S = \prod_{\alpha \mathop \in I} S_\alpha$
:$\ds T = \prod_{\alpha \mathop \in I} T_\alpha$
:$\ds U = \prod_{\alpha \mathop \in I} U_\alpha$
Let $f: S \to T$ and $\ds g: T \to U$ be defined as:
:$\ds f = \prod_{\alpha \mathop \in I} f_\alpha$
:$\ds g = \prod_{\alpha \mathop \in I} g_\alpha$
Then their composition $g \circ f: S \to U$ is: 
:$\ds g \circ f: \prod_{\alpha \mathop \in I} g_\alpha \circ f_\alpha$

Proof:
First note that for all $\alpha \in I$:
:$\Dom {g_\alpha} = \Cdm {f_\alpha} = T_\alpha$
where $\Dom {g_\alpha}$ denotes the domain of $g_\alpha$ and $\Cdm {f_\alpha}$ denotes the codomain of $f_\alpha$.
So $g_\alpha \circ f_\alpha$ is defined for all $\alpha \in I$.
Similarly:
:$\Cdm f = \Dom g = T$
and so $g \circ f$ is defined.
Let $\mathbf x \in S$ be arbitrary:
:$\mathbf x = \family {x_\alpha \in S_\alpha}_{\alpha \mathop \in I}$
We have that:
{{begin-eqn}}
{{eqn | l = \map {\paren {g \circ f} } {\mathbf x}
      | r = \map {\prod_{\alpha \mathop \in I} g_\alpha} {\map {\prod_{\alpha \mathop \in I} f_\alpha} {\mathbf x} }
      | c = Definition of $f$
}}
{{eqn | r = \map {\prod_{\alpha \mathop \in I} g_\alpha} {\family {\map {f_\alpha} {x_\alpha} }_{\alpha \mathop \in I} }
      | c = Definition of $\ds \prod_{\alpha \mathop \in I} f_\alpha$
}}
{{eqn | r = \family {\map {\paren {g_\alpha \circ f_\alpha} } {x_\alpha} }_{\alpha \mathop \in I}
      | c = 
}}
{{eqn | r = \map {\prod_{\alpha \mathop \in I} g_\alpha \circ f_\alpha} {\mathbf x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Partition of Indexing Set induces Bijection on Family of Sets

Let $I$ be an indexing set.
Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets indexed by $I$.
Let $\family {I_\gamma}_{\gamma \mathop \in J}$ be a partitioning of $I$.
Then there exists a bijection:
:$\ds \phi: \prod_{\gamma \mathop \in J} \paren {\prod_{\alpha \mathop \in I_\gamma} S_\alpha} \to \prod_{\alpha \mathop \in I} S_\alpha$

Proof:
First a lemma:
{{:Partition of Indexing Set induces Bijection on Family of Sets/Lemma}}{{qed|lemma}}
We can define a projection $\pr_\gamma$:
:$\ds \pr_\gamma: \prod_{\gamma \mathop \in J} \paren {\prod_{\alpha \mathop \in I_\gamma} S_\alpha} \to \prod_{\alpha \mathop \in I_\gamma} S_\alpha$
so that for $\ds X \in \prod_{\gamma \mathop \in J} \paren {\prod_{\alpha \mathop \in I_\gamma} S_\alpha}, X = \family {X_\gamma}_{\gamma \mathop \in J}$:
:$\map {\pr_\gamma} X = X_\gamma$
From the lemma we can build $\phi$ so that for $I_\gamma = \set {\alpha: \alpha \in I_\gamma}$:
:$\ds \map \phi {\mathbf x} = \prod_{\gamma \mathop \in J} \paren {\prod_{\alpha \mathop \in I_\gamma} \map {\psi_\alpha} {x_\alpha} }$
as $\phi$ uniquely sets all components of $\map {\pr_\gamma} X$ for all $\gamma$.
The result follows.
{{qed}}
Theorem: Partition of Indexing Set induces Bijection on Family of Sets/Lemma

Let $I$ be an indexing set.
Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets indexed by $I$.
Let $I = I_1 \cup I_2$ such that $I_1 \cap I_2 = \O$.
Then there exists a bijection:
:$\ds \psi: \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha} \to \prod_{\alpha \mathop \in I} S_\alpha$

Proof:
Let us define the mapping:
:$\ds \psi: \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha} \to \prod_{\alpha \mathop \in I} S_\alpha$
$\psi$ can be injective {{iff}}:
:$\map \psi a = \map \psi {a'} \implies a = a'$
where $\ds a, a' \in \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha}$
We can define a projection $\pr_1$:
:$\ds \pr_1: \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha} \to \prod_{\alpha \mathop \in I_1} S_\alpha$
so that for $\ds X \in \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha}, X = \tuple {X_1, X_2}$:
:$\map {\pr_1} X = X_1$
and similarly a projection $\pr_2$:
:$\ds \pr_2: \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha} \to \prod_{\alpha \mathop \in I_2} S_\alpha$
so that for $\ds X \in \paren {\prod_{\alpha \mathop \in I_1} S_\alpha} \times \paren {\prod_{\alpha \mathop \in I_2} S_\alpha}, X = \tuple {X_1, X_2}$:
:$\map {\pr_2} X = X_2$
From these we can build $\psi$ so that for $I_1 = \set {\alpha: \alpha \in I_1}$ and $I_2 = \set {\alpha: \alpha \in I_2}$:
:$\ds \map \psi {\mathbf x} = \paren {\prod_{\alpha \mathop \in I_1} \map {\psi_\alpha} {x_\alpha} } \times \paren {\prod_{\alpha \mathop \in I_2} \map {\psi_\alpha} {x_\alpha} }$
as $\psi$ uniquely sets all components of $\map {\pr_1} X$ and $\map {\pr_2} X$.
These in turn uniquely set the $2$ components of $X$.
That is:
:$\map f X = \map f {X'} \implies X = X'$
Surjection follows trivially.
{{qed}}
Theorem: Subsequence of Subsequence

Let $s$ be a set.
Let $\sequence {s_n}$ be a sequence in $S$.
Let $\sequence {s_m}$ be a subsequence of $\sequence {s_n}$.
Let $\sequence {s_k}$ be a subsequence of $\sequence {s_m}$.
Then $\sequence {s_k}$ is a subsequence of $\sequence {s_n}$.

Proof:
By definition, there exists a strictly increasing sequence $\sequence {n_r}$ in $\N$ such that:
:$\forall m \in \N: s_m = s_{n_r}$
Similarly, there exists a strictly increasing sequence $\sequence {m_s}$ in $\N$ such that:
:$\forall k \in \N: s_k = s_{m_s}$
We have that:
:$\forall k \in \N: s_k \in \sequence {s_m}$
and that:
:$\forall m \in \N: s_m \in \sequence {s_n}$
hence:
:$\forall k \in \N: s_k \in \sequence {s_n}$
Because $\sequence {s_k}$ is a subsequence of $\sequence {s_m}$, we have that:
:$k = m_s \implies k + 1 = m_s + p$ for some $p \in \Z_{>0}$
and:
:$m_s = n_r \implies m_s + p = n_r + q$ for some $q \in \Z_{>0}$
Hence:
:$k = n_r \implies k + 1 = n_r + q$
and so $\sequence {s_k}$ is a subsequence of $\sequence {s_n}$.
{{qed}}
Theorem: Cardinality of Extensions of Function on Subset of Finite Set

Let $m, n \in \Z_{>0}$ be (strictly) positive integers.
Let $S$ be a set with $m$ elements.
Let $T$ be a set with $n$ elements.
Let $A$ be a subset of $S$ with $r$ elements where $0 \le r < m$.
Let $f: A \to T$ be a mapping.
Then there are $n^{m - r}$ distinct extensions of $f$ to $S$.

Proof:
Let $N$ denote the number of distinct extensions of $f$ to $S$.
The question is equivalent to asking the number of distinct mappings from $S \setminus A$ to $T$.
There are $m - r$ elements in $S \setminus A$.
Hence from Cardinality of Set of All Mappings:
:$N = n^{m - r}$
{{qed}}
Theorem: L1 Metric is Topologically Equivalent to Supremum Metric on Bounded Continuous Real Functions

Let $\FF$ be the set of all real functions which are also bounded on the closed interval $\closedint a b$.
Let $d: \FF \times \FF \to \R$ be the $L^1$ metric on $\closedint a b$:
:$\ds \forall f, g \in \FF: \map d {f, g} := \int_a^b \size {\map f t - \map g t} \rd t$
Let $d': \FF \times \FF \to \R$ be the supremum metric on $\closedint a b$:
:$\ds \forall f, g \in \FF: \map {d'} {f, g} := \sup_{x \mathop \in S} \size {\map f x - \map g x}$
Then $d$ and $d'$ are topologically equivalent metrics.

Proof:
Let $U$ be an upper bound of $\set {\size {\map f x - \map g x} }$.
Then:
:$\ds U \ge \sup_{x \mathop \in S} \size {\map f x - \map g x}$
Hence:
:$\ds \max_{x \mathop \in \closedint a b} \set {\size {\map f x - \map g x} } = \map {d'} {f, g}$
Then:
{{begin-eqn}}
{{eqn | l = \map d {f, g}
      | r = \int_a^b \size {\map f t - \map g t} \rd t
      | c = 
}}
{{eqn | r = \lim_{\Delta h \mathop \to 0} \sum_{i \mathop = i}^n \size {\map f t - \map g t} \Delta h
      | c = 
}}
{{eqn | o = \le
      | r = \lim_{\Delta h \mathop \to 0} \sum_{i \mathop = i}^n \map {d'} {f, g} \Delta h
      | c = 
}}
{{eqn | r = \map {d'} {f, g} \int_a^b \rd t
      | c = 
}}
{{eqn | r = \paren {b - a} \map {d'} {f, g}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map d {f, g}
      | o = \le
      | r = \paren {b - a} \map {d'} {f, g}
      | c = 
}}
{{end-eqn}}
{{qed}}