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]