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 . We patch a small gap in the proof for unbounded functions, see exists_extension_forall_exists_le_ge_of_closedEmbedding.

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

theorem BoundedContinuousFunction.tietze_extension_step {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)) (he : ClosedEmbedding ⇑e) : ∃ (g : BoundedContinuousFunction Y ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (BoundedContinuousFunction.compContinuous g e) f ≤ 2 / 3 * ‖f‖

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

theorem BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)) (he : ClosedEmbedding ⇑e) : ∃ (g : BoundedContinuousFunction Y ℝ), ‖g‖ = ‖f‖ ∧ BoundedContinuousFunction.compContinuous g e = 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.

theorem BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : ClosedEmbedding e) : ∃ (g : BoundedContinuousFunction Y ℝ), ‖g‖ = ‖f‖ ∧ ⇑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.

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

theorem ContinuousMap.exists_extension_of_closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : C(X, ℝ)) (e : X → Y) (he : ClosedEmbedding e) : ∃ (g : C(Y, ℝ)), ⇑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.

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 ℝ} [Set.OrdConnected t] (ht : ∀ (x : ↑s), f x ∈ t) (hne : Set.Nonempty t) (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 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.

theorem ContinuousMap.exists_restrict_eq_of_closed {Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : C(↑s, ℝ)) (hs : IsClosed s) : ∃ (g : C(Y, ℝ)), 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. Then there exists a continuous real-valued function g : C(Y, ℝ) such that g.restrict s = f.