Dyadic Numbers and T$_4$ Topological Spaces

Jozef Bialas

Lodz \ University, Lodz

Yatsuka Nakamura

Shinshu University, Nagano

Summary.

This article is the first part of a paper proving the fundamental Urysohn's Theorem concerning the existence of a real valued continuous function on a normal topological space. The paper is divided into four parts. In the first part, we prove some auxiliary theorems concerning properties of natural numbers and prove two useful schemes about recurrently defined functions; in the second part, we define a special set of rational numbers, which we call dyadic, and prove some of its properties. The next part of the paper contains the definitions of T${}_1$ space and normal space, and we prove related theorems used in later parts of the paper. The final part of this work is developed for proving the theorem about the existence of some special family of subsets of a topological space. This theorem is essential in proving Urysohn's Lemma.

MML Identifier: URYSOHN1

Contents (PDF format)

1. Dyadic Numbers
2. Normal Spaces
3. Some Increasing Family of Sets in Normal Space

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. Countable sets and Hessenberg's theorem. Journal of Formalized Mathematics, 2, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[7] Agata Darmochwal. Compact spaces. Journal of Formalized Mathematics, 1, 1989.

[8] Agata Darmochwal and Yatsuka Nakamura. Metric spaces as topological spaces --- fundamental concepts. Journal of Formalized Mathematics, 3, 1991.

[9] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[10] Beata Padlewska. Locally connected spaces. Journal of Formalized Mathematics, 2, 1990.

[11] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.

[12] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[14] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.