Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Compact Spaces

Agata Darmochwal

Warsaw University, Bialystok
Summary.

The article contains definition of a compact space and some theorems about
compact spaces. The notions of a cover of a set and a centered family are
defined in the article to be used in these theorems. A set is compact in
the topological space if and only if every open cover of the set has a finite
subcover. This definition is equivalent, what has been shown next, to
the following definition: a set is compact if and only if a subspace generated
by that set is compact. Some theorems about mappings
and homeomorphisms of compact spaces have been also proved.
The following schemes used in proofs of theorems have
been proved in the article:
FuncExChoice  the scheme of choice of a function,
BiFuncEx  the scheme of parallel choice of two functions
and the theorem about choice of a finite counter image of a finite image.
The terminology and notation used in this paper have been
introduced in the following articles
[8]
[3]
[9]
[10]
[1]
[2]
[6]
[5]
[7]
[4]
Contents (PDF format)
Bibliography
 [1]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Agata Darmochwal.
Families of subsets, subspaces and mappings in topological spaces.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Agata Darmochwal.
Finite sets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Beata Padlewska.
Families of sets.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [9]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received September 19, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]