avewright/proofwiki-math huggingface dataset:
Theorem: Minimally Closed Class under Progressing Mapping

Statement of Conditions:
{{:Minimally Closed Class under Progressing Mapping/Statement}}
Then the following results hold:
=== Minimally Closed Class under Progressing Mapping induces Nest ===
{{:Minimally Closed Class under Progressing Mapping induces Nest}}
=== Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element ===
{{:Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element}}
=== Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element ===
{{:Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element}}
=== Minimally Closed Class under Progressing Mapping is Well-Ordered ===
{{:Minimally Closed Class under Progressing Mapping is Well-Ordered}}
=== Smallest Element of Minimally Closed Class under Progressing Mapping ===
{{:Smallest Element of Minimally Closed Class under Progressing Mapping}}

Proof:
According to hypothesis, let $M$ be a minimally closed under $g$ with respect to $b$.
By Minimally Closed Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
By Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element:
:if $x$ is a fixed point of $g$, then $x$ is the greatest element of $M$.
Thus the conditions for Closed Class under Progressing Mapping Lemma hold.
In order to show that $M$ is well-ordered under the subset relation, it is to be shown that every non-empty subclass $A$ of $M$ has a smallest element.
Let $A$ be an arbitrary non-empty subclass of $N$.
Let $L$ be the class of all elements $y$ of $N$ such that $y$ is a proper subset of all elements of $A$.
If $b \in A$, then from Smallest Element of Minimally Closed Class under Progressing Mapping, $b$ is the smallest element of $A$.
So, consider the case where $b \notin A$.
Then $b$ is a proper subset of every element of $A$.
Thus $b \in L$ and so $L$ is non-empty.
By definition, $L$ is bounded by all elements of $A$.
Since $A$ is non-empty, $L$ is bounded by at least one element of $A$.
Hence by Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element:
:$L$ has a greatest element $x$.
Therefore, by Closed Class under Progressing Mapping Lemma, $\map g x$ is the smallest element of $A$.
{{qed}}
Theorem: Minimally Closed Class under Progressing Mapping

Statement of Conditions:
{{:Minimally Closed Class under Progressing Mapping/Statement}}
Then the following results hold:
=== Minimally Closed Class under Progressing Mapping induces Nest ===
{{:Minimally Closed Class under Progressing Mapping induces Nest}}
=== Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element ===
{{:Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element}}
=== Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element ===
{{:Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element}}
=== Minimally Closed Class under Progressing Mapping is Well-Ordered ===
{{:Minimally Closed Class under Progressing Mapping is Well-Ordered}}
=== Smallest Element of Minimally Closed Class under Progressing Mapping ===
{{:Smallest Element of Minimally Closed Class under Progressing Mapping}}

Proof:
{{AimForCont}} $b$ is not the smallest element of $N$.
Then there exists $m \in N$ such that $b \nsubseteq m$.
In particular:
:$m \ne b$
Let $B$ be the subclass of $A$ defined as:
:$B = \set {x \in A: \paren {x = b} \lor \paren {\exists y \in B: x = \map g y} }$
This is a subclass of $A$ containing $b$ which is closed under $g$.
Let $z \in B$.
We have that:
:$b \nsubseteq m$
Suppose that:
:$z \nsubseteq m$
As $g$ is a Progressing Mapping, we have that:
:$z \subseteq \map g z$
It follows that:
:$\map g z \nsubseteq m$
By the Principle of General Induction for Minimally Closed Class it follows that:
:$\forall z \in B: m \nsubseteq \map g z$
and in particular:
:$\forall z \in B: m \ne \map g z$
In summary:
:$m \ne b$
and:
:$\not \exists z \in B: m = \map g z$
It follows that:
:$m \notin B$
Thus we have created a proper subclass $B$ of $A$ containing $b$ which is closed under $g$.
This contradicts the assumption that $A$ is a minimally closed class under $g$ with respect to $b$
Hence, by Proof by Contradiction, our supposition that $b$ is not the smallest element of $N$ was false.
The result follows.
{{qed}}
Theorem: Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element

Every bounded subset of $N$ has a greatest element.

Proof:
Let the hypothesis be assumed.
The proof proceeds by general induction.
For all $x \in N$, let $\map P x$ be the proposition:
:Every subset of $N$ which is bounded by $x$ has a greatest element.
=== Basis for the Induction ===
Let $x = b$.
From Smallest Element of Minimally Closed Class under Progressing Mapping, $b$ is the smallest element of $N$.
That is:
:$\forall x \in N: b \subseteq x$
So the only subset $B$ of $N$ such that $B$ is bounded by $b$ is $B = \set b$.
By definition, $\set b$ trivially has a greatest element, which is $b$.
Thus $\map P b$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
:Every subset of $N$ which is bounded by $x$ has a greatest element.
from which it is to be shown that:
:Every subset of $N$ which is bounded by $\map g x$ has a greatest element.
=== Induction Step ===
This is the induction step:
Let the induction hypothesis be assumed.
Let $B$ be a subset of $N$ which is bounded by $\map g x$.
Thus, by definition, every element of $B$ is a subset of $\map g x$.
It is to be shown that $B$ has a greatest element $m$.
That is, that $m \in B$ and every element of $B$ is a subset of $m$
Let $\map g x \in B$.
By definition of subset bounded by $\map g x$, every element of $B$ is a subset of $\map g x$.
That is, $\map g x$ is itself the greatest element of $B$.
Suppose that $\map g x \notin B$.
Then every element of $B$ is a proper subset of $\map g x$.
Let $y \in B$ be arbitrary.
Because $y$ is a proper subset of $\map g x$, there exists $z \in \map g x$ such that $z \notin y$.
Thus $\map g x$ is not a subset of $y$.
From Minimally Closed Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Because it is not the case that $\map g x \subseteq y$, it must be that:
:$y \subseteq x$
Thus, as $y$ is arbitrary, it follows that every element of $B$ is a proper subset of $x$.
Thus $B$ is bounded by $x$.
It follows by the induction hypothesis that $B$ has a greatest element.
So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.
Therefore:
:For all $x \in N$, every subset of $N$ which is bounded by $x$ has a greatest element.
That is:
:Every bounded subset of $N$ has a greatest element.
{{qed}}
Theorem: Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element

$g$ has no fixed point, unless possibly the greatest element, if there is one.

Proof:
Suppose $g$ has a fixed point.
Let $x$ be an element of $M$ such that $\map g x = x$.
We have from Smallest Element of Minimally Closed Class under Progressing Mapping that:
:$b \subseteq x$
Suppose that $y \subseteq x$.
Then by Image of Proper Subset under Progressing Mapping on Minimally Closed Class:
:$\map g y \subseteq \map g x$
But we have that $\map g x = x$.
Thus:
:$\map g y \subseteq x$
So we have:
:$b \subseteq x$
and:
:$y \subseteq x \implies \map g y \subseteq x$
and the result follows by the Principle of General Induction for Minimally Closed Class.
{{qed}}
Theorem: Minimally Closed Class under Progressing Mapping is Well-Ordered

$N$ is well-ordered under the subset relation.

Proof:
According to hypothesis, let $M$ be a minimally closed under $g$ with respect to $b$.
By Minimally Closed Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
By Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element:
:if $x$ is a fixed point of $g$, then $x$ is the greatest element of $M$.
Thus the conditions for Closed Class under Progressing Mapping Lemma hold.
In order to show that $M$ is well-ordered under the subset relation, it is to be shown that every non-empty subclass $A$ of $M$ has a smallest element.
Let $A$ be an arbitrary non-empty subclass of $N$.
Let $L$ be the class of all elements $y$ of $N$ such that $y$ is a proper subset of all elements of $A$.
If $b \in A$, then from Smallest Element of Minimally Closed Class under Progressing Mapping, $b$ is the smallest element of $A$.
So, consider the case where $b \notin A$.
Then $b$ is a proper subset of every element of $A$.
Thus $b \in L$ and so $L$ is non-empty.
By definition, $L$ is bounded by all elements of $A$.
Since $A$ is non-empty, $L$ is bounded by at least one element of $A$.
Hence by Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element:
:$L$ has a greatest element $x$.
Therefore, by Closed Class under Progressing Mapping Lemma, $\map g x$ is the smallest element of $A$.
{{qed}}
Theorem: Smallest Element of Minimally Closed Class under Progressing Mapping

$b$ is the smallest element of $N$.

Proof:
{{AimForCont}} $b$ is not the smallest element of $N$.
Then there exists $m \in N$ such that $b \nsubseteq m$.
In particular:
:$m \ne b$
Let $B$ be the subclass of $A$ defined as:
:$B = \set {x \in A: \paren {x = b} \lor \paren {\exists y \in B: x = \map g y} }$
This is a subclass of $A$ containing $b$ which is closed under $g$.
Let $z \in B$.
We have that:
:$b \nsubseteq m$
Suppose that:
:$z \nsubseteq m$
As $g$ is a Progressing Mapping, we have that:
:$z \subseteq \map g z$
It follows that:
:$\map g z \nsubseteq m$
By the Principle of General Induction for Minimally Closed Class it follows that:
:$\forall z \in B: m \nsubseteq \map g z$
and in particular:
:$\forall z \in B: m \ne \map g z$
In summary:
:$m \ne b$
and:
:$\not \exists z \in B: m = \map g z$
It follows that:
:$m \notin B$
Thus we have created a proper subclass $B$ of $A$ containing $b$ which is closed under $g$.
This contradicts the assumption that $A$ is a minimally closed class under $g$ with respect to $b$
Hence, by Proof by Contradiction, our supposition that $b$ is not the smallest element of $N$ was false.
The result follows.
{{qed}}
Theorem: Equivalence of Definitions of Minimally Closed Class

Let $A$ be a class.
Let $g$ be a mapping on $A$.
{{TFAE|def = Minimally Closed Class|view = minimally closed class under $g$}}

Proof:
Let it be given that $A$ is closed under $g$.
Theorem: Principle of General Induction/Minimally Closed Class

Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $b \in M$ such that $M$ is minimally closed under $g$ with respect to $b$.
Let $P: M \to \set {\T, \F}$ be a propositional function on $M$.
Suppose that:
:$(1): \quad \map P b = \T$
:$(2): \quad \forall x \in M: \map P x = \T \implies \map P {\map g x} = \T$
Then:
:$\forall x \in M: \map P x = \T$

Proof:
We are given that $M$ is minimally closed under $g$ with respect to $b$.
That is, $M$ is closed under $g$ with the extra property that $M$ has no proper class containing $b$ which is also closed under $g$.
Let $P$ be a propositional function on $M$ which has the properties specified:
:$(1): \quad \map P b = \T$
:$(2): \quad \forall x \in M: \map P x = \T \implies \map P {\map g x} = \T$
Let $S \subseteq M$ be the subclass of $M$ defined as:
:$S = \set {x \in M: \map P x}$
We have:
{{begin-eqn}}
{{eqn | l = \map P b
      | r = \T
      | c = 
}}
{{eqn | l = b
      | o = \in
      | r = M
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b
      | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
By definition, the class $S$ of all elements of $M$ such that $\map P x = \T$ is closed under $g$.
But because $M$ is minimally closed under $g$ with respect to $b$, if $b \in S$ then $S$ contains all elements of $M$.
That is:
:$S = M$
and so:
:$\forall x \in M: \map P x = \T$
as we were to show.
{{Qed}}
Theorem: Double Induction Principle/Minimally Closed Class

Let $M$ be a class which is closed under a progressing mapping $g$.
Let $b$ be an element of $M$ such that $M$ is minimally closed under $g$ with respect to $b$.
Let $\RR$ be a relation on $M$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in M
        | m = \map \RR {x, b}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in M
        | m = \map \RR {x, y} \land \map \RR {y, x} \implies \map \RR {x, \map g y}
}}
{{end-axiom}}
Then $\map \RR {x, y}$ holds for all $x, y \in M$.

Proof:
The proof proceeds by general induction.
Let an element $x$ of $M$ be defined as:
:'''left normal''' with respect to $\RR$ {{iff}} $\map \RR {x, y}$ for all $y \in M$
:'''right normal''' with respect to $\RR$ {{iff}} $\map \RR {y, x}$ for all $y \in M$.
Let the hypothesis be assumed.
First we demonstrate a lemma:
Theorem: Double Induction Principle/Minimally Closed Class/Lemma

Let $x$ be a right normal element of $M$ with respect to $\RR$.
Then $x$ is also a left normal element of $M$ with respect to $\RR$.

Proof:
The proof proceeds by general induction.
Let $x \in M$ be right normal with respect to $\RR$
Let $\map P y$ be the proposition:
:$\map \RR {x, y}$ holds.
Theorem: Sandwich Principle for Minimally Closed Class

Let $N$ be a class which is closed under a progressing mapping $g$.
Let $b$ be an element of $N$ such that $N$ is minimally closed under $g$ with respect to $b$.
Then for all $x, y \in N$:
:$x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$

Proof:
From Minimally Closed Class under Progressing Mapping induces Nest, we have that $N$ is a nest in which:
:$\forall x, y \in N: \map g x \subseteq y \lor y \subseteq x$
Thus the Sandwich Principle applies directly.
{{qed}}
Category:Sandwich Principle
Category:Minimally Closed Classes
Category:Progressing Mappings
lt38fy8t3d65u0mmqv6ujirfbpw5rxd
Theorem: Image of Proper Subset under Progressing Mapping on Minimally Closed Class

Let $N$ be a class which is closed under a progressing mapping $g$.
Let $b$ be an element of $N$ such that $N$ is minimally closed under $g$ with respect to $b$.
Then:
:$x \subset y \implies \map g x \subseteq y$

Proof:
From Minimally Closed Class under Progressing Mapping induces Nest, we have that $N$ is a nest in which:
:$\forall x, y \in N: \map g x \subseteq y \lor y \subseteq x$
Thus the corollary 1 of the Sandwich Principle applies directly.
{{qed}}
Category:Minimally Closed Classes under Progressing Mapping
nj5p8p3qi74wqw5b8x5tp7yejmwqsi4
Theorem: Even Impulse Pair is Fourier Transform of Cosine Function

Consider the (real) cosine function $\map \cos x: \R \to \R$.
:$\map f x = \map \cos {\pi x}$
Then:
{{begin-eqn}}
{{eqn | l = \map {\hat f} s
      | r = \dfrac 1 2 \map \delta {s - \dfrac 1 2} + \dfrac 1 2 \map \delta {s + \dfrac 1 2}
      | c = 
}}
{{eqn | r = \map {\operatorname {II} } s
      | c = 
}}
{{end-eqn}}
where:
:$\map {\hat f} s$ is the Fourier transform of $\map f x$.
:$\operatorname {II}$ denotes the even impulse pair function.

Proof:
By the definition of a Fourier transform:
{{begin-eqn}}
{{eqn | l = \map {\hat f} s
      | r = \int_{-\infty}^\infty e^{-2 \pi i x s} \map f x \rd x
      | c = 
}}
{{eqn | r = \int_{-\infty}^\infty e^{-2 \pi i x s} \map \cos {\pi x} \rd x
      | c = 
}}
{{eqn | r = \int_{-\infty}^\infty e^{-2 \pi i x s} \dfrac 1 2 \paren {e^{i \pi x} + e^{-i \pi x} } \rd x
      | c = Euler's Cosine Identity
}}
{{eqn | r = \dfrac 1 2 \int_{-\infty}^\infty e^{-2 \pi i x s} e^{i \pi x} \rd x + \dfrac 1 2 \int_{-\infty}^\infty e^{-2 \pi i x s} e^{-i \pi x} \rd x
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \dfrac 1 2 \int_{-\infty}^\infty e^{-2 \pi i x \paren {s - \frac 1 2 } } \rd x + \dfrac 1 2 \int_{-\infty}^\infty e^{-2 \pi i x \paren {s + \frac 1 2 } } \rd x
      | c = 
}}
{{eqn | r = \dfrac 1 2 \map \delta {s - \dfrac 1 2 } + \dfrac 1 2 \map \delta {s + \dfrac 1 2 }
      | c = Fourier Transform of 1
}}
{{end-eqn}}
{{qed}}
Theorem: Convolution of Real Function with Rectangle Function

Let $f: \R \to \R$ be a bounded piecewise continuous real function.
Consider the rectangle function $\Pi: \R \to \R$.
Then:
:$\forall x \in \R: \map \Pi x * \map f x = \ds \int_{x \mathop - \frac 1 2}^{x \mathop + \frac 1 2} \map f u \rd u$
where $*$ denotes the convolution integral.

Proof:
{{MissingLinks}}
By definition of convolution integral:
:$\ds \map \Pi x * \map f x  = \int_{-\infty}^\infty \map \Pi {x - t} \map f x \rd t$
The above integral exists because $f$ is discontinuous on a countable set (see Lebesgue-Vitali Theorem).
This is equal to:
:$\ds \int_{-\infty}^{x - \frac 1 2} \map \Pi {x - t} \map f t \rd t + \int_{x - \frac 1 2}^{x + \frac 1 2} \map \Pi {x - t} \map f t \rd t + \int_{x + \frac 1 2}^\infty \map \Pi {x - t} \map f t \rd t$ 
By definition of the rectangle function we have:
:$\map \Pi {x - t} = 1 \iff \size {x - t} \le \dfrac 1 2$
:$\map \Pi {x - t} = 0 \iff \size {x - t} > \dfrac 1 2$
Therefore:
{{begin-eqn}}
{{eqn | l = \int_{-\infty}^{x - \frac 1 2} \map \Pi {x - t} \map f t \rd t
      | r = \int_{x + \frac 1 2}^\infty \map \Pi {x - t} \map f t \rd t
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
What remains is:
{{begin-eqn}}
{{eqn | l = \int_{x - \frac 1 2}^{x + \frac 1 2} \map \Pi {x - t}\map f t \rd t
      | r = \int_{x - \frac 1 2}^{x + \frac 1 2} \map f t \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \Pi x * \map f x
      | r = \int_{x - \frac 1 2}^{x + \frac 1 2} \map f t \rd t
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Repeated Fourier Transform of Even Function

Let $f: \R \to \R$ be an even real function which is Lebesgue integrable.
Let $\ds \map \FF {\map f t} = \map F s = \int_{-\infty}^\infty e^{-2 \pi i s t} \map f t \rd t$ be the Fourier transform of $f$.
Let $\ds \map \FF {\map F s} = \map g t = \int_{-\infty}^\infty e^{-2 \pi i t s} \map F s \rd s$ be the Fourier transform of $F$.
Then:
:$\map g t = \map f t$

Proof:
{{begin-eqn}}
{{eqn | l = \map g t
      | r = \map f {-t}
      | c = Repeated Fourier Transform of Real Function
}}
{{eqn | r = \map f t
      | c = {{Defof|Even Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Repeated Fourier Transform of Odd Function

Let $f: \R \to \R$ be an odd real function which is Lebesgue integrable.
Let $\ds \map \FF {\map f t} = \map F s = \int_{-\infty}^\infty e^{-2 \pi i s t} \map f t \rd t$ be the Fourier transform of $f$.
Let $\ds \map \FF {\map F s} = \map g t = \int_{-\infty}^\infty e^{-2 \pi i t s} \map F s \rd s$ be the Fourier transform of $F$.
Then:
:$\map g t = -\map f t$

Proof:
{{begin-eqn}}
{{eqn | l = \map g t
      | r = \map f {-t}
      | c = Repeated Fourier Transform of Real Function
}}
{{eqn | r = -\map f t
      | c = {{Defof|Odd Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Fourier's Theorem/Integral Form

Let $f: \R \to \R$ be a real function which satisfies the Dirichlet conditions on $\R$.
Then:
:$\dfrac {\map f {t^+} + \map f {t^-} } 2 = \ds \int_{-\infty}^\infty e^{2 \pi i t s} \paren {\int_{-\infty}^\infty e^{-2 \pi i t s} \map f t \rd t} \rd s$
where:
:$\map f {t^+}$ and $\map f {t^-}$ denote the limit from above and the limit from below of $f$ at $t$.

Proof:
{{ProofWanted}}
{{Namedfor|Joseph Fourier|cat = Fourier}}
Theorem: Fourier's Theorem/Integral Form/Continuous Point

Let $f$ be continuous at $t \in \R$.
Then:
:$\ds \map f t = \int_{-\infty}^\infty e^{2 \pi i t s} \paren {\int_{-\infty}^\infty e^{-2 \pi i t s} \map f t \rd t} \rd s$

Proof:
At a point of continuity we have:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {t^+} + \map f {t^-} } 2
      | r = \dfrac {\map f t + \map f t} 2
      | c = as $\map f t = \map f {t^+} = \map f {t^-}$ at a point of continuity
}}
{{eqn | r = \dfrac {2 \map f t} 2
      | c = 
}}
{{eqn | r = \map f t
      | c = 
}}
{{end-eqn}}
The result follows from Fourier's Theorem: Integral Form.
{{qed}}
{{Namedfor|Joseph Fourier}}
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Lemma 1

:$\map {p_i^\to} {\map {\pr_k^\gets} {V_k} \cap Y_i}$ is open in $\struct{X_i, \tau_i}$

Proof:
We have that $p_i$ is a bijection from the lemmas:
:$p_i$ is an injection 
:$p_i$ is a surjection 
Let $x \in X_i$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {p_i^\to} {\map {\pr_k^\gets} {V_k} \cap Y_i}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {p_i^{-1} } x
      | o = \in
      | r = \map {\pr_k^\gets} {V_k} \cap Y_i 
      | c = {{Defof|Direct Image Mapping of Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {p_i^{-1} } x
      | o = \in
      | r = \map {\pr_k^\gets} {V_k}
      | c = as $\map {p_i^{-1} } x \in Y_i$
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {\pr_k} {\map {p_i^{-1} } x}
      | o = \in
      | r = V_k
      | c = {{Defof|Direct Image Mapping of Mapping}}
}}
{{end-eqn}}
By definition of $p_i$:
:$\map {p_i^{-1} } x = y$
where:
:$\forall j \in I : y_j = \begin {cases} z_j & j \ne i \\ x & j = i \end {cases}$
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Injection

Let $\family {X_i}_{i \mathop \in I}$ be a family of sets where $I$ is an arbitrary index set.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the Cartesian product of $\family {X_i}_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $p_i = \pr_i {\restriction_{Y_i}}$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is an injection.

Proof:
Let $x, y \in Y_i$.
Then for all $j \in I \setminus \set i$:
:$x_j = z_j = y_j$
Let $\map {p_i} x = \map {p_i} y$.
Then:
:$x_i = y_i$
Thus:
:$x = y$
It follows that $p_i$ is an injection by definition.
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Surjection

Let $\family {X_i}_{i \mathop \in I}$ be a family of sets where $I$ is an arbitrary index set.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the Cartesian product of $\family {X_i}_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $p_i = \pr_i {\restriction_{Y_i} }$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is a surjection.

Proof:
Let $x \in X_i$.
Let $y \in Y_i$ be defined by:
:<nowiki>$\forall j \in I: y_j = \begin{cases}
z_j & j \ne i \\
x & j = i
\end{cases}$</nowiki>
Then:
:$\map {p_i} y = y_i = x$
It follows that $p_i$ is a surjection by definition.