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.

#### MML Identifier: FINTOPO2

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

#### Contents (PDF format)

1. Some Useful Theorems on Finite Topological Spaces
2. 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. Many-argument relations. Journal of Formalized Mathematics, 2, 1990.