avewright/proofwiki-math huggingface dataset:
Theorem: Matrix is Unitary iff Columns are Orthonormal Basis

Let $\mathbf U$ be an $n \times n$ square matrix over $\mathbb C$.
Then:
:$\mathbf U$ is a unitary matrix
{{Iff}}
:The columns of $\mathbf U$ form an orthonormal basis of $\mathbb C^n$.

Proof:
=== Sufficient Condition ===
Let $\mathbf U$ be unitary.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf U^\dagger
      | r = \mathbf U^{-1}
      | c = {{Defof|Unitary Matrix}}
}}
{{eqn | ll= \leadsto
      | l = \mathbf U^\dagger \mathbf U
      | r = \mathbf U^{-1} \mathbf U
}}
{{eqn | ll= \leadsto
      | l = \mathbf U^\dagger \mathbf U
      | r = \mathbf I_n
}}
{{end-eqn}}
Considering the elements of the matrices on both sides of the above equation:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = [\mathbf U^\dagger \mathbf U]_{i j}
      | r = \mathbf [I_n]_{i j}
}}
{{eqn | ll= \leadsto
      | l = [\mathbf U^\dagger \mathbf U]_{i j}
      | r = \delta_{i j}
      | c = {{Defof|Identity Matrix}}
}}
{{eqn | ll= \leadsto
      | l = \mathbf u_i^\dagger \mathbf u_j
      | r = \delta_{i j}
      | c = $\mathbf u_i^\dagger$ is the $i^{th}$ row of $\mathbf U^\dagger$ and $\mathbf u_j$ is the $j^{th}$ column of $\mathbf U$
}}
{{eqn | ll= \leadsto
      | l = \innerprod {\mathbf u_j} {\mathbf u_i} 
      | r = \delta_{i j}
      | c = {{Defof|Complex Vector Inner Product}}
}}
{{end-eqn}}
Therefore, the columns of $\mathbf U$ are an orthonormal set.
Since $\mathbf U$ is square, its columns are $n$ vectors in $\mathbb C^n$.
By Sufficient Conditions for Basis of Finite Dimensional Vector Space, the columns of $\mathbf U$ form an orthonormal basis of $\mathbb C^n$.
{{qed|lemma}}
Theorem: Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Lemma 1

Let $a: X \to Y, b_1 : Y \to Z_1, b_2 : Y \to Z_2 \in \mathbf C$ be morphisms.
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
&
 X
  \ar[d]_*+{a}
\\
&
 Y
  \ar[ld]_*+{b_1}
  \ar[rd]^*+{b_2}
\\
 Z_1
&
&
 Z_2
}\end{xy}$</nowiki>
Then:
:$\family{b_1 \circ a, b_2 \circ a} = \family{b_1, b_2} \circ a$

Proof:
Consider the diagram:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
&&
 X
  \ar[ldld]_*+{b_1 \circ a}
  \ar[d]^*+{a}
  \ar[rdrd]^*+{b_2 \circ a}
\\
&&
 Y
  \ar[ldl]_*+{b_1}
  \ar@{-->}[d]^*+{\family{b_1, b_2} }
  \ar[rdr]^*+{b_2}
\\
 Z_1
&&
 Z_1 \times Z_2
  \ar[ll]^*+{p_1}
  \ar[rr]_*+{p_2}
&&
 Z_2
}\end{xy}$</nowiki>
This diagram commutes by the binary product UMP applied to $b_1$ and $b_2$.
By definition of the binary product UMP applied to $b_1 \circ a$ and $b_2 \circ a$ the following diagram commutes:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
&&
 X
  \ar[ldld]_*+{b_1 \circ a}
  \ar@{--}[d]^*+{}
  \ar[rdrd]^*+{b_2 \circ a}
\\
&&
  \ar@{-->}[d]^*+{\family{b_1 \circ a, b_2 \circ a} }
\\
 Z_1
&&
 Z_1 \times Z_2
  \ar[ll]^*+{p_1}
  \ar[rr]_*+{p_2}
&&
 Z_2
}\end{xy}$</nowiki>
By the uniqueness of the morphism $\family{b_1 \circ a, b_2 \circ a}$:
:$\family{b_1 \circ a, b_2 \circ a} = \family{b_1, b_2} \circ a$
{{qed}}
Category:Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products
0k1rps17eh1f7blchqbgj5bc4smhg7k
Theorem: Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Lemma 2

Let $a_1: X \to Y_1, a_2: X \to Y_2, b_1 : Y_1 \to Z_1, b_2 : Y_2 \to Z_2 \in \mathbf C$ be morphisms:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
&
 X
  \ar[ld]_*+{a_1}
  \ar[rd]^*+{a_2}
\\
 Y_1
  \ar[d]_*+{b_1}
&&
 Y_2
  \ar[d]^*+{b_2}
\\
 Z_1
&&
 Z_2
}\end{xy}$</nowiki>
Then:
:$\family{b_1 \circ a_1, b_2 \circ a_2} = \paren{b_1 \times b_2} \circ \family{a_1, a_2}$

Proof:
Consider the diagram:
::<nowiki>$\begin{xy}
<0em,5em>*+{X} = "TM",
<-6em,0em>*+{Y_1} = "ML",
<0em,0em>*+{Y_1 \times Y_2} = "MM",
<6em,0em>*+{Y_2} = "MR",
<-6em,-5em>*+{Z_1} = "BL",
<0em,-5em>*+{Z_1 \times Z_2} = "BM",
<6em,-5em>*+{Z_2} = "BR",
"TM";"ML" **\crv{<-4em,5em>} ?>*@{>} ?<>(.8)*!/^.8em/{a_1},
"TM";"MM" **@{--} ?>*@{>} ?<>(.5)*!/_2em/{\family{a_1, a_2} },
"TM";"MR" **\crv{<4em,5em>} ?>*@{>} ?<>(.8)*!/_.8em/{a_2},
"ML";"BL" **@{-} ?>*@{>} ?<>(.3)*!/^.8em/{b_1},
"MM";"ML" **@{-} ?>*@{>} ?<>(.5)*!/_.8em/{p_1},
"MM";"MR" **@{-} ?>*@{>} ?<>(.5)*!/^.8em/{p_2},
"BM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_.8em/{q_1},
"BM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^.8em/{q_2},
"MM";"BM" **@{--} ?>*@{>} ?<>(.5)*!/_2em/{b_1 \times b_2},
"MR";"BR" **@{-} ?>*@{>} ?<>(.3)*!/_.8em/{b_2},
\end{xy}$</nowiki>
This diagram commutes by:
:* the binary product UMP applied to $a_1$ and $a_2$
:* the product of morphisms $b_1$ and $b_2$
By definition of the binary product UMP the following diagram commutes:
::<nowiki>$\begin{xy}
<0em,5em>*+{X} = "TM",
<-6em,-5em>*+{Z_1} = "BL",
<0em,-5em>*+{Z_1 \times Z_2} = "BM",
<6em,-5em>*+{Z_2} = "BR",
"TM";"BL" **\crv{<-6em,4em>} ?>*@{>} ?<>(.7)*!/^2em/{b_1 \circ a_1},
"TM";"BR" **\crv{<5em,4em>} ?>*@{>} ?<>(.7)*!/_2em/{b_2 \circ a_2},
"TM";"BM" **@{--} ?>*@{>} ?<>(.5)*!/_2em/{\family{b_1 \circ a_1,\\ b_2 \circ a_2} },
"BM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_.8em/{q_1},
"BM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^.8em/{q_2},
\end{xy}$</nowiki>
By the uniqueness of the morphism $\family{b_1 \circ a_1, b_2 \circ a_2}$:
:$\family{b_1 \circ a_1, b_2 \circ a_2} = \paren{b_1 \times b_2} \circ \family{a_1, a_2}$
{{qed}}
Category:Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products
evawke4z533njug4keqp1br763g9j93
Theorem: Compact Space is Strongly Paracompact

Let $T = \struct {S, \tau}$ be a compact topological space.
Then $T$ is strongly paracompact.

Proof:
{{Recall|Strongly Paracompact Space|strongly paracompact space}}
{{:Definition:Strongly Paracompact Space}}
Let $T = \struct {S, \tau}$ be a compact topological space.
{{Recall|Compact Topological Space|compact topological space}}
{{:Definition:Compact Topological Space/Definition 1}}
Let $\CC$ be an arbitrary open cover for $S$.
Then by definition of compact space, $\CC$ has a finite subcover $\CC'$.
From {{Corollary|Subcover is Refinement of Cover}}, $\CC'$ is an open refinement of $\CC$.
From Finite Cover is Star-Finite, $\CC'$ is star-finite.
As $\CC$ is arbitrary, it follows that every open cover for $S$ has an open refinement which is star-finite.
Hence the result by definition of strongly paracompact space.
{{qed}}
Theorem: Finite Cover is Star-Finite

Let $T = \struct {S, \tau}$ be a topological space.
Let $\CC$ be a finite cover for $T$.
Then $\CC$ is star-finite.

Proof:
{{Recall|Star-Finite|star-finite}}
{{:Definition:Star-Finite}}
Let $\CC$ be a finite cover for $T$.
Let $H \in \CC$.
As $\CC$ is a finite set, it follows trivially that only a finite number of elements of $\CC$ intersect $H$.
Hence the result.
{{qed}}
Category:Star-Finite
Category:Covers
73eh4e2pdx5dj2hdke1fdb2mswybmdh
Theorem: Locally Finite Refinement is Point Finite

Let $\CC$ be a cover of a topological space $T = \struct {S, \tau}$.
Let $\UU$ be a locally finite refinement of $\CC$.
Then $\UU$ is also a point finite refinement of $\CC$.

Proof:
{{Recall|Locally Finite Cover|locally finite cover}}
{{:Definition:Locally Finite Cover}}
{{Recall|Point Finite Cover|point finite cover}}
{{:Definition:Point Finite Cover}}
Let $\UU$ be a locally finite refinement of a cover $\CC$ of $S$.
Let $x \in S$.
Then there exists some neighborhood $N_x$ of $x$ which intersects only finitely many elements of $\UU$.
Thus $x$ itself can be in only finitely many elements of $\UU$.
That is, $\UU$ is a refinement of $\CC$ which is point finite.
{{qed}}
Theorem: Submetacompact Space is Countably Metacompact

Let $T = \struct {S, \tau}$ be a submetacompact topological space.
Then $T$ is countably metacompact.

Proof:
{{Recall|Countably Metacompact Space|countably metacompact space}}
{{:Definition:Countably Metacompact Space}}
Let $T = \struct {S, \tau}$ be a submetacompact space.
{{Recall|Submetacompact Space|submetacompact space}}
{{:Definition:Submetacompact Space}}
{{ProofWanted}}
Theorem: Pseudometrizable Space has Sigma-Locally Finite Basis

Let $T = \struct {S, \tau}$ be a pseudometrizable topological space.
Then $T$ has a basis that is $\sigma$-locally finite.

Proof:
=== Construction of Basis $\VV$ ===
We construct a $\sigma$-locally finite basis $\VV$.
For each $n \in \N$, let:
:$\UU_n = \set {\map {B_{1 / 2^n} } x : x \in S}$
That is, $\UU_n$ is the set of all open balls of radius $\dfrac 1 {2^n}$.
From Open Balls of Same Radius form Open Cover:
:$\forall n \in \N: \UU_n$ is an open cover of $T$
{{finish|It needs to be established that there is a metric space associated with $T$ so the next line is appropriate}}
From Metric Space is Paracompact:
:$T$ is a paracompact space
By definition of paracompact space:
:$\forall n \in \N : \exists$ a open refinement $\VV_n$ of $\UU_n$ which is locally finite
Let $\VV = \ds \bigcup_{n \mathop in \N} \VV_n$.
By definition, $\VV$ is $\sigma$-locally finite.
{{qed|lemma}}
Theorem: Hermitian Conjugate of Unitary Matrix is Unitary

The Hermitian conjugate of a unitary matrix is unitary.

Proof:
Let $\mathbf U$ be unitary.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf U
      | r = \mathbf U
}}
{{eqn | ll=\leadsto
      | l = \paren {\mathbf U^\dagger}^\dagger
      | r = \paren {\mathbf U^{-1} }^{-1}
      | c = Hermitian Conjugate is Involution
}}
{{eqn | ll=\leadsto
      | l = \paren {\mathbf U^\dagger}^\dagger
      | r = \paren {\mathbf U^\dagger}^{-1}
      | c = $\mathbf U$ is unitary
}}
{{end-eqn}}
Thus, $\mathbf U^\dagger$ is unitary.
{{qed}}
Category:Unitary Matrices
Category:Hermitian Conjugates
7vuwoj2jzppuotbl9oqdkk0pfph5ksf
Theorem: Countable Anticompact Space has Countable K-Network

Let $T = \struct {S, \tau}$ be a countable anticompact topological space.
Then $T$ has a countable $k$-network.

Proof:
{{Recall|K-Network|$k$-network}}
{{:Definition:K-Network/K-Network}}
Let $T = \struct {S, \tau}$ be a countable anticompact topological space.
{{Recall|Anticompact Space|anticompact space}}
{{:Definition:Anticompact Space}}
Let $\VV$ be the set of all singleton subsets of $S$.
For all $U \in \VV$, $U$ is a compact subspace of $S$.
Hence trivially every compact subspace of $S$ is the union of elements of $\VV$.
Hence $\VV$ is a $k$-network.
As $T$ is countable, it follows that $\VV$ is likewise countable.
{{qed}}
Theorem: T3 Space with Sigma-Locally Finite Basis is Pseudometrizable

Let $T = \struct {S, \tau}$ be a $T_3$ topological space.
Let $\BB$ be a $\sigma$-locally finite basis of $T$.
Then $T$ is pseudometrizable.

Proof:
{{ProofWanted|see Nagata-Smirnov Metrization Theorem/Sufficient Condition}}
Theorem: Spectral Theorem for Real Symmetric Matrices

Let $\mathbf A$ be a square matrix.
Then $\mathbf A$ is a real symmetric matrix {{Iff}} it is diagonalizable to a real diagonal matrix via an orthogonal transformation.
That is, we can write:
:$\mathbf A = \mathbf U \mathbf D \mathbf U^\intercal$
where:
:$\mathbf D$ is a real diagonal matrix
:$\mathbf U$ is a real orthogonal matrix 
:$\mathbf U^\intercal$ is the transpose of $\mathbf U$.

Proof:
=== Necessary Case ===
Let $\mathbf A$ be diagonalizable to a real diagonal matrix via an orthogonal transformation.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf A^\intercal
      | r = \paren {\mathbf U \mathbf D \mathbf U^\intercal}^\intercal
}}
{{eqn | r = \mathbf U \mathbf D^\intercal \mathbf U^\intercal
      | c = Transpose of Matrix Product and Transpose of Transpose of Matrix
}}
{{eqn | r = \mathbf U \mathbf D \mathbf U^\intercal
      | c = $\mathbf D$ is diagonal
}}
{{eqn | r = \mathbf A
}}
{{end-eqn}}
Thus, $\mathbf A$ is symmetric.
Since $\mathbf U$ and $\mathbf D$ are real, $\mathbf A$ must be real, as well.
{{qed|lemma}}
Theorem: Hermitian Conjugate of Real Matrix is Transpose

Let $\mathbf A$ be a real matrix.
Then:
:$\mathbf A^\dagger = \mathbf A^\intercal$
where
:$\mathbf A^\dagger$ is the Hermitian conjugate of $\mathbf A$
:$\mathbf A^\intercal$ is the transpose of $\mathbf A$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf A^\dagger
      | r = \overline {\paren {\mathbf A^\intercal} }
      | c = {{Defof|Hermitian Conjugate}}
}}
{{eqn | r = \mathbf A^\intercal
      | c = Complex Number equals Conjugate iff Wholly Real
}}
{{end-eqn}}
{{qed}}
Category:Hermitian Conjugates
Category:Transposes of Matrices
ndoe4vcjl74dbdoxg87bmiqyla0u14g
Theorem: Identity Morphism of Coproduct

Let $\mathbf C$ be a metacategory.
Let $C$ and $D$ be objects of $\mathbf C$, and let $C \sqcup D$ be a binary coproduct for $C$ and $D$.
Then:
:$\operatorname{id}_{\paren {C \mathop \sqcup D} } = \operatorname{id}_C \sqcup \operatorname{id}_D$
where $\operatorname{id}$ denotes an identity morphism, and $\sqcup$ signifies a coproduct of morphisms.

Proof:
By definition of the coproduct morphism $\operatorname{id}_C \sqcup \operatorname{id}_D$, it is the unique morphism making:
$\quad\quad \begin{xy}\xymatrix@+1em@L+5px{
C
\ar[r]^*+{i_1}
\ar[d]_*+{\operatorname{id}_C}
&
C \sqcup D
\ar@{-->}[d]^*+{\operatorname{id}_C \sqcup \operatorname{id}_D}
&
D
\ar[l]_*+{i_2}
\ar[d]^*+{\operatorname{id}_D}
\\
C
\ar[r]_*+{i_1}
&
C \sqcup D
&
D
\ar[l]^*+{i_2}
}\end{xy}$
a commutative diagram.
By the behaviour of identity morphisms the diagram:
$\quad\quad \begin{xy}\xymatrix@+1em@L+5px{
C
\ar[r]^*+{i_1}
\ar[d]_*+{\operatorname{id}_C}
&
C \sqcup D
\ar@{-->}[d]^*+{\operatorname{id}_{C \mathop \sqcup D} }
&
D
\ar[l]_*+{i_2}
\ar[d]^*+{\operatorname{id}_D}
\\
C
\ar[r]_*+{i_1}
&
C \sqcup D
&
D
\ar[l]^*+{i_2}
}\end{xy}$
is a commutative diagram.
The identity morphism $\operatorname{id}_{\paren {C \mathop \sqcup D} }$ is the unique morphism sought.
{{qed}}
Category:Morphisms
8ywoxrhdhlno85fqzntftpi0e2hy0w2
Theorem: Coproduct of Composite Morphisms

Let $\mathbf C$ be a metacategory.
Let $f \sqcup f': A \sqcup A' \to B \sqcup B'$ and $g \sqcup g': B \sqcup B' \to C \sqcup C'$ be two composable coproducts of morphisms in $\mathbf C$.
Then:
:$\paren {g \circ f} \sqcup \paren {g' \circ f'} = \paren {g \sqcup g'} \circ \paren {f \sqcup f'}$
where $\sqcup$ signifies coproducts of morphisms.

Proof:
The situation is efficiently captured in the following commutative diagram:
$\quad\quad \begin{xy}
<-5em,0em>*+{A}            = "A",
<0em,0em>*+{A \sqcup A'}   = "P",
<5em,0em>*+{A'}            = "A2",
<-5em,-5em>*+{B}           = "B",
<0em,-5em>*+{B \sqcup B'}  = "Q",
<5em,-5em>*+{B'}           = "B2",
<-5em,-10em>*+{C}          = "C",
<0em,-10em>*+{C \sqcup C'} = "R",
<5em,-10em>*+{C'}          = "C2",
"A";"P"  **@{-} ?>*@{>} ?*!/_.8em/{i_1},
"A2";"P" **@{-} ?>*@{>} ?*!/^.8em/{i_2},
"B";"Q"  **@{-} ?>*@{>} ?*!/_.8em/{i_1},
"B2";"Q" **@{-} ?>*@{>} ?*!/^.8em/{i_2},
"C";"R"  **@{-} ?>*@{>} ?*!/^.8em/{i_1},
"C2";"R" **@{-} ?>*@{>} ?*!/_.8em/{i_2},
"A";"B"   **@{-} ?>*@{>}  ?*!/^.8em/{f},
"A2";"B2" **@{-} ?>*@{>}  ?*!/_.8em/{f'},
"P";"Q"   **@{--} ?>*@{>} ?*!/_1.4em/{f \sqcup f'},
"B";"C"   **@{-} ?>*@{>}  ?*!/^.8em/{g},
"B2";"C2" **@{-} ?>*@{>}  ?*!/_.8em/{g'},
"Q";"R"   **@{--} ?>*@{>} ?*!/_1.4em/{g \sqcup g'},
\end{xy}$
By definition of the coproduct morphism $\paren {g \circ f} \sqcup \paren {g' \circ f'}$, it is the unique morphism making:
$\quad\quad \begin{xy}
<-5em,0em>*+{A}            = "A",
<0em,0em>*+{A \sqcup A'}   = "P",
<5em,0em>*+{A'}            = "A2",
<-5em,-10em>*+{C}          = "C",
<0em,-10em>*+{C \sqcup C'} = "R",
<5em,-10em>*+{C'}          = "C2",
"A";"P"  **@{-} ?>*@{>} ?*!/_.8em/{i_1},
"A2";"P" **@{-} ?>*@{>} ?*!/^.8em/{i_2},
"C";"R"  **@{-} ?>*@{>} ?*!/^.8em/{i_1},
"C2";"R" **@{-} ?>*@{>} ?*!/_.8em/{i_2},
"A";"C"   **@{-} ?>*@{>}  ?*!/^1.5em/{g \circ f},
"A2";"C2" **@{-} ?>*@{>}  ?*!/_1.8em/{g' \circ f'},
"P";"R"   **@{--} ?>*@{>} ?*!/_2em/{\paren {g \circ f} \sqcup \\ \paren {g' \circ f'} },
\end{xy}$
a commutative diagram.
The uniqueness of $\paren {g \circ f} \sqcup \paren {g' \circ f'}$ implies it equals $\paren {g \sqcup g'} \circ \paren {f \sqcup f'}$.
{{qed}}
Category:Product Categories
Category:Morphisms
bqn89lxscf50mguumqp14fhi1o1xm8h
Theorem: Lindelöf Space is Meta-Lindelöf

Let $T = \struct{S, \tau}$ be a Lindelöf space.
Then $T = \struct{S, \tau}$ is also a meta-Lindelöf space.

Proof:
{{Recall|Meta-Lindelöf Space|meta-Lindelöf space}}
{{:Definition:Meta-Lindelöf Space}}
Let $T = \struct{S, \tau}$ be a Lindelöf space.
{{Recall|Lindelöf Space|Lindelöf space}}
{{:Definition:Lindelöf Space}}
Let $\CC$ be an open cover of $S$.
Then by Countable Cover is Point Countable, $\CC$ is an open point countable cover.
By Cover is Refinement of Itself, $\CC$ is a refinement of itself.
Hence $\CC$ is a point countable open refinement of itself.
The result follows.
{{qed}}
Theorem: Countable Cover is Point Countable

Let $S$ be a set.
Let $\CC$ be a countable cover of $S$.
Then $\CC$ is a point countable cover of $S$.

Proof:
Let $\CC$ be a countable cover of a set $S$.
Let $x$ be a point of $S$.
As $\CC$ is a countable set of sets, $x$ can be an element of only a countable number of elements of $\CC$.
Hence the result, by definition of point countable cover. 
{{qed}}
Theorem: Cover is Refinement of Itself

Let $S$ be a set.
Let $\CC$ be a cover for $S$.
Then $\CC$ is a refinement of $\CC$ itself.

Proof:
From Set is Subset of Itself, $\CC$ is a subcover of itself.
From Subcover is Refinement of Cover, $\CC$ is a refinement of itself.
Hence the result.
{{qed}}
Category:Refinements of Covers
Category:Covers
c3yb90hrnczsaefmu905f6vm5usxiub
Theorem: Weakly Locally Compact R1 Space is T3.5

Let $T = \struct {S, \tau}$ be an $R_1$ space which is weakly locally compact.
Then $T$ is a $T_{3 \frac 1 2}$ space.

Proof:
{{Recall|T3.5 Space|$T_{3 \frac 1 2}$ space}}
{{:Definition:T3.5 Space/Definition 1}}
Let $T = \struct {S, \tau}$ be a weakly locally compact $R_1$ space.
{{Recall|Weakly Locally Compact Space|weakly locally compact space}}
{{:Definition:Weakly Locally Compact Space}}
{{ProofWanted}}
Theorem: T2 Space is R1

Let $\struct {S, \tau}$ be a $T_2$ (Hausdorff) space.
Then $\struct {S, \tau}$ is also a $R_1$ space.

Proof:
Let $T$ be a $T_2$ space.
{{Recall|T2 Space|$T_2$ space}}
{{:Definition:T2 Space/Definition 3}}
By $T_2$ Space is $T_1$ and $T_1$ Space is $T_0$, $T$ is a $T_0$ space.
Hence by definition, for every pair of points $x, y \in T$, $x$ and $y$ are topologically distinguishable.
{{Recall|R1 Space|$R_1$ space}}
{{:Definition:R1 Space}}
The result follows.
{{qed}}
Theorem: Diagonal Functor on Product Category has Left Adjoint Iff Category has Binary Coproducts/Lemma 1

Let $a_1 : X_1 \to Y, a_2 : X_2 \to Y, b: Y \to Z \in \mathbf C$ be morphisms.
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 X_1
  \ar[rd]_*+{a_1}
&
&
 X_2
  \ar[ld]^*+{a_2}
\\
& 
 Y
  \ar[d]_*+{b}
\\
&
 Z
}\end{xy}$</nowiki>
Then:
:$\sqbrk{b \circ a_1, b \circ a_2} = b \circ \sqbrk{a_1, a_2}$

Proof:
Consider the diagram:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 X_1
  \ar[rr]^*+{i_1}
  \ar[rdr]_*+{a_1}
  \ar[rdrd]_*+{b \circ a_1}
&&
 X_1 \sqcup X_2
  \ar@{-->}[d]^*+{\sqbrk{a_1, a_2} }
&&
 X_2
  \ar[ll]_*+{i_2}
  \ar[ldl]^*+{a_2}
  \ar[ldld]^*+{b \circ a_2}
\\
&&
 Y
  \ar[d]^*+{b}
\\
&&
 Z
}\end{xy}$</nowiki>
This diagram commutes by the binary coproduct UMP applied to $a_1$ and $a_2$.
By definition of the binary coproduct UMP applied to $b \circ a_1$ and $b \circ a_2$ the following diagram commutes:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 X_1
  \ar[rr]^*+{i_1}
  \ar[rdrd]_*+{b \circ a_1}
&&
 X_1 \sqcup X_2
  \ar@{--}[d]^*+{\sqbrk{b \circ a_1, b \circ a_2} }
&&
 X_2
  \ar[ll]_*+{i_2}
  \ar[ldld]^*+{b \circ a_2}
\\
&&
  \ar@{-->}[d]^*+{}
\\
&&
 Z
}\end{xy}$</nowiki>
By the uniqueness of the morphism $\sqbrk{b \circ a_1, b \circ a_2}$:
:$\sqbrk{b \circ a_1, b \circ a_2} = b \circ \sqbrk{a_1, a_2}$
{{qed}}
Category:Diagonal Functor on Product Category has Left Adjoint Iff Category has Binary Coproducts
33567nnkfss4ox0dlfqmbqq1y4seq1f
Theorem: Diagonal Functor on Product Category has Left Adjoint Iff Category has Binary Coproducts/Lemma 2

Let $a_1: X_1 \to Y_1, a_2: X_1 \to Y_2, b_1 : Y_1 \to Z, b_2 : Y_2 \to Z \in \mathbf C$ be morphisms:
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 X_1
  \ar[d]_*+{a_1}
&&
 X_2
  \ar[d]^*+{a_2}
\\
 Y_1
  \ar[rd]_*+{b_1}
&&
 Y_2
  \ar[ld]^*+{b_2}
\\
&
 Z
}\end{xy}$</nowiki>
Then:
:$\sqbrk{b_1 \circ a_1, b_2 \circ a_2} = \sqbrk{b_1, b_2} \circ \paren{a_1 \sqcup a_2}$

Proof:
Consider the diagram:
::<nowiki>$\begin{xy}
<-6em,5em>*+{X_1} = "TL",
<0em,5em>*+{X_1 \sqcup X_2} = "TM",
<6em,5em>*+{X_2} = "TR",
<-6em,0em>*+{Y_1} = "ML",
<0em,0em>*+{Y_1 \sqcup Y_2} = "MM",
<6em,0em>*+{Y_2} = "MR",
<0em,-5em>*+{Z} = "BM",
"TL";"TM" **@{-} ?>*@{>} ?<>(.5)*!/_.8em/{i_1},
"TR";"TM" **@{-} ?>*@{>} ?<>(.5)*!/^.8em/{i_2},
"TM";"MM" **@{--} ?>*@{>} ?<>(.5)*!/_2em/{a_1 \sqcup a_2},
"TR";"MR" **@{-} ?>*@{>} ?<>(.3)*!/_.8em/{a_2},
"TL";"ML" **@{-} ?>*@{>} ?<>(.3)*!/^.8em/{a_1},
"ML";"MM" **@{-} ?>*@{>} ?<>(.5)*!/_.8em/{j_1},
"MR";"MM" **@{-} ?>*@{>} ?<>(.5)*!/^.8em/{j_2},
"ML";"BM" **\crv{<-4em,-5em>} ?>*@{>} ?<>(.5)*!/^.8em/{b_1},
"MM";"BM" **@{--} ?>*@{>} ?<>(.5)*!/_2em/{\sqbrk{b_1, b_2} },
"MR";"BM" **\crv{<4em,-5em>} ?>*@{>} ?<>(.5)*!/_.8em/{b_2},
\end{xy}$</nowiki>
This diagram commutes by:
:* the coproduct of morphisms $a_1$ and $a_2$
:* the binary coproduct UMP applied to $b_1$ and $b_2$
By definition of the binary coproduct UMP applied to $b_1 \circ a_1$ and $b_2 \circ a_2$ the following diagram commutes:
::<nowiki>$\begin{xy}
<-6em,5em>*+{X_1} = "TL",
<0em,5em>*+{X_1 \sqcup X_2} = "TM",
<6em,5em>*+{X_2} = "TR",
<0em,-5em>*+{Z} = "BM",
"TL";"TM" **@{-} ?>*@{>} ?<>(.5)*!/_.8em/{i_1},
"TR";"TM" **@{-} ?>*@{>} ?<>(.5)*!/^.8em/{i_2},
"TL";"BM" **\crv{<-6em,-4em>} ?>*@{>} ?<>(.3)*!/^2em/{b_1 \circ a_1},
"TR";"BM" **\crv{<5em,-4em>} ?>*@{>} ?<>(.3)*!/_2em/{b_2 \circ a_2},
"TM";"BM" **@{--} ?>*@{>} ?<>(.5)*!/_2em/{\sqbrk{b_1 \circ a_1,\\ b_2 \circ a_2} },
\end{xy}$</nowiki>
By the uniqueness of the morphism $\sqbrk{b_1 \circ a_1, b_2 \circ a_2}$:
:$\sqbrk{b_1 \circ a_1, b_2 \circ a_2} = \sqbrk{b_1, b_2} \circ \paren{a_1 \sqcup a_2}$
{{qed}}
Category:Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products
qyojmlepmn47s4kjcryqetlxh87q4j3
Theorem: First-Countable T2 Countably Compact Space is Regular

Let $\struct {S, \tau}$ be a first-countable $T_2$ (Hausdorff) space which is countably compact.
Then $\struct {S, \tau}$ is also a regular space.

Proof:
{{Recall|Regular Space|regular space}}
{{:Definition:Regular Space/Definition 3}}
So, let $\struct {S, \tau}$ be a first-countable $T_2$ (Hausdorff) space which is countably compact.
Let $A$ be a closed set of $T$.
Let $x \notin A$ be a point of $S$ which is not in $A$.
{{Recall|First-Countable Space|first-countable space}}
{{:Definition:First-Countable Space}}
Let $\family {U_n}_{n \mathop \in \N}$ be a countable local basis for $x$.
Because $T$ is a $T_2$ space, the (countably many) open sets $S \setminus \overline {U_n}$ cover $A$.
{{explain|why?}}
Since $A$ is closed in $T$, it is also countably compact.
{{explain|why?}}
{{Recall|Countably Compact Space|countably compact space}}
{{:Definition:Countably Compact Space/Definition 1}}
Consequently:
:$A \subseteq \ds \bigcup_{n \mathop \in I} \paren {S \setminus \overline {U_n} }$
for some finite $I \subseteq \N$.
Taking complements, one sees that:
:$\ds \bigcap_{n \mathop \in I} \overline {U_n}$
which is a closed neighborhood of $x$, is disjoint from $A$.
{{qed}}
Theorem: Topological Space with Countable Network has Sigma-Locally Finite Network

Let $T = \struct {S, \tau}$ be a topological space which has a countable network.
Then $T$ has a $\sigma$-locally finite network.

Proof:
{{ProofWanted|Clarification needed as to the nature of a $\sigma$-locally finite set decoupled from the context of a topological space}}
Theorem: Strongly Paracompact Space is Paracompact

Let $T = \struct {S, \tau}$ be a strongly paracompact space.
Then $T$ is paracompact.

Proof:
{{Recall|Paracompact Space|paracompact space}}
{{:Definition:Paracompact Space}}
Let $T = \struct {S, \tau}$ be a strongly paracompact space.
{{Recall|Strongly Paracompact Space|strongly paracompact space}}
{{:Definition:Strongly Paracompact Space}}
The result follows directly from Star-Finite Set is Locally Finite.
{{qed}}
Theorem: Star-Finite Set is Locally Finite

Let $S$ be a set.
Let $\FF$ be a set of subsets of $S$ which is '''star-finite'''.
Then $\FF$ is locally finite.

Proof:
{{Recall|Locally Finite Set of Subsets|locally finite}}
{{:Definition:Locally Finite Set of Subsets}}
Let $\FF \subseteq \powerset S$ be '''star-finite'''.
{{Recall|Star-Finite|star-finite}}
{{:Definition:Star-Finite}}
{{ProofWanted}}