avewright/proofwiki-math huggingface dataset:
Theorem: Sequential Continuity is Equivalent to Continuity in Metric Space

Let $\struct {X, d}$ and $\struct {Y, e}$ be metric spaces.
Let $f: X \to Y$ be a mapping.
Let $x \in X$.
Then $f$ is continuous at $x$ {{iff}} $f$ is sequentially continuous at $x$.

Proof:
We have that a Continuous Mapping is Sequentially Continuous.
To prove the converse, by the Rule of Transposition we may prove the contrapositive:
:If $f$ is not continuous at $x$, then $f$ is not sequentially continuous at $x$.
We suppose therefore that there exists $\epsilon_0 > 0$  such that for all $\delta > 0$ there exists $y \in X$ such that $\map d {x, y} < \delta$ and $\map e {\map f x, \map f y} \ge \epsilon_0$.
For $n \ge 1$, define $\delta_n = \dfrac 1 n$.
For $n \ge 1$, we may choose $y_n \in X$ such that $\map d {x, y_n} < \delta_n$ and $\map e {\map f x, \map f {y_n} } \ge \epsilon_0$.
Therefore, by definition the sequence $\sequence {y_n}_{n \mathop \ge 1}$ converges to $x$.
However, by definition the sequence $\sequence {\map f {y_n} }_{n \mathop \ge 1}$ does not converge to $\map f x$.
That is, $f$ is not sequentially continuous at $x$.
{{Qed}}
Category:Metric Spaces
Category:Sequential Continuity
Category:Continuous Mappings on Metric Spaces
mwn55jty5tg4zil8ryqxbrboqnolur0
Theorem: Pullback of Commutative Triangle

Let $\mathbf C$ be a metacategory.
Suppose that the following is a commutative diagram in $\mathbf C$:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+2px{
 A'
  \ar[rr]^*{h_\alpha}
  \ar[dd]_*{\alpha'}
& &
 A
  \ar[rd]^*{\gamma}
  \ar[dd]^(.4)*{\alpha}
\\ &
 B'
  \ar[ld]^*{\beta'}
  \ar[rr] |{\hole} ^(.3)*{h_\beta}
& &
 B
  \ar[ld]^*{\beta}
\\
 C'
  \ar[rr]_*{h}
& &
 C
}\end{xy}$</nowiki>
and that the two squares in it are pullback diagrams.
Then there is a unique morphism $\gamma': A' \to B'$ making the following commute:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+2px{
 A'
  \ar[rr]^*{h_\alpha}
  \ar[dd]_*{\alpha'}
  \ar@{-->}[rd]^*{\gamma'}
& &
 A
  \ar[rd]^*{\gamma}
  \ar[dd]^(.4)*{\alpha}
\\ &
 B'
  \ar[ld]^*{\beta'}
  \ar[rr] |{\hole} ^(.3)*{h_\beta}
& &
 B
  \ar[ld]^*{\beta}
\\
 C'
  \ar[rr]_*{h}
& &
 C
}\end{xy}$</nowiki>
Furthermore, $\gamma'$ makes the following a pullback:
::<nowiki>$\begin{xy}\xymatrix@+.5em@L+2px{
 A'
  \ar[r]^*{h_\alpha}
  \ar[d]_*{\gamma'}
&
 A
  \ar[d]^*{\gamma}
\\
 B'
  \ar[r]_*{h_\beta}
&
 B
}\end{xy}$</nowiki>

Proof:
The first diagram above can be distorted into:
::<nowiki>$\begin{xy}\xymatrix@+.5em@L+2px{
 A'
  \ar@/^/[rrd]^*{\gamma \circ h_\alpha}
  \ar@/_/[ddr]_*{\alpha'}
\\ &
 B'
  \ar[r]^*{h_\beta}
  \ar[d]^*{\beta'}
&
 B
  \ar[d]^*{\beta}
\\ &
 C'
  \ar[r]_*{h}
&
 C
}\end{xy}$</nowiki>
and since the square is a pullback, there is a unique $\gamma': A' \to B'$ as desired.
That:
::<nowiki>$\begin{xy}\xymatrix@+.5em@L+2px{
 A'
  \ar[r]^*{h_\alpha}
  \ar[d]_*{\gamma'}
&
 A
  \ar[d]^*{\gamma}
\\
 B'
  \ar[r]_*{h_\beta}
&
 B
}\end{xy}$</nowiki>
is a pullback follows immediately from the Pullback Lemma.
{{qed}}
Theorem: Associative Commutative Idempotent Operation is Self-Distributive

Let $\struct {S, \circ}$ be an algebraic structure, such that:
{{begin-itemize}}
{{item|(1):|$\circ$ is associative}}
{{item|(2):|$\circ$ is commutative}}
{{item|(3):|$\circ$ is idempotent}}
{{end-itemize}}
Then $\circ$ is self-distributive.
That is:
:$\forall a, b, c \in S: \paren {a \circ b} \circ \paren {a \circ c} = a \circ b \circ c = \paren {a \circ c} \circ \paren {b \circ c}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {a \circ b} \circ \paren {a \circ c}
      | r = a \circ \paren {b \circ a} \circ c
      | c = $\circ$ is associative
}}
{{eqn | r = a \circ \paren {a \circ b} \circ c
      | c = $\circ$ is commutative
}}
{{eqn | r = \paren {a \circ a} \circ b \circ c
      | c = $\circ$ is associative
}}
{{eqn | r = a \circ b \circ c
      | c = $\circ$ is idempotent
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \paren {a \circ c} \circ \paren {b \circ c}
      | r = a \circ \paren {c \circ b} \circ c
      | c = $\circ$ is associative
}}
{{eqn | r = a \circ \paren {b \circ c} \circ c
      | c = $\circ$ is commutative
}}
{{eqn | r = a \circ b \circ \paren {c \circ c}
      | c = $\circ$ is associative
}}
{{eqn | r = a \circ b \circ c
      | c = $\circ$ is idempotent
}}
{{end-eqn}}
{{qed}}
Category:Abstract Algebra
Category:Commutativity
Category:Associativity
Category:Idempotence
Category:Self-Distributive Operations
Category:Semilattices
c63sbqjhjkef3htm6ug51s9nvmf3o1w
Theorem: Set Intersection is Self-Distributive

Set intersection is self-distributive:
:$\forall A, B, C: \paren {A \cap B} \cap \paren {A \cap C} = A \cap B \cap C = \paren {A \cap C} \cap \paren {B \cap C}$
where $A, B, C$ are sets.

Proof:
We have:
:Intersection is Associative
:Intersection is Commutative
:Set Intersection is Idempotent
The result follows from Associative Commutative Idempotent Operation is Self-Distributive.
{{qed}}
Category:Set Intersection
Category:Examples of Self-Distributive Operations
Category:Set Intersection is Self-Distributive
6ew7tvv00uvl5jr9vkzjwnmro8ds3na
Theorem: Inclusion Mapping is Restriction of Identity

Let $T$ be a set.
Let $S \subseteq T$ be a subset of $T$.
Let $i_S: S \to T$ be the inclusion mapping on $S$.
Then $i_S$ is the restriction of the identity mapping $I_T: T \to T$ on $T$.

Proof:
By definition of inclusion mapping:
:$i_S: S \to T: \forall x \in S: \map {i_S} x = x$
By definition of identity mapping:
:$I_T: T \to T: \forall x \in T: \map {I_T} x = x$
The result follows by definition of restriction of mapping.
{{qed}}
Theorem: Preimage of Subset under Inclusion Mapping

Let $S$ be a set.
Let $H \subseteq S$ be a subset of $S$.
Let $i_H: H \to S$ be the inclusion mapping on $H$.
Let $T \subseteq S$.
Then:
:$i_H^{-1} \sqbrk T = T \cap H$
where $i_H^{-1} \sqbrk T$ is the preimage of $T$ under $i_H$.

Proof:
By definition of preimage:
:$i_H^{-1} \sqbrk T = \set {h \in H: \exists t \in T: \map {i_H} h = t}$
Let $T \cap H = \O$.
Then:
:$\nexists h \in H: \exists t \in T: \map {i_H} h = t$
That is:
:$i_H^{-1} \sqbrk T = \O$
That is:
:$i_H^{-1} \sqbrk T = T \cap H$
{{qed|lemma}}
Let $T \cap H \ne \O$.
From Intersection is Subset:
:$H \ne \O$
and:
:$T \ne \O$
From Subset of Empty Set:
:$S \ne \O$
Suppose $i_H^{-1} \sqbrk T = \O$.
Then from Empty Set is Subset of All Sets:
:$i_H^{-1} \sqbrk T \subseteq T \cap H$
Otherwise $i_H^{-1} \sqbrk T \ne \O$.
Let $x \in i_H^{-1} \sqbrk T$.
By the definition of inclusion mapping:
:$\map {i_H} x = x$
By definition of preimage of $T$ under $i_H$:
:$\map {i_H} x \in T$
Thus $x \in T$.
By definition of inclusion mapping:
:$x \in \Dom {i_H} = H$
So $x \in T$ and $x \in H$ and so by definition of set intersection:
:$x \in T \cap H$
Thus by definition of subset:
:$i_H^{-1} \sqbrk T \subseteq T \cap H$
Now let $x \in T \cap H$.
As $H = \Dom {i_H}$ it follows that:
:$x \in \Dom {i_H}$
As $x \in T \cap H$ it follows by definition of set intersection that $x \in T$.
Thus by definition of inclusion mapping again:
:$\map {i_H} x \in T$
and so by definition of preimage of $T$:
:$x \in i_H^{-1} \sqbrk T$
Therefore:
:$x \in T \cap H \implies x \in i_H^{-1} \sqbrk T$
Hence, by definition of subset:
:$T \cap H \subseteq i_H^{-1} \sqbrk T$
{{qed|lemma}}
We have shown that:
:$i_H^{-1} \sqbrk T \subseteq T \cap H$
and:
:$T \cap H \subseteq i_H^{-1} \sqbrk T$
Hence by definition of set equality:
:$T \subseteq S: i_H^{-1} \sqbrk T = T \cap H$
{{qed}}
Category:Inclusion Mappings
Category:Subsets
0u811l1g2h7hqt0rax128f14b9l8yo1
Theorem: Inclusion Mapping is Continuous

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$.
Let $i_H: H \to S$ be the inclusion mapping on $H$.
Then $i_H$ is a $\struct {\tau_H, \tau}$-continuous mapping.

Proof:
Let $I_H$ be the identity mapping on $H$.
From Continuity of Composite with Inclusion: Inclusion on Mapping, $I_H$ is $\tuple {\tau_H , \tau_H}$-continuous {{iff}} $i_H \circ I_H$ is $\tuple {\tau_H , \tau}$-continuous.
From Identity Mapping is Right Identity, it follows that:
:$i_H \circ I_H = i_H$
Therefore, $I_H$ is $\tuple {\tau_H , \tau_H}$-continuous {{iff}} $i_H$ is $\tuple {\tau_H , \tau}$-continuous.
Because of Identity Mapping is Continuous, it follows that $i_H$ is $\tuple {\tau_H , \tau}$-continuous.
{{qed}}
Theorem: Continuity of Composite with Inclusion/Mapping on Inclusion

If $f$ is $\tuple {\tau, \tau'}$-continuous, then $f \circ i$ is $\tuple {\tau_H, \tau'}$-continuous

Proof:
From Inclusion Mapping is Continuous, $i$ is $\tuple {\tau_H, \tau}$-continuous.
It follows from Composite of Continuous Mappings is Continuous that $f \circ i$ is $\tuple {\tau_H, \tau'}$-continuous.
{{qed}}
Theorem: Continuity of Composite with Inclusion/Inclusion on Mapping

$g$ is $\tuple {\tau', \tau_H}$-continuous {{iff}} $i \circ g$ is $\tuple {\tau', \tau}$-continuous.

Proof:
=== Necessary Condition ===
Suppose $g$ is $\tuple {\tau', \tau_H}$-continuous.
From Inclusion Mapping is Continuous, $i$ is $\tuple {\tau_H, \tau}$-continuous.
It follows from Composite of Continuous Mappings is Continuous that $i \circ g$ is $\tuple {\tau', \tau}$-continuous.
Theorem: Continuity of Composite with Inclusion/Uniqueness of Induced Topology

The induced topology $\tau_H$ is the ''only'' topology on $H$ satisfying Continuity of Composite with Inclusion: Inclusion on Mapping for all possible $g$.

Proof:
Suppose $\tau' '$ is a topology on $H$ such that:
:$(1) \quad$ For any topological space $T' = \struct {A', \tau'}$, and
:$(2) \quad$ For any mapping $g: A' \to H$:
$g$ is $\tuple {\tau', \tau' '}$-continuous {{iff}} $i \circ g$ is $\tuple {\tau', \tau}$-continuous.
It needs to be shown that $\tau' '$ must be the same as $\tau_H$.
Let $A' = H$ and $\tau' = \tau' '$.
Let $g$ be the identity mapping on $H$.
From Identity Mapping is Continuous, $g$ is $\tuple {\tau' ', \tau' '}$-continuous
Thus from Composite of Continuous Mappings is Continuous, $i \circ g$ is $\tuple {\tau' ', \tau}$-continuous.
Hence for any $U \in \tau$:
:$\map {\paren {i \circ g}^{-1} } U \in \tau' '$
But:
:$\map {\paren {i \circ g}^{-1} } U = \map {i^{-1} } U = U \cap H$
Hence $\tau_H \subseteq \tau' '$.
Next, take take $A' = H$ and $\tau' = \tau_H$.
Let $g$ be the identity mapping on $H$.
We have that $i \circ g = i$ is $\tuple {\tau_H, \tau}$-continuous,
From Continuity of Composite with Inclusion: Inclusion on Mapping, it follows that $g$ is $\tuple {\tau_H, \tau' '}$-continuous.
But by definition of continuity, this is the same as saying $\tau' ' \subseteq \tau_H$.
So $\tau' ' = \tau_H$, as required.
{{qed}}
Theorem: Products of Open Sets form Local Basis in Product Space

Let $T_1 = \struct {A_1, \tau_1}$ and $T_2 = \struct {A_2, \tau_2}$ be topological spaces.
Let $\struct {T, \tau} = T_1 \times T_2$ be the product space of $T_1$ and $T_2$.
Let $\tuple {x, y} \in A_1 \times A_2$.
Let $W \in \tau$ be an open set of $T$ such that $\tuple {x, y} \in W$.
Then:
:$\exists U_1 \in \tau_1, U_2 \in \tau_2: \tuple {x, y} \in U_1 \times U_2 \subseteq W$
That is, products of open sets from $T_1$ and $T_2$ form a local basis at $\tuple {x, y}$.

Proof:
Let $W \in \tau$ such that $\tuple {x, y} \in W$.
From Natural Basis of Product Topology of Finite Product, $\tau$ is the topology with basis:
:$\BB = \set{U_1 \times U_2: U_1 \in \tau_1, U_2 \in \tau_2}$
Thus $W$ is the union of sets of the form $U_1 \times U_2$ where $U_1 \in \tau_1$ and $U_2 \in \tau_2$.
That is:
:$\exists U_1 \in \tau_1, U_2 \in \tau_2: \tuple{x, y} \in U_1 \times U_2 \subseteq W$
which is what was to be proved.
{{qed}}
Theorem: Open Real Intervals are Homeomorphic

Let $\R$ be the real number line with the Euclidean topology.
Let $I_1 := \openint a b$ and $I_2 := \openint c d$ be non-empty open real intervals.
Then $I_1$ and $I_2$ are homeomorphic.

Proof:
By definition of open real interval, for $I_1$ and $I_2$ to be non-empty it must be the case that $a < b$ and $c < d$.
In particular it is noted that $a \ne b$ and $c \ne d$.
Thus $a - b \ne 0$ and $c - d \ne 0$.
Consider the real function $f: I_1 \to I_2$ defined as:
:$\forall x \in I_1: \map f x = c + \dfrac {\paren {d - c} \paren {x - a} } {b - a}$
Then after some algebra:
:$\forall x \in I_2: \map {f^{-1} } x = a + \dfrac {\paren {b - a} \paren {x - c} } {d - c}$
Both of these are defined as $a - b \ne 0$ and $c - d \ne 0$.
By the Combination Theorem for Continuous Real Functions, both $f$ and $f^{-1}$ are continuous on the open real intervals on which they are defined.
Hence the result by definition of homeomorphic.
{{qed}}
Theorem: Half-Open Real Interval is not Closed in Real Number Line

Let $\R$ be the real number line considered as an Euclidean space.
Let $\hointr a b \subset \R$ be a right half-open interval of $\R$.
Then $\hointr a b$ is not a closed set of $\R$.
Similarly, the left half-open interval $\hointl a b \subset \R$ is not a closed set of $\R$.

Proof:
Consider:
:$A := \R \setminus \hointr a b = \openint \gets a \cup \hointr b \to$
Let $A:= \openint \gets a$ and let $B := \hointr b \to$.
Let $\map {B_\epsilon} b$ be the open $\epsilon$-ball of $b$.
We have that $b - \epsilon < b$ and so $\map {B_\epsilon} b = \openint {b - \epsilon} {b + \epsilon}$ does not lie entirely in $\hointr b \to$.
Now $b - \epsilon$ may itself lie in $A$.
However:
:$\hointr b \to \cap \map {B_\epsilon} b \ne \O$
and so there are elements of $\map {B_\epsilon} b$ which are not in $\openint \gets a \cup \hointr b \to$.
So $\openint \gets a \cup \hointr b \to$ is not an open set of $\R$.
Thus, by definition, $\hointr a b$ is not a closed set of $\R$.
Hence the result.
And {{mutatis}}, the argument also shows that $\hointl a b \subset \R$ is neither an open set nor a closed set of $\R$.
{{qed}}
Theorem: Half-Open Real Interval is Closed in some Open Intervals

Let $\R$ be the real number line considered as an Euclidean space.
Let $\hointr a b \subset \R$ be a half-open interval of $\R$.
Let $c < a$.
Then $\hointr a b$ is a closed set of $\openint c b$.
Similarly, let $d > b$.
Then the half-open interval $\hointl a b$ is a closed set of $\openint a d$.

Proof:
Consider:
:$A := \openint c b \setminus \hointr a b = \openint c a$
Then $A$ is an open interval.
By Open Real Interval is Open Set, $A$ is open in $\R$.
By the definition of the subspace topology it follows that $A$ is open in $\openint c b$.
Thus by the definition of closed set, $\openint c b \setminus A = \hointr a b$ is closed in $\openint c b$.
And {{mutatis}}, the argument also shows that $\hointl a b \subset \R$ is a closed set of $\openint a d$.
{{qed}}
Theorem: Underlying Set of Topological Space is Clopen

Let $T = \struct {S, \tau}$ be a topological space.
Then the underlying set $S$ of $T$ is both open and closed in $T$.

Proof:
From the definition of topology, $S$ is open in $T$.
From Underlying Set of Topological Space is Closed $S$ is closed in $T$.
Hence the result.
{{qed}}
Theorem: Empty Set is Closed/Topological Space

Let $T = \struct {S, \tau}$ be a topological space.
Then $\O$ is closed in $T$.

Proof:
From the definition of closed set, $U$ is open in $T = \struct {S, \tau}$ {{iff}} $S \setminus U$ is closed in $T$.
By definition of topological space, $S$ is open in $T$.
From Set Difference with Self is Empty Set:
:$S \setminus S = \O$
Hence $\O$ is closed in $T$.
{{qed}}
Theorem: Basis induces Local Basis

Let $\struct {S, \tau}$ be a topological space.
Let $\BB$ be an analytic basis for $\tau$.
Let $x \in S$, and denote with $\BB_x$ the set $\set {B \in \BB: x \in B}$.
Then $\BB_x$ is a local basis at $x$.

Proof:
Let $x \in U$, with $U$ an open set of $\tau$.
Since $\BB$ is an analytic basis for $\tau$, we have:
:$U = \ds\bigcup \AA$
for some $\AA \subseteq \BB$.
Since $x \in \ds \bigcup \AA$, there is a $B \in \AA$ such that $x \in B$, by definition of set union.
Hence, by definition of $\BB_x$, $B \in \BB_x$.
From Set is Subset of Union: General Result, we also have:
:$B \subseteq U$
Hence $\BB_x$ is a local basis at $x$.
{{qed}}
Theorem: Fort Space is T0

Let $T = \struct {S, \tau_p}$ be a Fort space on an infinite set $S$.
Then $T$ is a $T_0$ space.

Proof:
Follows directly from:
:Fort Space is $T_1$
:$T_1$ Space is $T_0$ Space
{{qed}}
Category:Fort Spaces
Category:Examples of T0 Spaces
51k0w3v3pxvtbmwsndw2uf55mo5zzuo
Theorem: Pullback Functor is Functor

Let $\mathbf C$ be a metacategory having all pullbacks.
Let $f: C \to D$ be a morphism of $\mathbf C$.
Let $\mathbf C \mathbin / C$ and $\mathbf C \mathbin / D$ be the slice categories over $C$ and $D$, respectively.
Let $f^* : \mathbf C \mathbin / D \to \mathbf C \mathbin / C$ be the pullback functor defined by $f$.
Then $f^*$ is a functor.

Proof:
Let $\alpha: A \to D$ be an object of $\mathbf C \mathbin / D$.
Then the identity morphism $\operatorname{id}_\alpha: \alpha \to \alpha$ is by definition $\operatorname{id}_A: A \to A$.
Thus $f^* \operatorname{id}_\alpha$ is by definition the unique morphism fitting:
::<nowiki>$\begin{xy}\xymatrix@+1em{
 A'
  \ar[rr]^*{f_\alpha}
  \ar[dd]_*{f^* \alpha}
  \ar@{-->}[rd]^*{f^* \mathrm{id}_\alpha}
& &
 A
  \ar[rd]^*{\mathrm{id}_\alpha}
  \ar[dd]^(.4)*{\alpha}
\\ &
 A'
  \ar[ld]^*{f^* \alpha}
  \ar[rr] |{\hole} ^(.3)*{f_\alpha}
& &
 A
  \ar[ld]^*{\alpha}
\\
 C
  \ar[rr]_*{f}
& &
 D
}\end{xy}$</nowiki>
It is apparent that $\operatorname{id}_{A'}$ satisfies this condition.
Since by definition, $\operatorname{id}_{f^* \alpha} = \operatorname{id}_{A'}$, this shows that:
:$f^* \operatorname{id}_\alpha = \operatorname{id}_{f^* \alpha}$
Now let $\gamma_1: \alpha_2 \to \alpha_1$ and $\gamma_2: \alpha_3 \to \alpha_2$ be morphisms of $\mathbf C \mathbin / D$.
Then $f^* \left({\gamma_1 \circ \gamma_2}\right)$ is the unique morphism fitting the dashed arrow in:
::<nowiki>$\begin{xy}\xymatrix@+1em{
 A_3'
  \ar[rr]^*{f_{\alpha_3}}
  \ar[dd]_*{f^* \alpha_3}
  \ar@{-->}[rd]
& &
 A_3
  \ar[rd]^*{\gamma_1 \circ \gamma_2}
  \ar[dd]^(.4)*{\alpha_3}
\\ &
 A_1'
  \ar[ld]^*{f^* \alpha_1}
  \ar[rr] |{\hole} ^(.3)*{f_{\alpha_1}}
& &
 A_1
  \ar[ld]^*{\alpha_1}
\\
 C
  \ar[rr]_*{f}
& &
 D
}\end{xy}$</nowiki>
Unfolding the composition $\gamma_1 \circ \gamma_2$ yields the expanded diagram:
::<nowiki>$\begin{xy}\xymatrix@+1em{
 A_3'
  \ar[rr]^*{f_{\alpha_3}}
  \ar[ddd]_*{f^* \alpha_3}
  \ar[rd]^*{f^* \gamma_2}
  \ar@{-->}@/_/[rdd]
& &
 A_3
  \ar[rd]^*{\gamma_2}
  \ar[ddd]^*{\alpha_3}
\\ &
 A_2'
  \ar[d]^*{f^* \gamma_1}
  \ar[rr] |{\hole} ^(.3)*{f_{\alpha_2}}
& &
 A_2
  \ar[d]^*{\gamma_1}
\\ &
 A_1'
  \ar[ld]^*{f^* \alpha_1}
  \ar[rr] |{\hole} ^(.3)*{f_{\alpha_1}}
& &
 A_1
  \ar[ld]^*{\alpha_1}
\\
 C
  \ar[rr]_*{f}
& &
 D
}\end{xy}$</nowiki>
in which $f^* \left({\gamma_1 \circ \gamma_2}\right)$ again fits the dashed arrow.
But this means, in particular, that we must have:
:$f^* \left({\gamma_1 \circ \gamma_2}\right) = f^* \gamma_1 \circ f^* \gamma_2$
Therefore, $f^*$ is a functor.
{{qed}}
Theorem: Supremum of Bounded Above Set of Reals is in Closure

Let $\R$ be the real number line under the Euclidean metric.
Let $H \subseteq \R$ be a bounded above subset of $\R$ such that $H \ne \O$.
Let $u = \sup H$ be the supremum of $H$.
Then:
:$u \in \map \cl H$
where $\map \cl H$ denotes the closure of $H$ in $\R$.

Proof:
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {B_\epsilon} u$ be the open $\epsilon$-ball of $u$ in $\R$.
From Distance from Subset of Real Numbers:
:$\map d {u, H} = 0$
Thus by definition of distance from subset:
:$\exists x \in H: \map d {u, x} < \epsilon$
Thus $x \in \map {B_\epsilon} u$.
As $x \in H$ and $x \in \map {B_\epsilon} u$, from the definition of intersection:
:$x \in H \cap \map {B_\epsilon} u$
The result follows from Condition for Point being in Closure.
{{qed}}
Theorem: Topological Space is Open Neighborhood of Subset

Let $T = \left({S, \tau}\right)$ be a topological space.
Let $H \subseteq S$ be a subset of $S$.
Then $S$ is an open neighborhood of $H$.

Proof:
From Underlying Set of Topological Space is Clopen, $S$ is open in $T$.
By hypothesis, $H \subseteq S$.
The result follows from Open Superset is Open Neighborhood.
{{qed}}
Category:Topology
Category:Neighborhoods
23fxtpbd2ihzx2sxohd59o0o3q2xfuf
Theorem: Open Superset is Open Neighborhood

Let $T = \struct {S, \tau}$ be a topological space.
Let $U \in \tau$ be an open set of $T$.
Let $H \subseteq U$.
Then $U$ is an open neighborhood of $H$.

Proof:
By hypothesis, $U$ is open in $T$.
Also {{hypothesis}}, $H \subseteq U$.
The result follows by definition of open neighborhood.
{{qed}}
Category:Topology
3ijzgu0t8urimrs49ae4gjsfrubijzl
Theorem: Category has Products and Equalizers iff Pullbacks and Terminal Object

Let $\mathbf C$ be a metacategory.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\mathbf C$ has all finite products and equalizers}}
{{item|(2):|$\mathbf C$ has all pullbacks and a terminal object}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Suppose $\mathbf C$ has all finite products and equalizers.
That $\mathbf C$ has pullbacks follows from Pullback as Equalizer.
That $\mathbf C$ has a terminal object follows by Empty Product is Terminal Object.
{{qed|lemma}}
Theorem: Infimum of Bounded Below Set of Reals is in Closure

Let $\R$ be the real number line with the  usual (Euclidean} metric.
Let $H \subseteq \R$ be a bounded below subset of $\R$ such that $H \ne \O$.
Let $l = \map \inf H$ be the infimum of $H$.
Then:
:$l \in \map \cl H$
where $\map \cl H$ denotes the closure of $H$ in $\R$.

Proof:
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {B_\epsilon} l$ be the open $\epsilon$-ball of $l$ in $\R$.
From Distance from Subset of Real Numbers:
:$\map d {l, H} = 0$
Thus by definition of distance from subset:
:$\exists x \in H: \map d {l, x} < \epsilon$
Thus $x \in \map {B_\epsilon} l$.
As $x \in H$ and $x \in \map {B_\epsilon} l$, from the definition of intersection:
:$x \in H \cap \map {B_\epsilon} l$
The result follows from Condition for Point being in Closure.
{{qed}}
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:
Consider the real number line $\struct {\R, \tau_d}$ with the usual (Euclidean) topology $\tau_d$.
Let:
:$H_n \subseteq \R: H_n = \closedint {\dfrac 1 n} 1$ for $n \ge 2$
where $\closedint {\dfrac 1 n} 1$ denotes the closed real interval from $\dfrac 1 n$ to $1$.
From Closed Real Interval is Closed Set, $\closedint {\dfrac 1 n} 1$ is a closed set of $\struct {\R, \tau_d}$.
Then from Set is Closed iff Equals Topological Closure:
:$\map \cl {H_n} = H_n$
Also:
:$\ds \bigcup_{n \mathop \ge 2} \map \cl {H_n} = \bigcup_{n \mathop \ge 2} H_n = \hointl 0 1$
However:
:$\ds \map \cl {\bigcup_{n \mathop \ge 2} H_n} = \closedint 0 1$
So:
:$\ds \bigcup_{n \mathop \ge 2} \map \cl {H_n} \ne \map \cl {\bigcup_{n \mathop \ge 2} H_n}$