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

Families of Subsets, Subspaces and Mappings in Topological Spaces


Agata Darmochwal
Warsaw University, Bialystok

Summary.

This article is a continuation of [11]. Some basic theorems about families of sets in a topological space have been proved. Following redefinitions have been made: singleton of a set as a family in the topological space and results of boolean operations on families as a family of the topological space. Notion of a family of complements of sets and a closed (open) family have been also introduced. Next some theorems refer to subspaces in a topological space: some facts about types in a subspace, theorems about open and closed sets and families in a subspace. A notion of restriction of a family has been also introduced and basic properties of this notion have been proved. The last part of the article is about mappings. There are proved necessary and sufficient conditions for a mapping to be continuous. A notion of homeomorphism has been defined next. Theorems about homeomorphisms of topological spaces have been also proved.

MML Identifier: TOPS_2

The terminology and notation used in this paper have been introduced in the following articles [8] [4] [9] [10] [2] [3] [1] [5] [6] [7]

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Some basic properties of sets. 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.
[11] Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.

Received June 21, 1989


[ Download a postscript version, MML identifier index, Mizar home page]