avewright/proofwiki-math huggingface dataset:
Theorem: Sorgenfrey's Half-Open Square Topology is Not Paracompact

Let $T$ be a Sorgenfrey's half-open square.
Then $T$ is not a paracompact space.

Proof:
From Sorgenfrey's Half-Open Square Topology is Not Countably Paracompact, $T$ is not a countably paracompact space.
Hence from Paracompact Space is Countably Paracompact, $T$ cannot be a paracompact space.
{{qed}}
Category:Sorgenfrey's Half-Open Square Topology
Category:Examples of Paracompact Spaces
gm4ufdjt9hsiwyfmzyh04kyksji0chp
Theorem: Sorgenfrey Line is Metacompact

The Sorgenfrey line is a metacompact space.

Proof:
Follows from:
:Sorgenfrey Line is Paracompact
:Paracompact Space is Metacompact.
{{qed}}
Category:Sorgenfrey Line
Category:Examples of Metacompact Spaces
nv02tfv2k8bo2qfz64zxmb2jdl0qngi
Theorem: Sorgenfrey's Half-Open Square Topology is Not Metacompact

Let $T$ be a Sorgenfrey's half-open square.
Then $T$ is not a metacompact space.

Proof:
{{ProofWanted}}
Category:Sorgenfrey's Half-Open Square Topology
Category:Examples of Metacompact Spaces
pxiwzunufnfkiuv0m7ekfysfaa9oa0a
Theorem: Irreducible Space is not necessarily Ultraconnected

Let $T = \struct {S, \tau}$ be a topological space which is irreducible.
Then it is not necessarily the case that $T$ is ultraconnected.

Proof:
Let $T = \struct {S, \tau_p}$ be a particular point space with at least three points.
From Particular Point Space is Irreducible, $T$ is an irreducible space.
From Particular Point Space is not Ultraconnected, $T$ is not an ultraconnected space.
{{qed}}
Theorem: Ultraconnected Space is not necessarily Irreducible

Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then it is not necessarily the case that $T$ is irreducible.

Proof:
Let $T = \struct {S, \tau_{\bar p} }$ be an excluded point space with at least three points.
By Excluded Point Space is Ultraconnected, $T$ is an ultraconnected space.
By Excluded Point Space is not Irreducible, $T$ is not an irreducible space.
{{qed}}
Theorem: Components and Quasicomponents of Arens-Fort Space are Equal

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Let $A \subseteq S$ be a subset of $T$.
Then:
:$A$ is a component of $T$
{{iff}}:
:$A$ is a quasicomponent of $T$.

Proof:
{{ProofWanted}}
Category:Arens-Fort Space
Category:Examples of Topological Components
Category:Examples of Quasicomponents
8txk5dn9z78hccegwsxeyv2p86v0fqp
Theorem: Extended Topologist's Sine Curve is Path-Connected

Let $T$ be the extended topologist's sine curve.
Then $T$ is path-connected.

Proof:
From Extended Topologist's Sine Curve is Injectively Path-Connected we have that $T$ is injectively path-connected.
The result follows from Injectively Path-Connected Space is Path-Connected.
{{qed}}
Theorem: Union of Adjacent Open Intervals is Locally Path-Connected

Let $T = \struct {S, \tau_S}$ be the union of adjacent open intervals:
:$S = \openint a b \cup \openint b c$
where:
:$a, b, c \in \R: a < b < c$.
:$\tau_S$ is the subspace topology induced on $S$ by the usual topology $\tau_d$ on the real numbers $\R$.
Then $T$ is locally path-connected.

Proof:
From Union of Adjacent Open Intervals is Locally Injectively Path-Connected, $T$ is locally injectively path-connected.
The result follows from Locally Injectively Path-Connected Space is Locally Path-Connected.
{{qed}}
Category:Union of Adjacent Open Intervals
Category:Examples of Locally Path-Connected Spaces
h4vq2tt6ft7e9mqyxer6qpqxgkejiue
Theorem: Union of Adjacent Open Intervals is not Path-Connected

Let $T = \struct {S, \tau_S}$ be the union of adjacent open intervals:
:$S = \openint a b \cup \openint b c$
where:
:$a, b, c \in \R: a < b < c$.
:$\tau_S$ is the subspace topology induced on $S$ by the usual topology $\tau_d$ on the real numbers $\R$.
Then $T$ is ''not'' path-connected.

Proof:
{{Recall|Path-Connected Space|path-connected space}}
{{:Definition:Path-Connected Space}}
So, let $T$ be the union of adjacent open intervals as defined {{hypothesis}}.
Let $x \in \openint a b$.
Let $y \in \openint b c$.
Let $\I := \closedint 0 1$ denote the closed unit interval.
{{AimForCont}} there exists a path $f: \I \to S$ such that:
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = x
}}
{{eqn | l = \map f 1
      | r = y
}}
{{end-eqn}}
Then by Continuous Image of Closed Real Interval is Closed Real Interval:
:$f \sqbrk \I = \closedint x y$
Hence it follows that:
:$\exists S \in \I: b = \map f s$ for some $s \in \I$.
But $b \notin \openint a b \cup \openint b c$ by definition of union of adjacent open intervals.
This contradicts our assertion that such an $f$ exists.
Hence $f$ cannot exist.
The result follows by definition of path-connected.
{{qed}}
Category:Union of Adjacent Open Intervals
Category:Examples of Path-Connected Spaces
sc491hsbzratn8s94p2afuh3ynawnvl
Theorem: Union of Adjacent Open Intervals is Locally Injectively Path-Connected

Let $T = \struct {S, \tau_S}$ be the union of adjacent open intervals:
:$S = \openint a b \cup \openint b c$
where:
:$a, b, c \in \R: a < b < c$.
:$\tau_S$ is the subspace topology induced on $S$ by the usual topology $\tau_d$ on the real numbers $\R$.
Then $T$ is locally injectively path-connected.

Proof:
{{Recall|Locally Injectively Path-Connected Space|locally injectively path-connected space}}
{{Definition:Locally Injectively Path-Connected Space}}
Consider:
:$\BB := \set {\openint x y: x, y \in \R \cap \openint a b, x < y} \cup \set {\openint x y: x, y \in \R \cap \openint b c, x < y}$ 
From Basis for Union of Adjacent Open Intervals, $\BB$ is a basis for $T$.
From Real Interval is Injectively Path-Connected, the real intervals that go to make $\BB$ are all injectively path-connected sets.
Hence the result.
{{qed}}
Category:Union of Adjacent Open Intervals
Category:Examples of Locally Injectively Path-Connected Spaces
h1qsd51sftk0zitpw3p9iv0v56d4r2b
Theorem: Union of Adjacent Open Intervals is not Injectively Path-Connected

Let $T = \struct {S, \tau_S}$ be the union of adjacent open intervals:
:$S = \openint a b \cup \openint b c$
where:
:$a, b, c \in \R: a < b < c$.
:$\tau_S$ is the subspace topology induced on $S$ by the usual topology $\tau_d$ on the real numbers $\R$.
Then $T$ is ''not'' injectively path-connected.

Proof:
From Union of Adjacent Open Intervals is not Path-Connected, $T$ is not path-connected.
The result follows from Injectively Path-Connected Space is Path-Connected.
{{qed}}
Category:Union of Adjacent Open Intervals
Category:Examples of Injectively Path-Connected Spaces
rxq8yynk8544lhbkad118ybna902rs5
Theorem: Real Interval is Injectively Path-Connected

Let $\struct {\R, \tau_d}$ be the real number line under the Euclidean topology.
Let $T = \struct {S, \tau}$ be a real interval under the topology induced by $\tau_d$, which is also the Euclidean topology.
Then $T$ is injectively path-connected.

Proof:
{{Recall|Injectively Path-Connected Space|injectively path-connected space}}
{{Definition:Injectively Path-Connected Space}}
Let $a, b \in S$ be arbitrary such that $a < b$.
Let $\I$ denote the closed unit interval $\closedint 0 1$.
Let us define the injection $f: \I \to S$ as:
:$\forall x \in \I: \map f x = a + \paren {b - a} x$
Its injectivity is trivial, as is its continuouscontinuity.
We see that:
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = a + 0 b
      | c = 
}}
{{eqn | r = a
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map f 1
      | r = a + \paren {b - a} \times 1
      | c = 
}}
{{eqn | r = b
      | c = 
}}
{{end-eqn}}
We have that $a$ and $b$ are arbitrary, so we can progress to an instance of universal generalization and declare that:
:for all $a$ and $b$ in $S$, there exists a continuouscontinuous injection from $\I$ to $S$.
Hence the result, by definition of injectively path-connected space.
{{qed}}
Category:Real Intervals
Category:Examples of Injectively Path-Connected Spaces
c1imqzytl1g3um9upcx52i6rpl8m2m9
Theorem: Basis for Union of Adjacent Open Intervals

<onlyinclude>
Let $T = \struct {S, \tau_S}$ be the union of adjacent open intervals considered as a topological space:
:$S = \openint a b \cup \openint b c$
Let $\BB_1$ and  $\BB_2$ be the set of subsets of $\R$ defined as:
{{begin-eqn}}
{{eqn | l = \BB_1
      | r = \set {\openint x y: x, y \in \R \cap \openint a b, x < y}
      | c = 
}}
{{eqn | l = \BB_2
      | r = \set {\openint x y: x, y \in \R \cap \openint b c, x < y}
      | c = 
}}
{{end-eqn}}
Let $\BB = \BB_1 \cup \BB_2$.
Then $\BB$ is a basis for $T$.

Proof:
For $x \in S$, let:
:$\VV = \set {\openint s t: a < s < x < t < b} \cup \set {\openint s t: c < s < x < t < d}$
From Local Basis for Point in Union of Adjacent Open Intervals, $\VV$ is a local basis for $x$ in $T$.
Let $\openint s t \in \bigcup \VV$.
Then either:
:$\openint s t \in \BB_1$
or:
:$\openint s t \in \BB_2$
In either case:
:$\openint s t \in \BB_1 \cup \BB_2 = \BB$
Thus:
:$\bigcup \VV \subseteq \BB$
{{qed|lemma}}
Let $\openint s t \in \BB$.
Then either $\openint s t \in \BB_1$ or $\openint s t \in \BB_2$.
Thus either:
:$\exists x \in \openint a b: s < x < t$
or:
:$\exists x \in \openint c d: s < x < t$
Thus either:
:$x \in \set {\openint s t: a < s < x < t < b}$
or:
:$x \in \set {\openint s t: c < s < x < t < d}$
and so:
:$\openint s t \in \VV$
Hence it follows by definition of set union that:
:$\openint s t \in \bigcup \VV$
Thus:
:$\BB \subseteq \bigcup \VV$
{{qed|lemma}}
It follows by definition of set equality that:
:$\BB = \bigcup \VV$
From Union of Local Bases is Basis, it follows that $\BB$ is a basis for $T$.
Hence the result.
{{qed}}
Category:Union of Adjacent Open Intervals
Category:Examples of Topological Bases
cijanrvja9ryxhned5s02keace7aqpr
Theorem: Local Basis for Point on Real Number Line

Let $\struct {\R, \tau_d}$ be the real number line under the Euclidean topology.
Let $x \in \R$ be arbitrary.
Let $\BB = \set {\openint a b: a, b \in \R: a < x < b}$
Then $\BB$ is a local basis for $x$ in $\R$.

Proof:
Let $x \in \R$ be arbitrary.
{{Recall|Local Basis|local basis}}
{{:Definition:Local Basis/Local Basis for Open Sets}}
So, let $U = \openint a b$ be an arbitrary element of $\tau_d$ such that $x \in U$.
We have trivially that $\openint a b \in \BB$ by definition.
Hence $\BB$ is a local basis for $x$ in $\R$.
{{qed}}
Category:Real Number Line with Euclidean Topology
Category:Examples of Local Bases
dtl61qe0tkpos2elfh60ibsf3y5ynj8
Theorem: Preimage of Separation under Continuous Mapping is Separation

Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $f: T_1 \to T_2$ be a continuous mapping.
Let $A, B \subseteq S_2$ such that $A \mid B$.
That is, such that $A$ and $B$ separate $T_2$.
Then their preimages $f^{-1} \sqbrk A$ and $f^{-1} \sqbrk B$ form a separation of $f^{-1} \sqbrk {T_2}$.

Proof:
From Components of Separation are Clopen, we have that $A$ and $B$ are both clopen.
Hence from Clopen Set and Complement form Separation:
:$B = \relcomp {S_2} A$
and:
:$A = \relcomp {S_2} B$
From Complement of Preimage equals Preimage of Complement:
:$\relcomp {S_1} {f^{-1} \sqbrk A} = f^{-1} \sqbrk {\relcomp {S_2} A}$
and:
:$\relcomp {S_1} {f^{-1} \sqbrk B} = f^{-1} \sqbrk {\relcomp {S_2} B}$
That is:
:$\relcomp {S_1} {f^{-1} \sqbrk A} = f^{-1} \sqbrk B$
and:
:$\relcomp {S_1} {f^{-1} \sqbrk B} = f^{-1} \sqbrk A$
{{AimForCont}} $\relcomp {S_1} {f^{-1} \sqbrk A} \cap \relcomp {S_1} {f^{-1} \sqbrk B} \ne \O$.
Thus:
:$\exists x \in S_1: x \in \relcomp {S_1} {f^{-1} \sqbrk A} \land x \in \relcomp {S_1} {f^{-1} \sqbrk B}$
Then:
:$x \in \relcomp {S_1} {f^{-1} \sqbrk A} \implies \map f x \in B$
and:
:$x \in \relcomp {S_1} {f^{-1} \sqbrk B} \implies \map f x \in A$
That is:
:$\map f x \in A \cap B$
But $A$ and $B$ are disjoint by definition of separation.
From this contradiction it follows that:
:$\relcomp {S_1} {f^{-1} \sqbrk A} \cap \relcomp {S_1} {f^{-1} \sqbrk B} = \O$
That is, $\relcomp {S_1} {f^{-1} \sqbrk A}$ and $\relcomp {S_1} {f^{-1} \sqbrk B}$ form a separation of $f^{-1} \sqbrk {T_2}$.
{{qed}}
Category:Continuous Mappings (Topology)
Category:Separations
18033a8sg6y4syyw6ldfpl5m8ne67w2
Theorem: Totally Separated Space is Urysohn

Let $T = \struct {S, \tau}$ be a topological space which is totally separated.
Then $T$ is an Urysohn space.

Proof:
{{Recall|Urysohn Space|Urysohn space}}
{{:Definition:Urysohn Space}}
Let $T = \struct {S, \tau}$ be a totally separated space.
{{Recall|Totally Separated Space|totally separated space}}
{{:Definition:Totally Separated Space/Definition 1}}
Consider a mapping $f: S \to \closedint 0 1$ such that:
{{begin-eqn}}
{{eqn | l = \Img {f {\restriction_U} }
      | r = \set 0
}}
{{eqn | l = \Img {f {\restriction_V} }
      | r = \set 1
}}
{{end-eqn}}
where:
{{begin-itemize}}
{{item||$f {\restriction_U}$ and $f {\restriction_V}$ denote the restrictions of $f$ to $U$ and $V$ respectively}}
{{item||$\Img g$ denotes the image set of a mapping $g$.}}
{{end-itemize}}
From Constant Mapping is Continuous, both $f {\restriction_U}$ and $f {\restriction_V}$ are continuous on $U$ and $V$ respectively.
From Continuous Mapping of Separation, it follows that $f$ is continuous on $S$ itself.
By definition, $f$ is then an Urysohn function on $x$ and $y$.
Hence $T$ is Urysohn.
{{qed}}
Theorem: Totally Separated Space is T2.5

Let $T = \struct {S, \tau}$ be a topological space which is totally separated.
Then $T$ is a $T_{2 \frac 1 2}$ space.

Proof:
Let $T = \struct {S, \tau}$ be a totally separated space.
From Totally Separated Space is Urysohn, $T$ is an Urysohn space.
It follows from Urysohn Space is $T_{2 \frac 1 2}$ Space that $T$ is also a $T_{2 \frac 1 2}$ space.
{{qed}}
Theorem: Divisor Space is Connected

Let $T = \struct {S, \tau}$ be the divisor space.
Then $T$ is connected.

Proof:
{{ProofWanted}}
Category:Divisor Topology
Category:Examples of Connected Topological Spaces
7yu2oq8xxzyg2xr10xjotqcxws3jm7s
Theorem: Divisor Space is not T1

Let $T = \struct {S, \tau}$ be the divisor space.
Then $T$ is not a $T_1$ space.

Proof:
{{ProofWanted}}
Category:Divisor Topology
Category:Examples of T1 Spaces
dgfpuzigexqbzwdoctmtbclbo7axl1r
Theorem: Divisor Space is Scattered

Let $T = \struct {S, \tau}$ be the divisor space.
Then $T$ is a scattered space.

Proof:
{{ProofWanted}}
Category:Divisor Topology
Category:Examples of Scattered Spaces
ifwqtjd2azeup6wtpg4iswwt3ce63vi
Theorem: Power Series Expansion for Sinc Function

{{begin-eqn}}
{{eqn | l = \map \sinc x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } { \paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = 1 - \dfrac {x^2} { 3!} + \dfrac {x^4} { 5!} - \dfrac {x^6} { 7!} + \cdots 
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \sinc x
      | r = \frac {\map \sin x} x
      | c = {{Defof|Sinc Function}}
}}
{{eqn | r = \frac 1 x \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = Power Series Expansion for Sine Function
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n + 1}!}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Sinc Function
Category:Examples of Power Series
7qay43e5npupzb42o6rs2k6ucwsz9ce
Theorem: Derivative of Sinc Function

:$\dfrac \d {\d x} \paren {\map \sinc x} = \dfrac {x \cos x - \sin x} {x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\dfrac {\sin x} x}
      | r = \dfrac {x \map {\frac \d {\d x} } {\sin x} - \sin x \map {\frac \d {\d x} } x} {x^2}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \dfrac {x \cdot \cos x - \sin x \cdot 1} {x^2}
      | c = Derivative of Sine Function, Power Rule for Derivatives
}}
{{eqn | r = \dfrac {x \cos x - \sin x} {x^2}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Category:Sinc Function
Category:Derivatives
hzcckj9srf6zl1f51k03pn8ssassxbd
Theorem: Primitive of Sinc Function

:$\ds \int_{t \mathop \to 0}^{t \mathop = x} \frac {\sin t} t \rd t = \map \Si x $

Proof:
True by {{Defof|Sine Integral Function}}.
{{qed}}
Category:Primitives involving Sine Function
Category:Sinc Function
Category:Sine Integral Function
nf0hi6a81xxsm3k9z75bmyrtky7esxu
Theorem: Magnetic Force on Conductor carrying Steady Current

Let $s$ be a wire carrying a steady electric current $I$.
Let $\d \mathbf l$ be an infinitesimal length of the wire that points in the direction of the current.
Let $\mathbf B$ be the magnetic field acting at $\d \mathbf l$.
Then, the force $\d \mathbf F$ acting on $\d \mathbf l$ is
:$\d \mathbf F = I \d \mathbf l \times \mathbf B$
where $\times$ is the vector cross product.

Proof:
According to Magnetic Force on Moving Charged Particle, a single particle with charge $q$  moving with velocity $\mathbf v$ in a magnetic field $\mathbf B$ experiences a force of:
:$\mathbf F = q \mathbf v \times \mathbf B$
For a current in a wire, we will consider an infinitesimal amount of charge $\d q$ feeling an infinitesimal amount of force $\d \mathbf F$:
:$\d \mathbf F = \d q \, \mathbf v \times \mathbf B$
Let the linear density of moving charges in the wire be $\lambda$.
Then, the amount of charge in a length of wire $\d l = \size {\d \mathbf l}$ is:
:$\d q = \lambda \d l$
If the charges take a time $\d t$ to cross $\d l$, then their speed $v = \size {\mathbf v}$ is:
{{begin-eqn}}
{{eqn | l = v
      | r = \frac {\d l} {\d t}
      | c = {{Defof|Speed}}
}}
{{eqn | r = \frac 1 \lambda \frac {\d q} {\d t}
}}
{{eqn | r = \frac 1 \lambda I
      | c = {{Defof|Electric Current}}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \d q \, v
      | r = \paren {\lambda \d l} \paren {\frac 1 \lambda I}
}}
{{eqn | r = I \d l
}}
{{end-eqn}}
Multiplying both sides by a unit vector in the direction of $I$ results in:
:$\d q \, \mathbf v = I \d \mathbf l$
Thus:
{{begin-eqn}}
{{eqn | l = \d \mathbf F
      | r = \d q \, \mathbf v \times \mathbf B
}}
{{eqn | r = I \d \mathbf l \times \mathbf B
}}
{{end-eqn}}
{{qed}}
Category:Electromagnetism
Category:Magnetic Forces
Category:Electric Current
5181r7pm86c4brn845n2qwrolcbfjic
Theorem: Topology Induced by Metric is Unique

Let $M = \struct {A, d}$ be a metric space.
Let $T = \struct {A, \tau_d}$ be the topological space such that $\tau_d$ is the topology induced by $d$.
Then $\tau_d$ is unique.
That is, if $\tau_{d 1}$ and $\tau_{d 2}$ are both induced by $d$, then $\tau_{d 1} = \tau_{d 2}$.

Proof:
{{Recall|Topology Induced by Metric|topology induced by $d$}}
{{:Definition:Topology Induced by Metric/Definition 1}}
There is only one set of open sets of $M$.
Hence by definition there is only one set of open sets of $T$.
But by definition of topology, $\tau_d$ ''is'' the set of open sets of $T$.
The result follows.
{{qed}}
Theorem: Metric inducing Topology is not Unique

Let $T = \struct {A, \tau}$ be a topological space such that its topology $\tau$ is induced by a metric on $A$.
Then that metric is specifically ''not'' unique.
In other words, given that $\tau$ is the induced by a metric $d_1$ on $A$, there exists another metric $d_2$ on $A$ such that $d_2$ also induces topology $\tau$.

Proof:
A direct consequence of:
:Construction of Infinite Set of Metrics yielding Same Metric Space
:Metric Induces Topology
{{qed}}
Theorem: Construction of Infinite Set of Metrics yielding Same Metric Space

Let $M = \struct {A, d}$ be a metric space.
Let $\SS$ denote the set of open sets of $M$.
Then there exists an infinite set of metrics on $A$ such that the set of open sets of the resulting metric space is also $\SS$.
That is, given a metric space, there is an infinite number of metrics which yield that same metric space.

Proof:
;Outline of Proof
Let $M = \struct {A, d}$ be a metric space.
Let $\delta: A \to A$ be defined as:
:$\forall \tuple {x, y} \in A^2: \map \delta {x, y} := \dfrac {\map d {x, y} } {1 + \map d {x, y} }$
It is to be shown that $\delta$ is a metric on $A$.
Then it is to be shown that the open sets of $\struct {A, \delta}$ are the same sets as the open sets of $\struct {A, d}$.
{{finish|the above; use lemmata}}
Thus, from a given metric, a new metric can be defined different from the old metric yielding the same metric space.
From that metric $\delta$, another metric can be defined in the same way from $\delta$ as $\delta$ was from $d$.
This can be continued indefinitely.
{{qed}}
Theorem: Countably Compact Metric Space is Separable

Let $M$ be a countably compact metric space.
Then $M$ is separable.

Proof:
This follows directly from the results:
:Countably Compact Metric Space is Sequentially Compact
:Sequentially Compact Metric Space is Separable.
{{qed}}
Theorem: Countably Compact Metric Space is Second-Countable

Let $M$ be a countably compact metric space.
Then $M$ is second-countable.

Proof:
This follows directly from the results:
:Countably Compact Metric Space is Separable
:Separable Metric Space is Second-Countable.
{{qed}}
Theorem: Countably Compact Second-Countable Space is Compact

Let $T = \struct {S, \tau}$ be a countably compact second-countable space.
Then $T$ is compact.

Proof:
{{Recall|Compact Topological Space|compact topological space}}
{{:Definition:Compact Topological Space/Definition 1}}
Let $T$ be countably compact and second-countable.
{{Recall|Countably Compact Space|countably compact space}}
{{:Definition:Countably Compact Space/Definition 1}}
{{Recall|Second-Countable Space|second-countable space}}
{{:Definition:Second-Countable Space}}
Since $T$ is second-countable, we can choose a countable (analytic) basis $\BB$ for $\tau$.
Let $\CC$ be an open cover for $S$.
Define:
:$\CC' = \set {B \in \BB: \exists C \in \CC: B \subseteq C}$
Then $\CC' \subseteq \BB$, and so $\CC'$ is countable.
By the definition of an analytic basis, we have $\BB \subseteq \tau$; since $\subseteq$ is a transitive relation, it therefore follows that $\CC' \subseteq \tau$.
From Equivalence of Definitions of Analytic Basis:
:$\forall C \in \CC: \forall x \in C: \exists B \in \CC': x \in B$
That is, by the definition of set union:
:$\ds \forall C \in \CC: C \subseteq \bigcup \CC'$
Hence, by Union is Smallest Superset:
:$\ds S \subseteq \bigcup \CC \subseteq \bigcup \CC'$
Since $\subseteq$ is a transitive relation, it follows that $\CC'$ is an open cover for $S$.
Since $T$ is countably compact, there exists a finite subcover $\FF$ of $\CC'$ for $S$.
By the Principle of Finite Choice, there exists an indexed family $\family {C_B}_{B \mathop \in \FF}$ such that:
:$\forall B \in \FF: B \subseteq C_B \in \CC$
Note that $\set {C_B: B \in \FF}$ is a finite subcover of $\CC$ for $X$.
Hence, $T$ is compact.
{{qed}}