Tietze extension theorem #
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_isClosedEmbedding.
In addition we provide a class TietzeExtension encoding the idea that a topological space
satisfies the Tietze extension theorem. This allows us to get a version of the Tietze extension
theorem that simultaneously applies to ℝ, ℝ × ℝ, ℂ, ι → ℝ, ℝ≥0 et cetera. At some point
in the future, it may be desirable to provide instead a more general approach via
absolute retracts, but the current implementation covers the most common use cases easily.
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 = (↑).
Tags #
Tietze extension theorem, Urysohn's lemma, normal topological space
The TietzeExtension class #
A class encoding the concept that a space satisfies the Tietze extension property.
- exists_restrict_eq' : ∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] (s : Set X), IsClosed s → ∀ (f : C(↑s, Y)), ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f
Instances
Tietze extension theorem for TietzeExtension spaces, a version for a closed set. Let
s be a closed set in a normal topological space X. Let f be a continuous function
on s with values in a TietzeExtension space Y. Then there exists a continuous function
g : C(X, Y) such that g.restrict s = f.
Tietze extension theorem for TietzeExtension spaces. Let e be a closed embedding of a
nonempty topological space X₁ into a normal topological space X. Let f be a continuous
function on X₁ with values in a TietzeExtension space Y. Then there exists a
continuous function g : C(X, Y) such that g ∘ e = f.
Tietze extension theorem for TietzeExtension spaces. Let e be a closed embedding of a
nonempty topological space X₁ into a normal topological space X. Let f be a continuous
function on X₁ with values in a TietzeExtension space Y. Then there exists a
continuous function g : C(X, Y) such that g ∘ e = f.
This version is provided for convenience and backwards compatibility. Here the composition is phrased in terms of bare functions.
This theorem is not intended to be used directly because it is rare for a set alone to
satisfy [TietzeExtension t]. For example, Metric.ball in ℝ only satisfies it when
the radius is strictly positive, so finding this as an instance will fail.
Instead, it is intended to be used as a constructor for theorems about sets which do satisfy
[TietzeExtension t] under some hypotheses.
This theorem is not intended to be used directly because it is rare for a set alone to
satisfy [TietzeExtension t]. For example, Metric.ball in ℝ only satisfies it when
the radius is strictly positive, so finding this as an instance will fail.
Instead, it is intended to be used as a constructor for theorems about sets which do satisfy
[TietzeExtension t] under some hypotheses.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any retract of a TietzeExtension space is one itself.
Any homeomorphism from a TietzeExtension space is one itself.
The Tietze extension theorem for ℝ.
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.
Alias of BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding'.
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.
Alias of BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding.
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_isClosedEmbedding 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.
Alias of BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_isClosedEmbedding.
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_isClosedEmbedding 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₂.
Alias of BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_isClosedEmbedding.
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 OrdConnected 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.
Alias of BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding.
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 OrdConnected 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
OrdConnected 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 OrdConnected 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.
Alias of ContinuousMap.exists_extension_forall_mem_of_isClosedEmbedding.
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 OrdConnected 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.
Alias of ContinuousMap.exists_extension'.
Tietze extension theorem for TietzeExtension spaces. Let e be a closed embedding of a
nonempty topological space X₁ into a normal topological space X. Let f be a continuous
function on X₁ with values in a TietzeExtension space Y. Then there exists a
continuous function g : C(X, Y) such that g ∘ e = f.
This version is provided for convenience and backwards compatibility. Here the composition is phrased in terms of bare functions.
Alias of ContinuousMap.exists_extension'.
Alias of ContinuousMap.exists_extension'.
Tietze extension theorem for TietzeExtension spaces. Let e be a closed embedding of a
nonempty topological space X₁ into a normal topological space X. Let f be a continuous
function on X₁ with values in a TietzeExtension space Y. Then there exists a
continuous function g : C(X, Y) such that g ∘ e = f.
This version is provided for convenience and backwards compatibility. Here the composition is phrased in terms of bare functions.
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 OrdConnected 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.
Alias of ContinuousMap.exists_restrict_eq.
Tietze extension theorem for TietzeExtension spaces, a version for a closed set. Let
s be a closed set in a normal topological space X. Let f be a continuous function
on s with values in a TietzeExtension space Y. Then there exists a continuous function
g : C(X, Y) such that g.restrict s = f.
Tietze extension theorem for real-valued continuous maps.
ℝ is a TietzeExtension space.
Equations
Tietze extension theorem for nonnegative real-valued continuous maps.
ℝ≥0 is a TietzeExtension space.