Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
Formal Topological Spaces

Gang Liu

Tokyo University of Mercantile Marine

Yasushi Fuwa

Shinshu University, Nagano

Masayoshi Eguchi

Tokyo University of Mercantile Marine
Summary.

This article is divided into two parts. In the first part,
we prove some useful theorems on finite topological spaces. In the
second part, in order to consider a family of neighborhoods to a point
in a space, we extend the notion of finite topological
space and define a new topological space, which we call formal
topological space. We show the relation between formal
topological space struct ({\tt FMT\_Space\_Str}) and the {\tt TopStruct} by giving
a function ({\tt NeighSp}). And the following notions are
introduced in formal topological spaces: boundary, closure, interior,
isolated point, connected point, open set and close set,
then some basic facts concerning them are proved. We will discuss the
relation between the formal topological space and the
finite topological space in future work.
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[3]
[7]
[1]
[2]
[4]
[5]
[8]

Some Useful Theorems on Finite Topological Spaces

Formal Topological Spaces
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]
Hiroshi Imura and Masayoshi Eguchi.
Finite topological spaces.
Journal of Formalized Mathematics,
4, 1992.
 [5]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Edmund Woronowicz.
Manyargument relations.
Journal of Formalized Mathematics,
2, 1990.
Received October 13, 2000
[
Download a postscript version,
MML identifier index,
Mizar home page]