Mechanized Mathematics and Its Applications, Vol. 6, No. 1, November 2007, 23:31

The Urysohn Lemma

Józef Białas^{†} Yatsuka Nakamura^{††}

†University of Łódź Department of Mathematics and Informatics Banacha 22 90-238 Łódź, Poland

bialas@math.uni.lodz.pl

††Shinshu University, Faculty of Engineering Department of Information Engineering Nagano-ken Nagano-shi Wakasato 4-17-1 Japan

ynakamur@cs.shinshu-u.ac.jp

Abstract – In this paper we introduce a way of formalizing the Urysohn lemma in the Mizar system. The essential steps for outlining a formal proof of this theorem are described. The idea for a proof of Urysohn’s lemma is also generated.

1. Introduction

In his beautiful monograph ([3]) concerning functional analysis and its applications, Kôsaku Yoshida has introduced one of the fundamental theorems of mathematical analysis, Urysohn’s lemma. This theorem is equipped with a proof which is highly intuitive, clear, and consistent. The construction of functions which satisfy the thesis of Urysohn’s theorem there is also introduced. In formalizing this theorem in Mizar, we decided to preserve exactly the same scheme of the proof. For the purpose of clarifying the considerations, let us describe the expression of Urysohn’s lemma, without a detailed explanation of notions, by using a standard terminology from topology and mathematical analysis.

Urysohn’s lemma 1 . For a normal topological space X and A,B closed subsets of X which are disjoint there exists a continuous function F : X −→ R that satisfies the inequality

0 ≤ F (x) ≤ 1 for x ∈ X, such that F (x) = 0 for x ∈ A and F (x) = 1 for x ∈ B.

The proof of the above theorem in [3] is correct under the assumption A ≠ ∅. The thesis of the theorem is developed without this assumption because the case A = ∅ is easy to prove so we think the assumption A ≠ ∅ was accepted naturally. However, the above will have a consequence during formalization. We pointed that out in an appropriate place in our investigation. An analytical proof of Urysohn’s lemma may have the following form: in the first step, we construct a function F : X −→ R which is a candidate to satisfy the thesis and next we substantiate if F in reality satisfies the thesis of the theorem. This universal form of the proof will be preserved during our formal proof of the Urysohn lemma in the Mizar system.

Manuscript received August 16, 2007; revised October 30, 2007.

2. Description of the Method of Formalization of Urysohn’s Lemma

The formal proof of Urysohn’s lemma is contained in MML in three files: URYSOHN1.miz ([5]), URYSOHN2.miz ([6]) and URYSOHN3.miz ([7]). The first of them titled “Dyadic Numbers and T_{4} Topological Spaces” was developed to make it possible to preserve the form of the proof of Urysohn’s lemma from Yoshida’s monograph. The file includes a definition of dyadic numbers and some theorems about their properties. There are also definitions of topological spaces T_{1} and T_{4} and a proof of a theorem about the existence of some special family of subsets of T_{4} topological space, which are essential in proving Urysohn’s lemma. The second file titled “Some Properties of Dyadic Numbers and Intervals” describes definitions and theorems which concern the properties of intervals and dyadic numbers. The third file is the proper solving of the formalization of Urysohn’s lemma. Here we describe the construction of the function that solves the thesis of the Urysohn’s lemma and we introduce a formal proof of the Urysohn’s lemma in normal (T_{4}) space and a proof of a theorem for compact space.

2.1 The Topic in URYSOHN1.miz

Let R, R_{<0} , R_{>1} denote the sets of real numbers, negative real numbers, and real numbers larger than 1, respectively.

Definition 1. 1 . Let n be a natural number. The functor dyadic(n) yields a subset of R such that for every x ∈ R holds x ∈ dyadic(n) iff there exists a natural number i such that

0 ≤ x and x ≤ 2^{n} and x = \frac{i}{2^{n}}.  (2..1)

The set DYADIC ⊂ R is defined by

Definition 1. 2 . For every x ∈ R holds x ∈ DYADIC iff there exists a natural number n such that

x ∈ dyadic(n) .  (2..2)

The equation

DOM = R_{<0} ∪ DYADIC ∪ R_{>1}  (2..3)

defines the subset of R important in future investigations. From (2..1), (2..2), and(2..3) let us note that DOM , DYADIC and for every natural n dyadic(n) are nonempty subsets of real numbers. For writers unused to formalized substantiation mathematical theories, the above may seem trivial and superfluous, but in the process of formalization theories such corroboration is indispensable.

One can prove the following properties

Property 1. 1 . For every natural number n and for every x ∈ R holds

x ∈ dyadic(n) implies 0 ≤ x and x ≤ 1,  (2..4)

dyadic(0) = { 0 , 1},  (2..5)
dyadic(1) = \{ 0 , \frac{1}{2} , 1\},  (2..6)
dyadic(n) ⊆ dyadic(n + 1),  (2..7)
0 ∈ dyadic(n) and 1 ∈ dyadic(n).  (2..8)

Property 1. 2 . For every natural number n, for every x ∈ R, and for every natural number i such that 0 ≤ i and i ≤ 2^{n} holds

\frac{2i − 1}{2^{n+1}} ∈ dyadic(n + 1) \ dyadic(n),  (2..9)
\frac{2i + 1}{2^{n+1}} ∈ dyadic(n + 1) \ dyadic(n),  (2..10)
\frac{1}{2^{n+1}} ∈ dyadic(n + 1) \ dyadic(n).  (2..11)

We now define the functor axis which yields a natural number by

Definition 1. 3 . Let n be natural number and let x be an element of dyadic(n). By axis(x,n) we denote a natural number satisfying the equality

x = \frac{axis(x,n)}{2^{n}}.  (2..12)

It is easy to see by (2..1) and (2..12) the property

Property 1. 3 . For every natural number n and for every x ∈ dyadic(n) holds

0 ≤ axis(x,n) and axis(x,n) ≤ 2^{n},  (2..13)
\frac{axis(x,n) − 1}{2^{n}} ≤ x and x ≤ \frac{axis(x,n) + 1}{2^{n}}.  (2..14)

From (2..9), (2..10), (2..11), and (2..13) we obtain the following two properties:

Property 1. 4 . For natural number n and x, x_{1}, x_{2} ∈ dyadic(n + 1) holds x ∉ dyadic(n) and x_{1} ≤ x_{2} and x_{1} ∉ dyadic(n) and x_{2} ∉ dyadic(n) implies

\frac{axis(x,n+1)−1}{2^{n+1}} ∈ dyadic(n) and \frac{axis(x,n+1)+1}{2^{n+1}} ∈ dyadic(n) and

\frac{axis(x_{1},n+1)+1}{2^{n+1}} ≤ \frac{axis(x_{2},n+1)−1}{2^{n+1}} .

Property 1. 5 . For natural number n and x_{1},x_{2} ∈ dyadic(n)holds x_{1} ≤ x_{2} implies x_{1} ≤ \frac{axis(x_{2},n)−1}{2^{n}} and \frac{axis(x_{1},n)+1}{2^{n}} ≤ x_{2} and

axis(x_{1},n) ≤ axis(x_{2},n).

Let T be a topological space and x be a point of it. A neighbourhood of x, open and closed subsets of T, and other definitions such as T_{1},T_{2},T_{3},T_{4} spaces are understood to be in standard terminology from topology.

The following two theorems are true:

Theorem 1 .Let T be a topological space. Suppose T is a T_{4} space. Let A,B be open subsets of T such that A ≠ ∅ and \overline{A}⊂ B . Then there exists an open subset C of T such that C ≠ ∅ and \overline{A}⊂ C and \overline{C}⊂ B.

Theorem 2 .Let T be a topological space. Suppose T is a T_{4} space. Let A,B be closed subsets of T such that A ≠ ∅ and A ∩ B = ∅ . Let n be a natural number and let G be a function from dyadic(n) into bool T. Suppose that for all elements r_{1},r_{2} of dyadic(n) such that n_{1} ≤ n_{2} holds G(r_{1}) is open and G(r_{2}) is open and \overline{G(r_{1})}⊂ G(r_{2}) and A ⊂ G(0) and G(1) = T \ B . Then there exists a function F from dyadic(n+1) into bool T such that for all elements r of dyadic(n+1) F(r) is open and for all elements r_{1},r_{2} of dyadic(n+1) if r_{1} ≤ r_{2}

then \overline{F (r_{1})}⊂ F (r_{2}) and A ⊂ F (0) and F (1) = T \B and if r ∈ dyadic(n) then F (r) = G(r) .

The above theorem will be useful later in the article.

2.2 Most Important Elements of URYSOHN2.miz

This file includes some additional properties of intervals defined in [9] and here we present some of most important of them. One is the property: the DYADIC is dense in interval [0,1].

Property 2. 1 . For all real numbers a,b such that a < b there exists a real number c such

that c ∈ DYADIC and a < c and c < b .

The dual property takes place for the set DOM .

Property 2. 2 . For all real numbers such that a < b there exists a real number c such that

c ∈ DOM and a < c and c < b .

From the property

Property 2. 3 . For every real number eps > 0 there exists a natural number n such that

1 < 2^{n}· eps.

it follows that for eps > 0 there exists a dyadic number \frac{1}{2^{n}} lower than eps.

Most of the definitions and properties in this section fulfill a task to be completed for [9] and [10]. They are natural and are described for the purpose of making it possible to use theorems from other MML papers.

2.3 The Essentials in URYSOHN3.miz for the Formalization of Urysohn’s Lemma

This file is essential for accomplishing our aim of formalizing Urysohn’s lemma. We begin with a kind of apology for the fact that in the sequel we will be discussing things seriously in a bit of a facetious form. During the construction of the formal proof of Urysohn’s lemma, the first author stayed at Shinshu University in Nagano. It was the time of a burdensome (for European people) - but very beautiful, rainy season. Some of the names used in the definitions of special functors in the article were inspired by real happenings observed in that time.

The notation and terminology introduced below will be used in the sequel without any futher references. In the end we change them, but they will be explicit marked.

Let T be a non empty T_{4} topological space and let A,B be a closed subset of T. We will suppose that A ≠ ∅ and A ∩ B = ∅.

One can prove the following proposition.

Property 3. 1 . Let n be a natural number. Then there exists a function G from dyadic(n) into bool T such that for elements r_{1},r_{2} of dyadic(n) if r_{1} < r_{2} , then G(r_{1}) is open and

G(r_{2}) is open and \overline{G(r_{1})}⊂ G(r_{2}) and A ⊂ G(0) and G(1) = T \ B .

A function satisfying the thesis of the above proposition is said to be a drizzle of A,B,n.

Definition 3. 1 . A function G from dyadic(n) into bool T is said to be a drizzle of A,B,n if satisfies the condition:

for elements r_{1},r_{2} of dyadic(n) if r_{1} < r_{2} , then G(r_{1}) is open and G(r_{2}) is open and

\overline{G(r_{1})}⊂ G(r_{2}) and A ⊂ G(0) and G(1) = T \ B .

Considering Prop. 3.1, it is easy to prove the following by Def. 3.1:

Property 3. 2 . Let n be a natural number and D be a drizzle of A,B,n . Then A ∈ D(0)

and B = T \ D(1).

One can prove the following proposition.

Property 3. 3 . Let n be a natural number and G be a drizzle of A,B,n . Then there exists

a drizzle F of A,B,n + 1 such that for every element r of dyadic(n + 1) if r ∈ dyadic(n), then F (r) = G(r).

For a set S_{1},S_{2} by P(S_{1},S_{2}) we denote the set of partial functions from S_{1} into S_{2} . For F which is a partial function by dom(F) we denote the domain of F.

Now we state the following proposition:

Property 3. 4 . Let n be a natural number. Then every drizzle of A,B,n is an element of

P(DYADIC,bool T).

Property 3. 5 . Exists a sequence F of partial functions from P(DYADIC,bool T) such that for every natural number n holds :

F (n) is a drizzle of A,B,n and for every element r of dom(F (n)) holds F (n)(r) = F (n + 1)(r)

From the above property, we can introduce the following:

Definition 3. 2 . A sequence D of partial functions from P(DYADIC,bool T) is said to be a rain of A,B if it satisfies the condition: for every natural number n , D(n) is a drizzle of A,B,n and for every element r of

dom(D(n)) holds D(n)(r) = D(n + 1)(r) .

From Def. 3.1 we can infer that for every natural number n and D a rain of A,B

dom(D(n)) = dyadic(n) .

In the classical proof of Urysohn’s lemma, a rain of A,B is named a Urysohn’s "onion" function.

Definition 3. 3 . For a real number x, InfDyadic x yields such a natural number which satisfies the following conditions:

InfDyadic x = 0 iff x ∈ dyadic(0) and for every natural number n such that x ∈ dyadic(n+ 1) and x ∉ dyadic(n) InfDyadic x = n + 1 .

The following properties are true.

Property 3. 6 . For every real number x such that x ∈ DYADIC holds x ∈ dyadic(InfDyadic x) .

Property 3. 7 . For every real number x such that x ∈ DYADIC and for every natural number

n such that InfDyadic x ≤ n holds x ∈ dyadic(n) .

Property 3. 8 . For every real number x such that x ∈ DYADIC and for every natural number n such that x ∈ dyadic(n) holds InfDyadic x ≤ n.

The next three theorems are not so difficult to prove.

Theorem 3 . Let G be a rain of A,B and let x be a real number such that x ∈ DYADIC.

Then for every natural number n holds G(InfDyadic x)(x) = G((InfDyadic x) + n)(x) .

Theorem 4 . Let G be a rain of A,B and let x be a real number such that x ∈ DYADIC. Then there exists an element y of bool T such that for every natural number n if x ∈ dyadic(n)

then y = G(n)(x) .

Theorem 5 . Let G be a rain of A,B . Then there exists a function F from DOM into bool T such that for every real number x holds

if x ∈ R_{<0} then F (x) = ∅ and if x ∈ R_{>1} then F (x) = T and

if x ∈ DYADIC , then for every natural number n such that

x ∈ dyadic(n) holds F (x) = G(n)(x) ;

From the above theorem arises the correctness of the definition

Definition 3. 4 . Let D be a rain of A,B . The functor Tempest D yielding a function from DOM into bool T is defined by the condition: for every real number x holds

if x ∈ R_{<0} then (Tempist D)(x) = ∅ and if x ∈ R_{>1} then (Tempist D)(x) = T and

if x ∈ DYADIC , then for every natural number n such that

x ∈ dyadic(n) holds (Tempist D)(x) = D(n)(x) .

By applying the above definition one can prove the following properties:

Property 3. 9 . Let D be a rain of A,B and let r be a real number. If r ∈ DOM then

(Tempest D)(r) is open.

Property 3. 10 . Let D be a rain of A,B then for r_{1},r_{2} being real numbers such that

r_{1} ∈ DOM and r_{2} ∈ DOM and r_{1} < r_{2} holds \overline{(Tempest D)(r_{1})}⊂ (Tempest D)(r_{2}) .

In the next property R̃ denotes the set of extended real numbers, i.e., the set R̃ = R ∩

{−∞,+∞}.

Property 3. 11 . Let D be a rain of A,B and p be a point of T then there exists a subset Q of R̃ such that for every element x of R̃ holds x ∈ Q if and only if the following condition is satisfied:

x ∈ DYADIC and p ∉ (Tempest D)(x) .

In the above property, in reality we could have placed R in place of R̃, but the functor sup necessary in the following is defined in MML only in R̃.

Definition 3. 5 . Let D be a rain of A,B and let p be a point of T . The functor Rainbow(p,D) yielding a subset of R̃ is defined by: for every element x of R̃ holds x ∈ Rainbow(p,D) if and only if the following condition are satisfied:

x ∈ DYADIC and p ∉ (Tempest D)(x) .

One can prove the following properties:

Property 3. 12 . Let D be a rain of A,B and let p be a point of T then Rainbow(p,D) ⊂ DYADIC .

Property 3. 13 . Let D be a rain of A,B. Then there exists a map F from T into R^{1} such that for every point p of T holds :

if Rainbow(p,D) = ∅ then F (p) = 0 and if Rainbow(p,D) ≠ ∅ then F (p) = sup Rainbow(p,D) .

In the above property R^{1} means the set of real numbers R like a topological space. Functor sup is understood in the usual sense.

Definition 3. 6 . Let D be a rain of A,B . The functor T hunder D yielding a map from T into R^{1} is defined by the condition: let p be a point of T , then if Rainbow(p,D) = ∅ then

(T hunder D)(p) = 0 and if Rainbow(p,D) ≠ ∅ then (T hunder D)(p) = sup Rainbow(p,D) .

The following properties are true.

Property 3. 14 . Let D be a rain of A,B and let p be a point of T then if Rainbow(p,D) ≠ ∅ then 0 ≤ sup Rainbow(p,D) and sup Rainbow(p,D) ≤ 1.

Property 3. 15 . Let D be a rain of A,B and r be an element of DOM , and p be a point of T then from

(T hunder D)(p) < r follows p ∈ (Tempest D)(r) .

Property 3. 16 . Let D be a rain of A,B and n be a natural number and r be an element of DOM such that 0 < r . For every point p of T such that r < (T hunder D)(p) holds

p ∉ (Tempest D)(r) .

Property 3. 17 . Let D be a rain of A,B and r be a real number such that 0 < r and r ∈

DYADIC ∪R_{>1} . Let p be a point of T . If p ∈ (Tempest D)(r), then (T hunder D)(p) ≤ r .

From the next theorem we can observe that for a rain D of A,B T hunder D is a function which satisfies the thesis of Urysohn’s lemma.

Theorem 6 . Let D be rain of A,B. T hunder D is continuous and for every point x of T holds:

0 ≤ (T hunder D)(x) and (T hunder D)(x) ≤ 1 and if x ∈ A then (T hunder D)(x) = 0 and if x ∈ B then (T hunder D)(x) = 1 .

Under the assumption given in the beginning of this section, from the above theorem we have

Theorem 7 . Exists a map F from T to R^{1} such that F is continuous and for every point x of T holds:

0 ≤ F (x) and F (x) ≤ 1 and if x ∈ A then F (x) = 0 and if x ∈ B then F (x) = 1 .

The last two theorems we express below.

Urysohn’s lemma 2 . Let T be a non empty T_{4} topological space and let A,B be closed subsets of T . Suppose that A ∩ B = ∅. Then there exists a map F from T to R^{1} such that F is continuous and for every point x of T holds:

0 ≤ F (x) and F (x) ≤ 1 and if x ∈ A then F (x) = 0 and if x ∈ B then F (x) = 1 .

Urysohn’s lemma 3 . Let T be a non empty T_{2} topological space and let A,B be closed subsets of T . Suppose that T is compact and A ∩ B = ∅ . Then there exists a map F from T to R^{1} such that F is continuous and for every point x of T holds:

0 ≤ F (x) and F (x) ≤ 1 and if x ∈ A then F (x) = 0 and if x ∈ B then F (x) = 1 .

3. Future Formalization of Urysohn’s Lemma

We will consider if in this place we ought to put down some remarks about file URYSOHN4.miz for example concerning application of Urysohn’s lemma in formalization of Tietze extension theorem.

References

[1] J. L. Kelley, General Topology, von Nostnend, 1955.

[2] N. Bourbaki, Topologie Generale, Herman, Paris, 1966.

[3] K. Yoshida, Functional Analysis, Springer Verlag, Berlin, 1965.

[4] J. Dieudonné, Foundations of Modern Analysis, Academic Press, New York, 1960.

[5] J. Białas, Y. Nakamura, Dyadic Numbers and T_{4} Topological Spaces, Formalized Mathematics, 5(3), 1996, pp. 361-366.

[6] J. Białas, Y. Nakamura, Some Properties of Dyadic Numbers and Intervals, Formalized Mathematics, 9(3), 2001, pp. 627-630.

[7] J. Białas, Y. Nakamura, The Urysohn Lemma, Formalized Mathematics, 9(3), 2001, pp. 631-636.

[8] J. Białas, Infimum and Supremum of the Set of Real Numbers, Formalized Mathematics, 2(1), 1991, pp. 163-171.

[9] J. Białas, Properties of the Intervals of Real Numbers, Formalized Mathematics, 3(2), 1992, pp. 263-269.

[10] J. Białas, Some Properties of the Intervals, Formalized Mathematics, 5(1), 1996, pp. 21-26.