FORMALIZED MATHEMATICS

Vol. 24, No. 3, Pages 167–172, 2016

DOI: 10.1515/forma-2016-0013 degruyter.com/view/j/forma

Compactness in Metric Spaces

Kazuhisa Nakasho Keiko Narita Yasunari Shidama

Shinshu University Hirosaki-city Shinshu University
Nagano, Japan Aomori, Japan Nagano, Japan

Summary. In this article, we mainly formalize in Mizar [2] the equiva-

lence among a few compactness definitions of metric spaces, norm spaces, and
the real line. In the first section, we formalized general topological properties of
metric spaces. We discussed openness and closedness of subsets in metric spaces
in terms of convergence of element sequences. In the second section, we firstly
formalize the definition of sequentially compact, and then discuss the equivalen-
ce of compactness, countable compactness, sequential compactness, and totally
boundedness with completeness in metric spaces.
In the third section, we discuss compactness in norm spaces. We formalize
the equivalence of compactness and sequential compactness in norm space. In
the fourth section, we formalize topological properties of the real line in terms
of convergence of real number sequences. In the last section, we formalize the
equivalence of compactness and sequential compactness in the real line. These
formalizations are based on [20], [5], [17], [14], and [4].

MSC: 46B50 54E45 03B35

Keywords: metric spaces; normed linear spaces; compactness
MML identifier: TOPMETR4, version: 8.1.05 5.37.1275

1. Topological Properties of Metric Spaces

Now we state the propositions:

(1) Let us consider a non empty set M , and a sequence x of M . Suppose
rng x is finite. Then there exists an element z of M such that
(i) x−1 ({z}) ⊆ N, and
(ii) x−1 ({z}) is infinite.
c 2016 University of Białystok
CC-BY-SA License ver. 3.0 or later
167 ISSN 1426–2630(Print), 1898-9934(Online)

Brought to you by | ReadCube/Labtiva

Authenticated
Download Date | 2/15/17 11:01 AM
168 kazuhisa nakasho, keiko narita, and yasunari shidama

Proof: Define X (object) = x−1 ({$1 }). Set K = {X (w), where w is

an element of M : w ∈ rng x}. K is finite from [18, Sch. 21]. For eve-
ry set Y such that Y ∈ K holds Y is finite. dom x ⊆ K by [6, (3)].
S


(2) Let us consider a subset X of N. Suppose X is infinite. Then there exists
an increasing sequence N of N such that rng N ⊆ X.
Proof: Reconsider B = 2X as a non empty set. Reconsider N0 = min∗ X
as an element of N. Reconsider Y0 = X as an element of B. Define
P[object, object, set, object, set] ≡ $5 = $3 \ {$2 } and $4 = min∗ $5 . For
every natural number n and for every element x of N and for every ele-
ment y of B, there exists an element x1 of N and there exists an element y1
of B such that P[n, x, y, x1 , y1 ]. Consider N being a sequence of N, Y being
a sequence of B such that N (0) = N0 and Y (0) = Y0 and for every natural
number n, P[n, N (n), Y (n), N (n + 1), Y (n + 1)] from [13, Sch. 3]. Define
Q[natural number] ≡ N ($1 ) = min∗ (Y ($1 )) and N ($1 ) ∈ Y ($1 ) and Y ($1 )
is infinite and Y ($1 ) ⊆ N. For every natural number i such that Q[i] holds
Q[i + 1] by [8, (31)]. For every natural number i, Q[i] from [1, Sch. 2].
rng N ⊆ X by [7, (11)]. For every natural number i, N (i) < N (i + 1). 
(3) Let us consider a non empty metric space M , and a subset V of Mtop .
Suppose V is open. Then there exists a family F of subsets of M such
that
(i) F = {Ball(x, r), where x is an element of M, r is a real number : r >
0 and Ball(x, r) ⊆ V }, and
S
(ii) V = F.
Proof: Set F = {Ball(x, r), where x is an element of M, r is a real num-
ber: r > 0 and Ball(x, r) ⊆ V }. For every object z such that z ∈ F holds
z ∈ the open set family of M by [3, (29)]. Reconsider Q = F as a subset
S

of Mtop . For every object z, z ∈ V iff z ∈ Q by [9, (15)], [12, (1), (11)]. 
(4) Let us consider a non empty metric space M , a subset X of Mtop , and
an element p of M . Then p ∈ X if and only if for every real number r such
that 0 < r holds X meets Ball(p, r).
(5) Let us consider a non empty metric space M , a subset X of Mtop , and
an object x. Then x ∈ X if and only if there exists a sequence S of M
such that for every natural number n, S(n) ∈ X and S is convergent and
lim S = x.
(6) Let us consider a non empty metric space M , and a subset X of Mtop .
Then X is closed if and only if for every sequence S of M such that for
every natural number n, S(n) ∈ X and S is convergent holds lim S ∈ X.
The theorem is a consequence of (5).

Brought to you by | ReadCube/Labtiva

Authenticated
Download Date | 2/15/17 11:01 AM
 Compactness in metric spaces 169

(7) Let us consider non empty metric spaces X, Y, and a function f from
Xtop into Ytop . Then f is continuous if and only if for every sequence S of
X and for every sequence T of Y such that S is convergent and T = f · S
holds T is convergent and lim T = f (lim S).
Proof: For every subset B of Ytop such that B is closed holds f −1 (B) is
closed by [7, (15)], (6). 

2. Compactness in Metric Spaces

Let M be a non empty metric space and X be a subset of M . We say that

X is sequentially compact if and only if
(Def. 1) for every sequence S1 of M such that rng S1 ⊆ X there exists a sequence
S2 of M such that there exists an increasing sequence N of N such that
S2 = S1 · N and S2 is convergent and lim S2 ∈ X.
Let us observe that every subset of M which is empty is also sequentially
compact.
We say that M is sequentially compact if and only if
(Def. 2) ΩM is sequentially compact.
Now we state the proposition:
(8) Let us consider a non empty metric space M , a subset X of M , a subset
Y of Mtop , an element x of M , and an element y of Mtop . Suppose X = Y
and x = y. Then y is an accumulation point of Y if and only if for every
real number r such that 0 < r holds Ball(x, r) meets X \ {x}.
Let us consider a non empty metric space M . Now we state the propositions:
(9) If Mtop is countably-compact, then M is sequentially compact.
Proof: For every subset X of M such that X is infinite there exists
an element x of M such that for every real number r such that 0 < r
holds Ball(x, r) meets X \ {x} by [16, (28)], [11, (16)], (8). For every
sequence x of M such that rng x ⊆ ΩM there exists a sequence x1 of M
such that there exists an increasing sequence N of N such that x1 = x · N
and x1 is convergent and lim x1 ∈ ΩM by (1), (2), [7, (4), (38), (15)]. 
(10) If M is sequentially compact, then Mtop is countably-compact.
Proof: For every subset X of M such that X is infinite there exists
an element x of M such that for every real number r such that 0 < r
holds Ball(x, r) meets X \ {x} by [15, (3)], [7, (2)], [19, (26)], [7, (112)].
For every subset A of Mtop such that A is infinite holds Der A is not empty
by (8), [11, (16)]. 
(11) Mtop is compact if and only if M is sequentially compact. The theorem
is a consequence of (9).

Brought to you by | ReadCube/Labtiva

Authenticated
Download Date | 2/15/17 11:01 AM
170 kazuhisa nakasho, keiko narita, and yasunari shidama

(12) M is totally bounded and complete if and only if M is sequentially

compact. The theorem is a consequence of (11).
Let us consider a non empty metric space M and a non empty subset S of
M . Now we state the propositions:
(13) S is sequentially compact if and only if M S is sequentially compact.
Proof: For every sequence S1 of M such that rng S1 ⊆ S there exists
a sequence S2 of M such that there exists an increasing sequence N of N
such that S2 = S1 · N and S2 is convergent and lim S2 ∈ S by [7, (6)]. 
(14) S is sequentially compact if and only if M S is compact. The theorem
is a consequence of (11) and (13).
(15) Let us consider a non empty metric space M , a subset S of M , and
a subset T of Mtop . If T = S, then T is compact iff S is sequentially
compact. The theorem is a consequence of (11) and (13).
(16) Let us consider a non empty metric space M , a non empty subset S of
M , and a non empty subset T of Mtop . Suppose T = S. Then Mtop T is
countably-compact if and only if S is sequentially compact. The theorem
is a consequence of (11) and (13).
(17) Let us consider a non empty metric space M , and a non empty subset
S of M . Then M S is totally bounded and complete if and only if S is
sequentially compact. The theorem is a consequence of (12) and (13).

3. Compactness in Norm Spaces

Now we state the propositions:

(18) Let us consider a real normed space N , a subset S of N , and a subset T
of MetricSpaceNorm N . If S = T , then S is compact iff T is sequentially
compact.
(19) Let us consider a real normed space N , a subset S of N , and a subset T
of TopSpaceNorm N . If S = T , then S is compact iff T is compact. The
theorem is a consequence of (15) and (18).

4. Topological Properties of the Real Line

Let us consider a sequence S1 of the metric space of real numbers, a sequence

s of real numbers, a real number g, and an element g1 of the metric space of
real numbers. Now we state the propositions:
(20) Suppose S1 = s and g = g1 . Then for every real number p such that
0 < p there exists a natural number n such that for every natural number

Brought to you by | ReadCube/Labtiva

Authenticated
Download Date | 2/15/17 11:01 AM
 Compactness in metric spaces 171

m such that n ¬ m holds |s(m) − g| < p if and only if for every real
number p such that 0 < p there exists a natural number n such that for
every natural number m such that n ¬ m holds ρ(S1 (m), g1 ) < p.
Proof: For every real number p such that 0 < p there exists a natural
number n such that for every natural number m such that n ¬ m holds
|s(m) − g| < p by [9, (11)]. 
(21) If S1 = s and g = g1 , then s is convergent and lim s = g iff S1 is
convergent and lim S1 = g1 . The theorem is a consequence of (20).
(22) Let us consider a sequence S1 of the metric space of real numbers, and
a sequence s of real numbers. Suppose S1 = s and s is convergent. Then
(i) S1 is convergent, and
(ii) lim S1 = lim s.
The theorem is a consequence of (20).

5. Compactness in the Real Line

Now we state the propositions:

(23) Let us consider a subset N of R, and a subset M of R1 . Suppose N = M .
Then for every family F of subsets of R such that F is a cover of N and for
every subset P of R such that P ∈ F holds P is open there exists a family
G of subsets of R such that G ⊆ F and G is cover of N and finite if and
only if for every family F1 of subsets of R1 such that F1 is cover of M and
open there exists a family G1 of subsets of R1 such that G1 ⊆ F1 and G1
is cover of M and finite.
Proof: Reconsider F1 = F as a family of subsets of R1 . For every subset
P1 of R1 such that P1 ∈ F1 holds P1 is open by [10, (39)]. Consider G1
being a family of subsets of R1 such that G1 ⊆ F1 and G1 is cover of M
and finite. 
(24) Let us consider a subset N of R. Then N is compact if and only if for
every family F of subsets of R such that F is a cover of N and for every
subset P of R such that P ∈ F holds P is open there exists a family G of
subsets of R such that G ⊆ F and G is cover of N and finite. The theorem
is a consequence of (23).

Brought to you by | ReadCube/Labtiva

Authenticated
Download Date | 2/15/17 11:01 AM
172 kazuhisa nakasho, keiko narita, and yasunari shidama

References
[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathe-
matics, 1(1):41–46, 1990.
[2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Ma-
tuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and
beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Vol-
ker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in
Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-
319-20614-1. doi:10.1007/978-3-319-20615-8 17.
[3] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481–
485, 1991.
[4] Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media,
2013.
[5] Nicolas Bourbaki, H.G. Eggleston, and S. Madan. Elements of mathematics: Topological
vector spaces. Springer-Verlag, 1987.
[6] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):
55–65, 1990.
[7] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164,
1990.
[8] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53,
1990.
[9] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces – funda-
mental concepts. Formalized Mathematics, 2(4):605–608, 1991.
[10] Adam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3):
313–322, 2003.
[11] Adam Grabowski. On the boundary and derivative of a set. Formalized Mathematics, 13
(1):139–146, 2005.
[12] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathe-
matics, 1(3):607–610, 1990.
[13] Artur Korniłowicz. Recursive definitions. Part II. Formalized Mathematics, 12(2):167–
172, 2004.
[14] Erwin Kreyszig. Introductory Functional Analysis with Applications. Wiley, 1 edition,
1989.
[15] Gilbert Lee and Piotr Rudnicki. Dickson’s lemma. Formalized Mathematics, 10(1):29–37,
2002.
[16] Karol Pąk. Complete spaces. Formalized Mathematics, 16(1):35–43, 2008.
doi:10.2478/v10037-008-0006-2.
[17] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
[18] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1
(3):495–500, 1990.
[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1
(1):73–83, 1990.
[20] Kosaku Yoshida. Functional Analysis. Springer, 1980.

Received June 30, 2016

Brought to you by | ReadCube/Labtiva

Authenticated
Download Date | 2/15/17 11:01 AM