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.

MML Identifier: COMPTS_1

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.