Mechanized Mathematics and Its Applications, Vol. 6, No. 1, November 2007, 41:45

Formalization of the Tietze extension theorem in Mizar^{⋆}

Adam Naumowicz

Institute of Computer Science University of Białystok, Poland

adamn@mizar.org

Abstract – In this paper we report on the formalization of the Tietze extension theorem using the Mizar system. This theorem has been formalized as a part of the project aimed at formalizing the Jordan curve theorem. However, this development has turned out to be also useful for other formalizations.

1. Introduction

The main theorem attributed to the Austrian mathematician Heinrich Franz Friedrich Tietze (1880 – 1964) states that if X is a normal topological space and f : A → ℝ is a continuous map from a closed subset A of X into the real numbers carrying the standard topology, then there exists a continuous map F : X → ℝ with F (a) = f(a) for all a in A. Then F is called a continuous extension of f and the theorem is referred to as the Tietze extension theorem.

The theorem generalizes Urysohn’s lemma and is widely applicable, since all metric spaces and all compact Hausdorff spaces are normal. Although being important as such, unlike the Urysohn’s lemma which was formalized in Mizar in 2001 ([2]), the Tietze theorem had not been formalized until it became indispensable in order to complete a crucial part of the proof of the Jordan curve theorem ([5]) that has been initiated according to [9] and completed according to [3].

2. Formalization

The result of formalization of the Tietze extension theorem is documented in [6]. In the following we present the most important aspects of this development.

2.1 The formulation

The theorem is usually phrased in the form of an equivalence that provides a characterization of normal spaces. The actual formulations, however, may vary - below are some possible versions:

• The topological space X is normal if and only if for all closed subsets A of X, every continuous function f : A → [−1,1] can be extended to a continuous function F : X → [−1,1].

⋆ This work has been partially supported by the FP6 IST project no. 510996 Types for Proofs and Programs (TYPES).

Manuscript received August 22, 2007; revised September 12, 2007.

• The topological space X is normal if and only if for all closed subsets A of X, every continuous function f : A → (−1,1) can be extended to a continuous function F : X → (−1,1).

• The topological space X is normal if and only if for all closed subsets A of X, every continuous function f : A → ℝ can be extended to a continuous function F : X → ℝ.

In our formalization we adopted the first formulation and followed the proof presented at the PlanetMath server^{1}.

Please note that with the second formulation, i.e., if f is a function satisfying |f(x)| < 1, we find an extension F of f as in the first case. The set B = F^{−1} ({−1} ∪ {1}) is closed and disjoint from A because |F (x)| = |f(x)| < 1 for x ∈ A. By Urysohn’s lemma there is a continuous function ϕ such that ϕ(A) = {1} and ϕ(B) = {0}. Hence F (x)ϕ(x) is a continuous extension of f(x), and has the property that |F (x)ϕ(x)| < 1.

If f is unbounded as permitted with the third formulation, consider t(x) = tan^{−1} (x)/(π/2). The function t ∘ f has the property that (t ∘ f)(x) < 1 for x ∈ A so it can be extended to a continuous function h: X → ℝ which has the property |h(x)| < 1. Then t^{−1} ∘ h is a continuous extension of f.

For storing the theorem in the Mizar library it seemed more convenient to state it as two implications rather than an equivalence:

theorem :: TIETZE:25 T is being_T4 implies for A being closed Subset of T for f being Function of T|A, Closed-Interval-TSpace(-1,1)

st f is continuous ex g being continuous Function of T, Closed-Interval-TSpace(-1,1)

st g|A = f;

theorem :: TIETZE:26 (for A being non empty closed Subset of T for f being continuous Function of T|A, Closed-Interval-TSpace(-1,1) ex g being continuous Function of T, Closed-Interval-TSpace(-1,1)

st g|A = f) implies T is being_T4;

Separating the two implications enables us to check immediately which of them is actually needed in a particular situation.

A notational comment is also due here - the distinction that some authors make between the notions of normal and T_{4} spaces is often a source of confusion. Let us clarify that in the Mizar library the T_{4} spaces are introduced to fulfill only the separation axiom which states that if A and B are disjoint closed subsets of the space, then there are disjoint open subsets U and V such that A ⊆ U and B ⊆ V. Therefore Mizar’s T_{4} spaces need not be T_{1} - this is what many authors call normal spaces, instead.

1 http://planetmath.org/encyclopedia/ProofOfTietzeExtensionTheorem2.html

2.2 The proof

In order to prove the first of the above implications (TIETZE:25), a lemma was required that stated the following:

If T is a T_{4} topological space and A is closed in T, then for any continuous function f: A → ℝ such that |f(x)| ≤ 1, there is a continuous function g: X → ℝ such that |g(x)| ≤ \frac{1}{3}

for x ∈ T, and |f(x) − g(x)| ≤ \frac{2}{3} for x ∈ A.

We formalized it in a slightly generalized form:

theorem :: TIETZE:19 r > 0 & T is being_T4 implies for f being continuous Function of T|A, R^1 st f,A is_absolutely_bounded_by r ex g being continuous Function of T, R^1 st g,dom g is_absolutely_bounded_by r/3 &

f-g,A is_absolutely_bounded_by 2*r/3;

The proof we formalized is as follows. Let T be T_{4} and A be closed in T. By the above lemma (TIETZE:19), there is a continuous function g_{0}: X → ℝ such that |g_{0}(x)| ≤ \frac{1}{3} for x ∈ X and |f(x)−g_{0}(x)| ≤ \frac{2}{3} for x ∈ A. Since (f −g_{0}): A → ℝ is continuous, the lemma tells us there is a continuous function g_{1}: X → ℝ such that |g_{1}(x)| ≤ \frac{1}{3}(\frac{2}{3}) for x ∈ X and |f(x) − g_{0}(x) −

g_{1}(x)| ≤ \frac{2}{3}(\frac{2}{3}) for x ∈ A.

At this point the informal proof we followed required a repeated application of the lemma in order to construct a sequence of continuous functions g_{0},g_{1},g_{2},... such that |g_{n}(x)| ≤ \frac{1}{3}(\frac{2}{3})^{n} for all x ∈ T, and |f(x) − g_{0}(x) − g_{1}(x) − g_{2}(x) − ...| ≤ (\frac{2}{3})^{n} for x ∈ A. To formalize this in Mizar, we had to use one of the schemes for defining recursive functions from [4]. Then we could define F (x) = ∑ _{n=0}^{∞} g_{n}(x). Since |g_{n}(x)| ≤ \frac{1}{3}(\frac{2}{3})^{n} and ∑ _{n=0}^{∞} \frac{1}{3}(\frac{2}{3})^{n} converges as a geometric series, then ∑ _{n=0}^{∞} g_{n}(x) converges absolutely and uniformly, so F is a continuous function defined everywhere. Moreover ∑ _{n=0}^{∞} \frac{1}{3}(\frac{2}{3})^{n} = 1 implies that |F (x)| ≤ 1.

In our formalization the above conclusions were obtained thanks to the following lemma:

theorem :: TIETZE:11 for X,Z being non empty set for F being Functional_Sequence of X,REAL st Z common_on_dom F for a,r being positive (real number) st r < 1 & for n being natural number holds (F.n)-(F.(n+1)), Z is_absolutely_bounded_by a*(r to_power n) holds F is_unif_conv_on Z & for n being natural number holds lim(F,Z)-(F.n), Z is_absolutely_bounded_by a*(r to_power n)/(1-r);

Finally for x ∈ A, we have that |f(x) − ∑ _{n=0}^{k} g_{n}(x)| ≤ (\frac{2}{3})^{k+1} and as k goes to infinity, the right side goes to zero and the sum goes to F (x). Thus |f(x)−F (x)| = 0. Therefore F extends f, which completes the proof of this implication.

To prove the second implication of the Tietze extension theorem (TIETZE:26), we first had to formalize the respective variant of Urysohn’s lemma - NB: this was not done in [2].

theorem :: TIETZE:20 (for A, B being non empty closed Subset of T st A misses B ex f being continuous Function of T, R^1 st f.:A = {0} & f.:B = {1}) implies T is_T4;

From this, we first suppose that for any continuous function on a closed subset there is a continuous extension. Let A and B be disjoint and closed in T. Define f: A ∪ B → ℝ by f(x) = 0 for x ∈ A and f(x) = 1 for x ∈ B. Now f is continuous and we can extend it to a continuous function F : T → ℝ. By the Urysohn’s lemma we proved before (TIETZE:20), T is T_{4} because F is a continuous function such that F (x) = 0 for x ∈ A and F (x) = 1 for x ∈ B.

2.3 The influence on MML

As we stated previously, the Tietze extension theorem was used directly in the final part of the proof of the Jordan curve theorem ([5]). The theorem actually used was TIETZE:25, i.e., the implication that states the existence of a suitable extension function. But now it is not the only MML article that draws on this result. Another topological development presented in [1] also uses it to show that the Nemytzki plane is an example of a Tychonoff space which is not T_{4}.

Another article that used some information formalized in [6] was [7] in which homeomorphisms of Jordan curves were analyzed - this article was also used in the proof of the Jordan curve theorem. Namely, a quite trivial but useful lemma of this form was re-used:

theorem :: TIETZE:6 for T1 being empty TopSpace, T2 being TopSpace for f being Function of T1,T2 holds f is continuous;

Quite surprisingly, some theorems developed in [6] were also used in [8]:

theorem :: TIETZE:7 for f,g being summable Real_Sequence st for n being Element of NAT holds f.n <= g.n holds Sum f <= Sum g;

theorem :: TIETZE:8 for f being Real_Sequence st f is absolutely_summable holds abs Sum f <= Sum abs f;

These theorems were proved in [6] in order to show properties of sequences constructed for defining the extension functions. However, since they were formalized in a form of general lemmas, they could also be of perfect use for an article on Catalan numbers.

3. Conclusions

From today’s perspective it seems that proving the Tietze extension theorem in Mizar was an important development. Not only did it help complete the proof of the Jordan curve theorem, which is of course its main value, but it was also used by a new formalization in topology – the Niemytzki plane. The theorem also gave new evidence that properly formulated lemmas can be useful for further developments – it is definitely worth the effort to create lemmas as general as possible so that new articles, sometimes apparently concerning different fields of mathematics, can be written more easily by drawing on them.

References

[1] Bancerek, G., Niemytzki Plane – an Example of Tychonoff Space Which Is Not T_{4}, Formalized Mathematics, 13(4), 2005, pp.515–524.

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

[3] Gauld, D., Brouwer’s Fixed Point Theorem and the Jordan Curve Theorem, URL: http://aitken.math.

auckland.ac.nz/~gauld/750-05/section5.pdf.

[4] Hryniewiecki, K., Recursive definitions, Formalized Mathematics, 1(2), 1990, pp.321–328.

[5] Korniłowicz, A., Jordan Curve Theorem, Formalized Mathematics, 13(4), 2005, pp.481–491.

[6] Korniłowicz, A., Bancerek, G. and Naumowicz, A., Tietze Extension Theorem, Formalized Mathematics, 13(4), 2005, pp.471–475.

[7] Naumowicz, A. and Bancerek, G., Homeomorphisms of Jordan Curves, Formalized Mathematics, 13(4), 2005, pp.477–480.

[8] Pa̧k, K., The Catalan Numbers. Part II, Formalized Mathematics, 14(4), 2006, pp.153–159.

[9] Takeuchi, Y. and Nakamura, Y., On the Jordan curve theorem, Technical Report 19804, Dept. of Information Eng., Shinshu University, 1980.