Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001
Association of Mizar Users
Some Properties of Dyadic Numbers and Intervals

Jozef Bialas

Lodz University

Yatsuka Nakamura

Shinshu University, Nagano
Summary.

The article is the second part of a paper proving
the fundamental Urysohn Theorem concerning the
existence of a real valued continuous function on
a normal topological space.
The paper is divided into two parts. In the first
part, we introduce some definitions and theorems
concerning properties of intervals; in the second we
prove some of properties of dyadic numbers used in
proving Urysohn Lemma.
The terminology and notation used in this paper have been
introduced in the following articles
[11]
[13]
[1]
[8]
[12]
[9]
[2]
[3]
[4]
[5]
[6]
[10]
[7]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Jozef Bialas.
Infimum and supremum of the set of real numbers. Measure theory.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Jozef Bialas.
Series of positive real numbers. Measure theory.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Jozef Bialas.
Properties of the intervals of real numbers.
Journal of Formalized Mathematics,
5, 1993.
 [5]
Jozef Bialas.
Some properties of the intervals.
Journal of Formalized Mathematics,
6, 1994.
 [6]
Jozef Bialas and Yatsuka Nakamura.
Dyadic numbers and T$_4$ topological spaces.
Journal of Formalized Mathematics,
7, 1995.
 [7]
Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.
Scalar multiple of Riemann definite integral.
Journal of Formalized Mathematics,
11, 1999.
 [8]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Rafal Kwiatek.
Factorial and Newton coefficients.
Journal of Formalized Mathematics,
2, 1990.
 [10]
Jan Popiolek.
Some properties of functions modul and signum.
Journal of Formalized Mathematics,
1, 1989.
 [11]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [12]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [13]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received February 16, 2001
[
Download a postscript version,
MML identifier index,
Mizar home page]