avewright/proofwiki-math huggingface dataset:
Theorem: Closure of Infinite Union may not equal Union of Closures

Let $T$ be a topological space.
Let $I$ be an infinite indexing set.
Let $\family {H_i}_{i \mathop \in I}$ be an indexed family of subsets of a set $S$.
Let $\ds H = \bigcup_{i \mathop \in I} H_i$ be the union of $\family {H_i}_{i \mathop \in I}$.
Then it is not always the case that:
:$\ds \bigcup_{i \mathop \in I} \map \cl {H_i} = \map \cl {\bigcup_{i \mathop \in I} H_i}$
where $\map \cl {H_i}$ denotes the closure of $H_i$.

Proof:
Proof by Counterexample:
Let $\struct {\R, \tau_d}$ denote the real number line with the usual (Euclidean) topology $\tau_d$.
Let $\struct {\Q, \tau_d}$ be the rational number space, also under the usual (Euclidean) topology $\tau_d$.
For a rational number $\alpha \in \Q$, let $B_\alpha$ denote the singleton containing $\alpha$.
From Union of Closures of Singleton Rationals is Rational Space:
:$\ds \bigcup_{\alpha \mathop \in \Q} \map \cl {B_\alpha} = \Q$
From Closure of Union of Singleton Rationals is Real Number Line:
:$\ds \map \cl {\bigcup_{\alpha \mathop \in \Q} B_\alpha} = \R$
So it is seen that:
:$\ds \bigcup_{\alpha \mathop \in \Q} \map \cl {B_\alpha} \subset \ds \map \cl {\bigcup_{\alpha \mathop \in \Q} B_\alpha}$
but it is not the case that:
:$\ds \bigcup_{\alpha \mathop \in \Q} \map \cl {B_\alpha} = \ds \map \cl {\bigcup_{\alpha \mathop \in \Q} B_\alpha}$
and the result is apparent.
{{qed}}
Theorem: Set of Reciprocals of Positive Integers is Nowhere Dense in Reals

Let $N$ be the set defined as:
:$N := \set {\dfrac 1 n: n \in \Z_{>0} }$
where $\Z_{>0}$ is the set of (strictly) positive integers.
Let $\R$ denote the real number line with the usual (Euclidean) metric.
Then $N$ is nowhere dense in $\R$.

Proof:
From Zero is Limit Point of Integer Reciprocal Space, the only limit point of $N$ is $0$.
Hence:
:$\map \cl N = \set {\dfrac 1 n: n \in \Z_{>0} } \cup \set 0$
where $\map \cl N$ denotes the closure of $N$ in $\R$.
Trivially, $\map \cl N$ contains no open real intervals.
Hence no subset of $\map \cl N$ is open in $\R$.
Hence the union of all the subset of $\map \cl N$ which are open in $\R$ is empty.
That is, by definition, the interior of $N$ is empty.
That is:
:$\paren {\map \cl N}^\circ = \O$
and the result follows by definition of nowhere dense.
{{qed}}
Theorem: Nowhere Dense iff Complement of Closure is Everywhere Dense/Corollary

Let $H$ be a closed set of $T$.
Then $H$ is nowhere dense in $T$ {{iff}} $S \setminus H$ is everywhere dense in $T$.

Proof:
From Closed Set equals its Closure, $H$ is closed in $T$ {{iff}}:
:$H = H^-$
where $H^-$ is the closure of $H$.
The result then follows directly from Nowhere Dense iff Complement of Closure is Everywhere Dense.
{{qed}}
Theorem: Equivalence of Definitions of Topology Generated by Synthetic Basis

Let $S$ be a set.
Let $\BB$ be a synthetic basis on $S$.
{{TFAE|def = Topology Generated by Synthetic Basis}}
=== Definition 1 ===
{{:Definition:Topology Generated by Synthetic Basis/Definition 1}}
=== Definition 2 ===
{{:Definition:Topology Generated by Synthetic Basis/Definition 2}}
=== Definition 3 ===
{{:Definition:Topology Generated by Synthetic Basis/Definition 3}}

Proof:
=== Definition 1 iff Definition 2 ===
{{:Equivalence of Definitions of Topology Generated by Synthetic Basis/Definition 1 iff Definition 2}}{{qed|lemma}}
Theorem: Union from Synthetic Basis is Topology

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ is a topology on $X$.

Proof:
Let $\AA \subseteq \tau$.
It is to be shown that:
:$\ds \bigcup \AA \in \tau$
Define:
:$\ds \AA' = \bigcup_{U \mathop \in \AA} \set {B \in \BB: B \subseteq U}$
By Union is Smallest Superset: Family of Sets, it follows that $\AA' \subseteq \BB$.
Hence, by Equivalence of Definitions of Topology Generated by Synthetic Basis and General Self-Distributivity of Set Union:
:$\ds \bigcup \AA = \bigcup_{U \mathop \in \AA} \bigcup \set {B \in \BB: B \subseteq U} = \bigcup \AA' \in \tau$
Theorem: Union from Synthetic Basis is Topology

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ is a topology on $X$.

Proof:
Let $U, V \in \tau$.
It is to be shown that:
:$U \cap V \in \tau$
Define:
:$\OO = \set {A \cap B: A, B \in \BB, \, A \subseteq U, \, B \subseteq V}$
By the definition of a synthetic basis:
:$\forall A, B \in \BB: A \cap B \in \tau$
Hence, by the definition of a subset, it follows that $\OO \subseteq \tau$.
By {{Open-set-axiom|1}}, which has been verified above for $\tau$, we have:
:$\ds \bigcup \OO \in \tau$
Since set intersection preserves subsets, we have:
:$\ds \forall W \in \OO: \exists A, B \in \BB: W = A \cap B \subseteq U \cap V$
By Union is Smallest Superset: General Result, it follows that:
:$\ds \bigcup \OO \subseteq U \cap V$
By the definition of $\tau$, it follows from Set is Subset of Union: General Result that:
:$\ds \forall x \in U \cap V: \exists A, B \in \BB: A \subseteq U, \, B \subseteq V: x \in A \cap B \subseteq \bigcup \OO$
That is, by the definition of a subset:
:$\ds U \cap V \subseteq \bigcup \OO$
By definition of set equality:
:$\ds U \cap V = \bigcup \OO \in \tau$
Theorem: Union from Synthetic Basis is Topology

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ is a topology on $X$.

Proof:
By the definition of a synthetic basis, $\BB$ is a cover for $S$.
By Equivalent Conditions for Cover by Collection of Subsets, it follows that:
:$\ds S = \bigcup \BB \in \tau$
Theorem: Union from Synthetic Basis is Topology

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ is a topology on $X$.

Proof:
By the definition of a synthetic basis, we have that:
:$\forall x \in X: \exists B \in \BB: x \in B \subseteq X$
Theorem: Union from Synthetic Basis is Topology

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ is a topology on $X$.

Proof:
This theorem is divided into the following sections, each one of which contains its subproof under the associated links.
=== Open Set Axiom $(\text O 1)$: Union of Open Sets ===
{{:Union from Synthetic Basis is Topology/Open Set Axiom 1}}
=== Open Set Axiom $(\text O 2)$: Pairwise Intersection of Open Sets ===
{{:Union from Synthetic Basis is Topology/Open Set Axiom 2}}
=== Open Set Axiom $(\text O 3)$: Underlying Set is Element of Topology ===
{{:Union from Synthetic Basis is Topology/Open Set Axiom 3}}
Theorem: Binary Product as Limit

Let $\mathbf C$ be a metacategory.
Let $C_1, C_2$ be objects of $\mathbf C$.
Let their binary product $C_1 \times C_2$ exist in $\mathbf C$.
Then $C_1 \times C_2$ is the limit of the diagram $D: 2 \to \mathbf C$ defined by:
:$D_0 := C_1, D_1 := C_2$
where $2$ is the discrete category with two objects $0, 1$.

Proof:
Since there are no non-identity morphisms, a cone to $D$ is simply a pair:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 C_1
&
 C
  \ar[l]_*+{f_1}
  \ar[r]^*+{f_2}
&
 C_2
}\end{xy}$</nowiki>
of morphisms with common domain $C$.
By the universal mapping property of the binary product $C_1 \times C_2$, for such a cone to $D$ there is a unique $u: C \to C_1 \times C_2$ making:
::<nowiki>$\begin{xy}\xymatrix@L+3px@+1em{
&
 C
  \ar[dl]_*+{f_1}
  \ar@{-->}[d]^*{u}
  \ar[dr]^*+{f_2}
\\
 C_1
&
 C_1 \times C_2
  \ar[l]_*+{p_1}
  \ar[r]^*+{p_2}
&
 C_2
}\end{xy}$</nowiki>
a commutative diagram.
The conditions $p_1 \circ u = f_1$ and $p_2 \circ u = f_2$ precisely mean that $u: C \to C_1 \times C_2$ is a morphism of cones.
Thus for every cone $\struct{C, f_1, f_2}$ to $D$, there is a unique morphism of cones to the cone $\struct{C_1 \times C_2, p_1, p_2}$.
That is, $\struct{C_1 \times C_2, p_1, p_2}$ is a terminal object in $\map {\mathbf{Cone}} D$, the category of cones to $D$.
Hence the result, by definition of limit.
{{qed}}
Theorem: Equalizer as Limit

Let $\mathbf C$ be a metacategory.
Let $f_1, f_2: C_1 \to C_2$ be morphisms of $\mathbf C$.
Let their equalizer $e: E \to C_1$ exist in $\mathbf C$.
Define $\tilde e : E \to C_2$ by:
:$\tilde e = f_1 e = f_2 e$
Then $\struct {E, \sequence {e, \tilde e} }$ is the limit of the diagram $D: \mathbf J \to \mathbf C$ defined by:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 \mathbf{J}:
&
 \ast
  \ar[r]<2pt>
  \ar[r]<-2pt>
&
 \star
}\end{xy}$</nowiki>
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 D:
&
 C_1
  \ar[r]<2pt>^*+{f_1}
  \ar[r]<-2pt>_*+{f_2}
&
 C_2
}\end{xy}$</nowiki>

Proof:
Let $\struct {A, \sequence {a, \tilde a} }$ be a cone to $D$.
That is:
::<nowiki>$\begin{xy}\xymatrix{
 A
  \ar[d]_*+{a}
  \ar[dr]^*+{\tilde a}
\\
 C_1
  \ar[r]<2pt>^*+{f_1}
  \ar[r]<-2pt>_*+{f_2}
&
 C_2
}\end{xy}$</nowiki>
is a commutative diagram.
That is, $f_1 a = f_2 a$.
By {{Defof|Equalizer}}, there is a unique $u:A\to E$ such that:
:::<nowiki>$\begin{xy}\xymatrix{
 E 
  \ar[r]^*{e}
&
 C_1
  \ar[r]<2pt>^*{f_1}
  \ar[r]<-2pt>_*{f_2} 
&
 C_2
\\
 A
  \ar@{.>}[u]^*{u}
  \ar[ur]_*{a}
}\end{xy}$</nowiki>
is a commutative diagram.
This $u: A \to C$ is unique such that:
::<nowiki>$\begin{xy}\xymatrix{
&
A
  \ar@/_/[ddl]_*+{a}
  \ar@/^/[ddr]^*+{\tilde a}
  \ar@{.>}[d]^*+{u}
\\
&
E
  \ar[dl]_*+{e}
  \ar[dr]^*+{\tilde e}
\\
C_1
  \ar[rr]<2pt>^*+{f_1}
  \ar[rr]<-2pt>_*+{f_2}
&&
 C_2
}\end{xy}$</nowiki>
is a commutative diagram.
{{qed}}
Theorem: Terminal Object as Limit

Let $\mathbf C$ be a metacategory.
Let $\mathbf C$ have a terminal object $1$.
Then $1$ is the limit of the unique diagram $D: \mathbf 0 \to \mathbf C$, where $\mathbf 0$ is the zero category.

Proof:
By definition of cone to $D$, the objects of $\map {\mathbf{Cone} } D$ are just the objects of $\mathbf C$ with no associated morphisms.
In particular, the morphisms of $\map {\mathbf{Cone} } D$ are just the morphisms of $\mathbf C$.
Thus $1$ is a terminal object in $\map {\mathbf{Cone} } D$.
That is, $1$ is the limit of $D$.
{{qed}}
Theorem: Pullback as Limit

Let $\mathbf C$ be a metacategory.
Let $f_1: A \to C$ and $f_2: B \to C$ be morphisms of $\mathbf C$.
Let their pullback:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 P
  \ar[r]^*+{p_1}
  \ar[d]_*+{p_2}
&
 A
  \ar[d]^*+{f_1}
\\
 B
  \ar[r]_*+{f_2}
&
 C
}\end{xy}$</nowiki>
exist in $\mathbf C$.
Define the morphisms $p_3 : P \to C$ by:
:$p_3 = f_1 p_1 = f_2 p_2$
Then $\struct {P, \sequence {p_1, p_2, p_3} }$ is the limit of the diagram $D: \mathbf J \to \mathbf C$ defined by:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 \save[]+<0em,-2em>*{\mathbf{J}:} \restore
& &
 \cdot
  \ar[d]
\\ &
 \cdot
  \ar[r]
&
 \cdot
}\end{xy}$</nowiki>
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 \save[]+<0em,-2em>*{D:} \restore
& &
 A
  \ar[d]^*+{f_1}
\\ &
 B
  \ar[r]_*+{f_2}
&
 C
}\end{xy}$</nowiki>

Proof:
First, $\struct {P, \sequence {p_1, p_2, p_3} }$ is indeed a cone to $D$, as:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 P
  \ar[r]^*+{p_1}
  \ar[d]_*+{p_2}
  \ar[rd]^*+{p_3}
&
 A
  \ar[d]^*+{f_1}
\\
 B
  \ar[r]_*+{f_2}
&
 C
}\end{xy}$</nowiki>
is a commutative diagram.
We need to show that this is a terminal object in $\map {\mathbf{Cone} } D$.
Let $\struct {Q, \sequence {q_1, q_2, q_3} }$ be a cone to $D$.
That is:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 Q
  \ar[r]^*+{q_1}
  \ar[d]_*+{q_2}
  \ar[rd]^*+{q_3}
&
 A
  \ar[d]^*+{f_1}
\\
 B
  \ar[r]_*+{f_2}
&
 C
}\end{xy}$</nowiki>
is a commutative diagram.
By {{Defof|Pullback (Category Theory)|Pullback}}, there exists a unique $u : Q \to P$ such that:
:::<nowiki>$\begin{xy}\xymatrix@+1em{
 Q
  \ar@/^/[rrd]^*+{q_1}
  \ar@/_/[ddr]_*+{q_2}
  \ar@{-->}[rd]^*+{u}
\\
&
 P
  \ar[r]_*+{p_1}
  \ar[d]^*+{p_2}
&
 A
  \ar[d]^*+{f_1}
\\
&
 B
  \ar[r]_*+{f_2}
&
 C
}\end{xy}$</nowiki>
is a commutative diagram.
In particular:
:$q_1 = p_1 u$
:$q_2 = p_2 u$
:$q_3 = f_1 q_1 = f_1 p_1 u = p_3 u$
That is, $u$ is a morphism in $\map {\mathbf{Cone} } D$:
:$\struct {Q, \sequence {q_1, q_2, q_3} } \to \struct {P, \sequence {p_1, p_2, p_3} }$
Finally, uniqueness of this morphism $u$ follows also from the diagram above.
As this is true for all $\struct {Q, \sequence {q_1, q_2, q_3} }$ in $\map {\mathbf{Cone} } D$
, $\struct {P, \sequence {p_1, p_2, p_3} }$ is a terminal object.
{{qed}}
Theorem: Identification Topology is Topology

Let $T_1 = \struct {S_1, \tau_1}$ be a topological space.
Let $S_2$ be a set.
Let $f: S_1 \to S_2$ be a mapping.
Let $\tau_2$ be the identification topology on $S_2$ with respect to $f$ and $\struct {S_1, \tau_1}$.
Then $\tau_2$ is a topology on $S_2$.

Proof:
By definition:
:$\tau_2 = \set {V \in \powerset {S_2}: f^{-1} \sqbrk V \in \tau_1}$
We examine each of the open set axioms in turn:
Theorem: Identification Mapping is Continuous

Let $T_1 = \struct {S_1, \tau_1}$ be a topological space.
Let $S_2$ be a set.
Let $f: S_1 \to S_2$ be a mapping.
Let $\tau_2$ be the identification topology on $S_2$ with respect to $f$ and $\struct {S_1, \tau_1}$.
Then the identification mapping $f$ is continuous.

Proof:
By definition of identification topology:
:$\tau_2 = \set {V \in \powerset {S_2}: f^{-1} \sqbrk V \in \tau_1}$
That is:
:$V \in \tau_2 \implies f^{-1} \sqbrk V \in \tau_1$
This is precisely the definition of a continuous mapping.
{{qed}}
Category:Identification Topology
p1p49egjbhzpe3wej3gre4srnw99xg3
Theorem: Existence and Uniqueness of Identification Topology

Let $T_1 = \struct {S_1, \tau_1}$ be a topological space.
Let $S_2$ be a set.
Let $f: S_1 \to S_2$ be a mapping.
Let $\tau_2$ be the identification topology on $S_2$ with respect to $f$ and $\struct {S_1, \tau_1}$.
Then the identification topology on $S_2$ with respect to $f$ and $\struct {S_1, \tau_1}$ always exists and is unique.

Proof:
Let $\tau_2$ be the identification topology on $S_2$ with respect to $f$ and $\struct {S_1, \tau_1}$.
By definition:
:$\tau_2 := \set {V \in \powerset {S_2}: f^{-1} \sqbrk V \in \tau_1} \subseteq \powerset {S_2}$
where $\powerset {S_2}$ is the power set of $S_2$.
Let $V \subseteq S_2$.
Then either:
:$f^{-1} \sqbrk V \in \tau_1 \implies V \in \tau_2$
or:
:$f^{-1} \sqbrk V \notin \tau_1 \implies V \notin \tau_2$
In particular:
:$f^{-1} \sqbrk {S_2} = S_1 \in \tau_1 \implies S_2 \in \tau_2$
Thus $\tau_2$ exists.
By the same coin, given any $V \subseteq S_2$, either $V \in \tau_2$ or $V \notin \tau_2$, and so the set:
:$\tau_2 := \set {V \in \powerset {S_2}: f^{-1} \sqbrk V \in \tau_1}$
consists of a uniquely defined set of elements.
{{qed}}
Theorem: Category has Finite Limits iff Finite Products and Equalizers

Let $\mathbf C$ be a metacategory.
Then:
:$\mathbf C$ has all finite limits
{{iff}}:
:$\mathbf C$ has all finite products and equalizers.

Proof:
=== Necessary Condition ===
By definition, finite products are instances of finite limits.
So are equalizers, by Equalizer as Limit.
{{qed|lemma}}
Theorem: Identification Topology is Finest Topology for Mapping to be Continuous

Let $T_1 := \struct {S_1, \tau_1}$ be a topological space.
Let $S_2$ be a set.
Let $f: S_1 \to S_2$ be a mapping.
Let $\tau_2$ be the identification topology on $S_2$ with respect to $f$ and $\struct {S_1, \tau_1}$.
Let $T_2 := \struct {S_2, \tau_2}$ be the resulting topological space.
Then $\tau_2$ is the finest topology on $S_2$ such that $f: T_1 \to T_2$ is continuous.

Proof:
It is established in Identification Mapping is Continuous that $f$ is continuous.
Let $\tau \subseteq \powerset {S_2}$ be a topology on $S_2$ for which $f$ is $\struct {\tau_1, \tau}$-continuous.
Let $U \in \tau$.
Then by definition of $\struct {\tau_1, \tau}$-continuous:
:$f^{-1} \sqbrk U \in \tau_1$
By definition of $\tau_2$ it then follows that $U \in \tau_2$.
By definition of subset it follows that $\tau \subseteq \tau_2$.
Thus it has been shown that $\tau_2$ is finer than any topology on $S_2$ for which $f$ is $\struct {\tau_1, \tau}$-continuous.
Hence the result, by definition of finest topology.
{{qed}}
Theorem: Identification Topology equals Quotient Topology on Induced Equivalence

Let $\struct {S_1, \tau_1}$ be a topological space.
Let $S_2$ be a set.
Let $f: S_1 \to S_2$ be a surjective mapping.
Let $\tau_2$ be the identification topology on $S_2$ {{WRT}} $f$ and $\struct {S_1, \tau_1}$:
:$\tau_2 = \set {V \subseteq S_2 : f^{-1} \sqbrk V \in \tau_1}$
Let $\RR_f \subseteq S_1 \times S_1$ be the equivalence on $S_1$ induced by $f$:
:$\tuple {s_1, s_2} \in \RR_f \iff \map f {s_1} = \map f {s_2}$
Let $q_{\RR_f}$ be the quotient mapping induced by $\RR_f$.
Let $\tau_{\RR_f}$ be the quotient topology on $S_1 / \RR_f$ by $q_{\RR_f}$:
:$\tau_{\RR_f} := \set {U \subseteq S_1 / \RR_f: q_{\RR_f}^{-1} \sqbrk U \in \tau_1}$
Then:
:$\struct {S_2, \tau_2}$ is homeomorphic to the quotient space $\struct {S_1 / \RR_f, \tau_{\RR_f} }$.

Proof:
Define a mapping $\tilde f: S_1 / \RR_f \to S_2$ by:
:$\map {\tilde f} {\eqclass s { \RR_f} } = \map f s$
:<nowiki>$\begin{xy} \xymatrix@L+2mu@+1em{
 S_1 \ar[r]^*{f}
     \ar[rd]_*{ q_{\RR_f} }
&
 S_2 
\\ &
 S_1 / \RR_f \ar@{-->}[u]^*{\tilde f}
}\end{xy}$</nowiki>
Then $\tilde f$ is well-defined, as for all $s' \in \eqclass s {\RR_f}$, we have:
:$\map f {s'} = \map f s$
For any $s_1, s_2 \in S_1$ with $\eqclass {s_1} {\RR_f} \ne \eqclass {s_2} {\RR_f}$, we have:
:$\map f {s_1} \ne \map f {s_2}$
so:
:$\map {\tilde f} {\eqclass {s_1} {\RR_f} } \ne \map {\tilde f} {\eqclass {s_2} {\RR_f} }$
It follows that $\tilde f$ is injective.
For all $t \in S_2$, we can find $s \in S_1$ such that $\map f s = t$, as $f$ is surjective.
Then $\map {\tilde f} {\eqclass s {\RR_f} } = t$, so $\tilde f$ is surjective.
Let $V \in \tau_2$.
As Identification Mapping is Continuous, it follows that:
:$ f^{-1} \sqbrk V \in \tau_1$
Then:
{{begin-eqn}}
{{eqn | l = f^{-1} \sqbrk V
      | r = \set {s \in S_1 : \map f s \in V}
}}
{{eqn | r = q_{\RR_f}^{-1} \sqbrk {\set {\eqclass s {\RR_f} \in S_1 / \RR_f : \map f s \in V} }
}}
{{end-eqn}}
By definition of quotient topology, we have:
:$\set {\eqclass s {\RR_f} \in S_1 / \RR_f : \map f s \in V} \in \tau_{\RR_f}$
By definition of continuity, $\tilde f$ is continuous.
Let $U \in \tau_{\RR_f}$.
By definition of quotient topology, we have:
:$q_{\RR_f}^{-1} \sqbrk U \in \tau_1$
By definition of identification topology, we have:
:$f \sqbrk {q_{\RR_f}^{-1} \sqbrk U } \in \tau_2$
Then:
{{begin-eqn}}
{{eqn | l = f \sqbrk {q_{\RR_f}^{-1} \sqbrk U}
      | r = f \sqbrk {\set {s \in S_1 : \map {q_{\RR_f} } s \in U} }
}}
{{eqn | r = \set {t \in S_2 : \map f s = t, \eqclass s {\RR_f} \in U}
}}
{{eqn | r = \tilde f \sqbrk U
}}
{{eqn | r = \paren {\tilde f^{-1} }^{-1} \sqbrk U
}}
{{end-eqn}}
By definition of continuity, $\tilde f^{-1}$ is continuous.
By definition of homeomorphism, $\tilde f$ is a homeomorphism between $\struct {S_1 / \RR_f, \tau_{\RR_f} }$ and $\struct {S_2, \tau_2}$.
{{qed}}
Theorem: Young's Inequality for Increasing Functions

Let $a_0$ and $b_0$ be strictly positive real numbers.
Let $f: \closedint 0 {a_0} \to \closedint 0 {b_0}$ be a strictly increasing bijection.
Let $a$ and $b$ be real numbers such that $0 \le a \le a_0$ and $0 \le b \le b_0$.
Then:
:$\ds ab \le \int_0^a \map f u \rd u + \int_0^b \map {f^{-1} } v \rd v$
where $\ds \int$ denotes the definite integral.

Proof:
200pxthumbrightThe blue colored region corresponds to $\ds \int_0^a \map f u \rd u$ and the red colored region to $\ds \int_0^b \map {f^{-1} } v \rd v$.
{{ProofWanted}}
{{Namedfor|William Henry Young|cat = Young, W.H.}}
Theorem: Set is Closed iff Equals Topological Closure

Let $T$ be a topological space.
Let $H \subseteq T$.
Then $H$ is closed in $T$ {{iff}}:
:$H = \map \cl H$

Proof:
Let $H'$ denote the derived set of $H$.
By Closed Set iff Contains all its Limit Points, $H$ is closed in $T$ {{iff}} $H' \subseteq H$.
By Union with Superset is Superset, $H' \subseteq H$ {{iff}} $H = H \cup H'$.
The result follows from the definition of closure.
{{qed}}
Theorem: Set is Closed iff Equals Topological Closure

Let $T$ be a topological space.
Let $H \subseteq T$.
Then $H$ is closed in $T$ {{iff}}:
:$H = \map \cl H$

Proof:
Let $H^\complement$ denote the relative complement of $H$ in $T$.
By definition, we have that $H$ is closed in $T$ {{iff}} $H^\complement$ is open in $T$.
By Set is Open iff Neighborhood of all its Points, this is equivalent to:
:$\forall x \in H^\complement: \exists U \in \tau: x \in U \subseteq H^\complement$
By Empty Intersection iff Subset of Complement, we have that:
:$U \subseteq H^\complement \iff U \cap H = \O$
By Condition for Point being in Closure, it follows that $H^{\complement}$ is open in $T$ {{iff}}:
:$\forall x \in H^\complement: x \notin \map \cl H$
By the Rule of Transposition, this is equivalent to $\map \cl H \subseteq H$.
From Set is Subset of its Topological Closure, we have that $H \subseteq \map \cl H$.
By definition of set equality, this is equivalent to:
:$H = \map \cl H$
{{qed}}
Theorem: Equivalence of Definitions of Compact Topological Subspace

{{TFAE|def = Compact Topological Subspace}}
Let $T = \struct {S, \tau}$ be a topological space.
Let $T_H = \struct {H, \tau_H}$ be a topological subspace of $T$, where $H \subseteq S$.

Proof:
=== $1$ implies $2$ ===
Suppose $T_H$ is compact in the sense of Definition 1.
Let $\CC$ be a cover of $H$ by open sets of $T$.
Then for each $U \in \CC$, $U \cap H$ is open in $T_H$ by definition of the subspace topology.
Since $\CC$ is a cover of $H$ it follows that $\CC' = \set{U \cap H: U \in \CC}$ is also a cover of $H$.
By hypothesis, there exists a finite subcover $\FF'$ of $\CC'$ for $H$.
Thus let $\FF' = \set {U_1 \cap H, U_2 \cap H, \ldots, U_n \cap H}$ where $U_1, U_2, \ldots, U_n \in \CC$.
It follows that $\FF = \set {U_1, U_2, \ldots, U_n}$ is a finite subcover of $H$.
That is, $T_H$ is compact in the sense of Definition 2.
{{qed|lemma}}