Tietze extension theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove a few version of the Tietze extension theorem. The theorem says that a
continuous function s → ℝ defined on a closed set in a normal topological space Y can be
extended to a continuous function on the whole space. Moreover, if all values of the original
function belong to some (finite or infinite, open or closed) interval, then the extension can be
chosen so that it takes values in the same interval. In particular, if the original function is a
bounded function, then there exists a bounded extension of the same norm.
The proof mostly follows https://ncatlab.org/nlab/show/Tietze+extension+theorem. We patch a small
gap in the proof for unbounded functions, see
exists_extension_forall_exists_le_ge_of_closed_embedding.
Implementation notes #
We first prove the theorems for a closed embedding e : X → Y of a topological space into a normal
topological space, then specialize them to the case X = s : set Y, e = coe.
Tags #
Tietze extension theorem, Urysohn's lemma, normal topological space
One step in the proof of the Tietze extension theorem. If e : C(X, Y) is a closed embedding
of a topological space into a normal topological space and f : X →ᵇ ℝ is a bounded continuous
function, then there exists a bounded continuous function g : Y →ᵇ ℝ of the norm ‖g‖ ≤ ‖f‖ / 3
such that the distance between g ∘ e and f is at most (2 / 3) * ‖f‖.
Tietze extension theorem for real-valued bounded continuous maps, a version with a closed
embedding and bundled composition. If e : C(X, Y) is a closed embedding of a topological space
into a normal topological space and f : X →ᵇ ℝ is a bounded continuous function, then there exists
a bounded continuous function g : Y →ᵇ ℝ of the same norm such that g ∘ e = f.
Tietze extension theorem for real-valued bounded continuous maps, a version with a closed
embedding and unbundled composition. If e : C(X, Y) is a closed embedding of a topological space
into a normal topological space and f : X →ᵇ ℝ is a bounded continuous function, then there exists
a bounded continuous function g : Y →ᵇ ℝ of the same norm such that g ∘ e = f.
Tietze extension theorem for real-valued bounded continuous maps, a version for a closed
set. If f is a bounded continuous real-valued function defined on a closed set in a normal
topological space, then it can be extended to a bounded continuous function of the same norm defined
on the whole space.
Tietze extension theorem for real-valued bounded continuous maps, a version for a closed
embedding and a bounded continuous function that takes values in a non-trivial closed interval.
See also exists_extension_forall_mem_of_closed_embedding for a more general statement that works
for any interval (finite or infinite, open or closed).
If e : X → Y is a closed embedding and f : X →ᵇ ℝ is a bounded continuous function such that
f x ∈ [a, b] for all x, where a ≤ b, then there exists a bounded continuous function
g : Y →ᵇ ℝ such that g y ∈ [a, b] for all y and g ∘ e = f.
Tietze extension theorem for real-valued bounded continuous maps, a version for a closed
embedding. Let e be a closed embedding of a nonempty topological space X into a normal
topological space Y. Let f be a bounded continuous real-valued function on X. Then there
exists a bounded continuous function g : Y →ᵇ ℝ such that g ∘ e = f and each value g y belongs
to a closed interval [f x₁, f x₂] for some x₁ and x₂.
Tietze extension theorem for real-valued bounded continuous maps, a version for a closed
embedding. Let e be a closed embedding of a nonempty topological space X into a normal
topological space Y. Let f be a bounded continuous real-valued function on X. Let t be
a nonempty convex set of real numbers (we use ord_connected instead of convex to automatically
deduce this argument by typeclass search) such that f x ∈ t for all x. Then there exists
a bounded continuous real-valued function g : Y →ᵇ ℝ such that g y ∈ t for all y and
g ∘ e = f.
Tietze extension theorem for real-valued bounded continuous maps, a version for a closed
set. Let s be a closed set in a normal topological space Y. Let f be a bounded continuous
real-valued function on s. Let t be a nonempty convex set of real numbers (we use
ord_connected instead of convex to automatically deduce this argument by typeclass search) such
that f x ∈ t for all x : s. Then there exists a bounded continuous real-valued function
g : Y →ᵇ ℝ such that g y ∈ t for all y and g.restrict s = f.
Tietze extension theorem for real-valued continuous maps, a version for a closed
embedding. Let e be a closed embedding of a nonempty topological space X into a normal
topological space Y. Let f be a continuous real-valued function on X. Let t be a nonempty
convex set of real numbers (we use ord_connected instead of convex to automatically deduce this
argument by typeclass search) such that f x ∈ t for all x. Then there exists a continuous
real-valued function g : C(Y, ℝ) such that g y ∈ t for all y and g ∘ e = f.
Tietze extension theorem for real-valued continuous maps, a version for a closed
embedding. Let e be a closed embedding of a nonempty topological space X into a normal
topological space Y. Let f be a continuous real-valued function on X. Then there exists a
continuous real-valued function g : C(Y, ℝ) such that g ∘ e = f.
Tietze extension theorem for real-valued continuous maps, a version for a closed set. Let
s be a closed set in a normal topological space Y. Let f be a continuous real-valued function
on s. Let t be a nonempty convex set of real numbers (we use ord_connected instead of convex
to automatically deduce this argument by typeclass search) such that f x ∈ t for all x : s. Then
there exists a continuous real-valued function g : C(Y, ℝ) such that g y ∈ t for all y and
g.restrict s = f.
Tietze extension theorem for real-valued continuous maps, a version for a closed set. Let
s be a closed set in a normal topological space Y. Let f be a continuous real-valued function
on s. Then there exists a continuous real-valued function g : C(Y, ℝ) such that
g.restrict s = f.