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

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.