Documentation

Mathlib.Topology.TietzeExtension

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_closedEmbedding.

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.

Instances
    theorem TietzeExtension.exists_restrict_eq' {Y : Type v} [TopologicalSpace Y] [self : TietzeExtension Y] {X : Type u} [TopologicalSpace X] [NormalSpace X] (s : Set X) (hs : IsClosed s) (f : C(s, Y)) :
    ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f
    theorem ContinuousMap.exists_restrict_eq {X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (f : C(s, Y)) :
    ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f

    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.

    theorem ContinuousMap.exists_extension {X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁X} (he : ClosedEmbedding e) {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (f : C(X₁, Y)) :
    ∃ (g : C(X, Y)), g.comp { toFun := e, continuous_toFun := } = 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.

    theorem ContinuousMap.exists_extension' {X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁X} (he : ClosedEmbedding e) {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (f : C(X₁, Y)) :
    ∃ (g : C(X, Y)), 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.

    theorem ContinuousMap.exists_forall_mem_restrict_eq {X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) {Y : Type v} [TopologicalSpace Y] (f : C(s, Y)) {t : Set Y} (hf : ∀ (x : s), f x t) [ht : TietzeExtension t] :
    ∃ (g : C(X, Y)), (∀ (x : X), g x t) ContinuousMap.restrict s g = f

    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.

    theorem ContinuousMap.exists_extension_forall_mem {X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁X} (he : ClosedEmbedding e) {Y : Type v} [TopologicalSpace Y] (f : C(X₁, Y)) {t : Set Y} (hf : ∀ (x : X₁), f x t) [ht : TietzeExtension t] :
    ∃ (g : C(X, Y)), (∀ (x : X), g x t) g.comp { toFun := e, continuous_toFun := } = f

    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.

    instance Pi.instTietzeExtension {ι : Type u_1} {Y : ιType v} [(i : ι) → TopologicalSpace (Y i)] [∀ (i : ι), TietzeExtension (Y i)] :
    TietzeExtension ((i : ι) → Y i)
    Equations
    • =
    theorem TietzeExtension.of_retract {Y : Type v} {Z : Type w} [TopologicalSpace Y] [TopologicalSpace Z] [TietzeExtension Z] (ι : C(Y, Z)) (r : C(Z, Y)) (h : r.comp ι = ContinuousMap.id Y) :

    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.

    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.

    theorem BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ) {a : } {b : } {e : XY} (hf : ∀ (x : X), f x Set.Icc a b) (hle : a b) (he : ClosedEmbedding e) :
    ∃ (g : BoundedContinuousFunction Y ), (∀ (y : Y), g y Set.Icc a b) g e = f

    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_closedEmbedding 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.

    theorem BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] [Nonempty X] (f : BoundedContinuousFunction X ) {e : XY} (he : ClosedEmbedding e) :
    ∃ (g : BoundedContinuousFunction Y ), (∀ (y : Y), ∃ (x₁ : X) (x₂ : X), g y Set.Icc (f x₁) (f x₂)) 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₂.

    theorem BoundedContinuousFunction.exists_extension_forall_mem_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ) {t : Set } {e : XY} [hs : t.OrdConnected] (hf : ∀ (x : X), f x t) (hne : t.Nonempty) (he : ClosedEmbedding e) :
    ∃ (g : BoundedContinuousFunction Y ), (∀ (y : Y), g y t) 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. 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.

    theorem BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed {Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction s ) (hs : IsClosed s) {t : Set } [t.OrdConnected] (hf : ∀ (x : s), f x t) (hne : t.Nonempty) :
    ∃ (g : BoundedContinuousFunction Y ), (∀ (y : Y), g y t) g.restrict s = 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.

    theorem ContinuousMap.exists_extension_forall_mem_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : C(X, )) {t : Set } {e : XY} [hs : t.OrdConnected] (hf : ∀ (x : X), f x t) (hne : t.Nonempty) (he : ClosedEmbedding e) :
    ∃ (g : C(Y, )), (∀ (y : Y), g y t) 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. 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.

    @[deprecated ContinuousMap.exists_extension']
    theorem ContinuousMap.exists_extension_of_closedEmbedding {X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁X} (he : ClosedEmbedding e) {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (f : C(X₁, Y)) :
    ∃ (g : C(X, Y)), 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.

    theorem ContinuousMap.exists_restrict_eq_forall_mem_of_closed {Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : C(s, )) {t : Set } [t.OrdConnected] (ht : ∀ (x : s), f x t) (hne : t.Nonempty) (hs : IsClosed s) :
    ∃ (g : C(Y, )), (∀ (y : Y), g y t) ContinuousMap.restrict s g = 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 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.

    @[deprecated ContinuousMap.exists_restrict_eq]
    theorem ContinuousMap.exists_restrict_eq_of_closed {X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (f : C(s, Y)) :
    ∃ (g : C(X, Y)), ContinuousMap.restrict s g = 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.

    Equations