BoundedContinuousFunction.tietze_extension_step
theorem BoundedContinuousFunction.tietze_extension_step :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
(f : BoundedContinuousFunction X ℝ) (e : C(X, Y)),
ClosedEmbedding ⇑e → ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
This theorem is one step in the proof of the Tietze extension theorem. It states that given a closed embedding `e` of a topological space `X` into a normal topological space `Y`, and a bounded continuous function `f` from `X` to the real numbers, there exists a bounded continuous function `g` from `Y` to the real numbers such that the norm of `g` is less than or equal to one third of the norm of `f`, and the distance between `g` composed with `e` and `f` is at most two thirds of the norm of `f`.
More concisely: Given a closed embedding of a topological space X into a normal space Y and a bounded continuous function f from X to the real numbers, there exists a bounded continuous g from Y to the real numbers with norm less than or equal to 1/3 * norm(f) such that |g ∘ e - f| ≤ 2/3 * norm(f).
|
ContinuousMap.exists_extension_forall_mem_of_closedEmbedding
theorem ContinuousMap.exists_extension_forall_mem_of_closedEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
(f : C(X, ℝ)) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected],
(∀ (x : X), f x ∈ t) → t.Nonempty → ClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
The **Tietze Extension Theorem** for real-valued continuous maps, a particular version for a closed embedding, can be described as follows: Given a nonempty topological space `X` embedded into a normal topological space `Y` through a closed embedding `e`, and a continuous real-valued function `f` on `X`. Suppose we have a nonempty convex set `t` of real numbers such that every value of `f` for any `x` in `X` lies in `t` (in Lean 4, we use `OrdConnected` to represent this convex property). Then the theorem asserts that there exists a continuous real-valued function `g` on `Y`, such that every value of `g` for any `y` in `Y` lies in `t` and the composition of `g` and `e` is equal to `f`. In other words, `g` extends `f` over the entire space `Y` while preserving the property that its values lie in the set `t`.
More concisely: Given a closed embedding of a nonempty topological space `X` into a normal space `Y`, and a continuous real-valued function `f` on `X` with domain `X` and image in a convex set `t` of real numbers, there exists a continuous real-valued function `g` on `Y` with domain `Y` such that `g | X = f` and the image of `g` is contained in `t`.
|
BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding'
theorem BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding' :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
(f : BoundedContinuousFunction X ℝ) (e : C(X, Y)), ClosedEmbedding ⇑e → ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
The **Tietze extension theorem** for real-valued bounded continuous maps with a closed embedding and bundled composition, states that if `e` is a closed embedding of a topological space `X` into a normal topological space `Y` and `f` is a bounded continuous function from `X` to `ℝ`, then there exists a bounded continuous function `g` from `Y` to `ℝ` of the same norm as `f` such that `g` composed with `e` equals `f`. In other words, it's possible to extend the bounded continuous function `f` to the larger space `Y` without changing the norm.
More concisely: Given a normal topological space `Y`, a closed embedding `e` of a topological space `X` into `Y`, and a bounded continuous function `f` from `X` to `ℝ`, there exists a bounded continuous function `g` from `Y` to `ℝ` with the same norm as `f`, such that `g ∘ e = f`.
|
TietzeExtension.of_homeo
theorem TietzeExtension.of_homeo :
∀ {Y : Type v} {Z : Type w} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] [inst_2 : TietzeExtension Z],
Y ≃ₜ Z → TietzeExtension Y
This theorem states that if there exists a homeomorphism (a bijective, continuous function whose inverse is also continuous) from a space Y to a space Z, and if Z is a Tietze Extension space (a topological property that guarantees the ability to extend a continuous real-valued function defined on a closed subset to a continuous real-valued function on the whole space), then Y is also a Tietze Extension space.
More concisely: If Y is a Hausdorff space homeomorphic to a Tietze Extension space Z, then Y is also a Tietze Extension space.
|
ContinuousMap.exists_restrict_eq_forall_mem_of_closed
theorem ContinuousMap.exists_restrict_eq_forall_mem_of_closed :
∀ {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : NormalSpace Y] {s : Set Y} (f : C(↑s, ℝ)) {t : Set ℝ}
[inst_2 : t.OrdConnected],
(∀ (x : ↑s), f x ∈ t) → t.Nonempty → IsClosed s → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ContinuousMap.restrict s g = f
This is the **Tietze Extension Theorem** for real-valued continuous maps, specifically for a closed set. The theorem states that given a closed set `s` in a normal topological space `Y`, and a continuous real-valued function `f` that maps from `s` to a nonempty convex set `t` of real numbers (where each `f(x)` belongs to `t` for every `x` in `s`), there exists a continuous real-valued function `g` mapping from `Y` to the real numbers such that `g(y)` belongs to `t` for all `y` in `Y` and the restriction of `g` to `s` equals `f`. In Lean 4, the convexity of `t` is represented through the `OrdConnected` typeclass.
More concisely: Given a closed set in a normal topological space and a continuous real-valued function from the set to a nonempty convex subset of the real numbers, there exists a continuous extension of the function to the entire space.
|
BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding
theorem BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
(f : BoundedContinuousFunction X ℝ) {e : X → Y}, ClosedEmbedding e → ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
The **Tietze extension theorem** for real-valued bounded continuous maps, this version involving a closed embedding and unbundled composition, states that for a closed embedding `e : C(X, Y)` of a topological space into a normal topological space and a bounded continuous function `f : X →ᵇ ℝ`, there exists a bounded continuous function `g : Y →ᵇ ℝ` with the same norm as `f` such that `g` composed with `e` is equivalent to `f`. In other words, the function `f` can be extended over the entire space `Y` preserving the norm (‖∙‖).
More concisely: Given a closed embedding of a topological space into a normal space and a bounded continuous function from the original space to ℝ, there exists a bounded continuous extension to the entire target space with the same norm.
|
BoundedContinuousFunction.exists_norm_eq_restrict_eq_of_closed
theorem BoundedContinuousFunction.exists_norm_eq_restrict_eq_of_closed :
∀ {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : NormalSpace Y] {s : Set Y}
(f : BoundedContinuousFunction ↑s ℝ), IsClosed s → ∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
The **Tietze extension theorem** for real-valued bounded continuous maps is stated as follows for a closed set: Given any topological space 'Y' that is a normal space, for any closed set 's' in 'Y', if 'f' is a bounded continuous real-valued function defined on 's', there exists a function 'g' such that 'g' can be extended to the entire space 'Y' while maintaining the same norm as 'f' and 'g' restricted to 's' is equal to 'f'. In other words, 'f' can be extended from the closed set to the entire space without altering its norm.
More concisely: Given a normal space 'Y' and a closed set 's' in it, any bounded continuous real-valued function 'f' on 's' has a continuous extension 'g' to 'Y' with the same norm.
|
BoundedContinuousFunction.exists_extension_forall_mem_of_closedEmbedding
theorem BoundedContinuousFunction.exists_extension_forall_mem_of_closedEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
(f : BoundedContinuousFunction X ℝ) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected],
(∀ (x : X), f x ∈ t) → t.Nonempty → ClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
This is the **Tietze extension theorem** for real-valued bounded continuous maps, specifically a version for a closed embedding. The theorem states that given a nonempty topological space `X` embedded into a normal topological space `Y` through a closed embedding `e`, and a bounded continuous real-valued function `f` on `X`, along with a nonempty convex set `t` of real numbers such that every `f(x)` is an element of `t`, there exists another bounded continuous real-valued function `g` on `Y` such that for every `y` in `Y`, `g(y)` is in `t`, and `g` composed with `e` equals `f`.
In simpler terms, this theorem says that if we have a continuous function defined on a subset of a space (the image of `X` under `e`), we can extend this function to the whole space (`Y`) while still keeping its values within the set `t`. The conditions that `X` is nonempty and `t` is a convex set of real numbers are necessary to ensure that such extension is possible.
More concisely: Given a nonempty closed subset X of a normal topological space Y, and a bounded continuous real-valued function f on X such that its image is contained in a convex set t of real numbers, there exists a bounded continuous extension g of f to all of Y with image in t.
|
BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_closedEmbedding
theorem BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_closedEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
(f : BoundedContinuousFunction X ℝ) {a b : ℝ} {e : X → Y},
(∀ (x : X), f x ∈ Set.Icc a b) → a ≤ b → ClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ Set.Icc a b) ∧ ⇑g ∘ e = ⇑f
The **Tietze extension theorem** states that for any real-valued bounded continuous function defined on a closed subset of a normal space, there is an extension of this function to the entire space. Specifically, if `e` is a function embedding a topological space `X` into another topological space `Y` in a closed manner and `f` is a bounded continuous function from `X` to the real numbers such that the image of each element of `X` under `f` lies in the closed interval `[a, b]` with `a` less than or equal to `b`, then there exists a bounded continuous function `g` from `Y` to the real numbers such that the image of each element of `Y` under `g` also lies in the interval `[a, b]` and the composition of `g` and `e` equals `f`. In other words, `g` extends `f` while maintaining its bounds and continuity properties.
More concisely: Given a normal space `X`, a closed subset `S` of `X`, and a bounded continuous real-valued function `f` on `S`, there exists a bounded continuous extension `g` of `f` to all of `X`.
|
ContinuousMap.exists_restrict_eq_of_closed
theorem ContinuousMap.exists_restrict_eq_of_closed :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {s : Set X},
IsClosed s →
∀ {Y : Type v} [inst_2 : TopologicalSpace Y] [inst_3 : TietzeExtension Y] (f : C(↑s, Y)),
∃ g, ContinuousMap.restrict s g = f
This is the Tietze Extension theorem for TietzeExtension spaces, specifically for a closed set. The theorem states that given a closed set `s` in a normal topological space `X₂`, and a continuous function `f` on `s` mapping to a TietzeExtension space `Y`, there exists a continuous function `g : C(X₂, Y)` such that when `g` is restricted to the set `s`, it equals the original function `f`. In simpler terms, we can extend a continuous function defined on a closed subset of a normal topological space to a continuous function on the whole space.
More concisely: Given a closed set in a normal topological space and a continuous function on it to a TietzeExtension space, there exists a continuous extension of that function to the whole space.
|
ContinuousMap.exists_extension_of_closedEmbedding
theorem ContinuousMap.exists_extension_of_closedEmbedding :
∀ {X₁ : Type u₁} [inst : TopologicalSpace X₁] {X : Type u} [inst_1 : TopologicalSpace X] [inst_2 : NormalSpace X]
{e : X₁ → X},
ClosedEmbedding e →
∀ {Y : Type v} [inst_3 : TopologicalSpace Y] [inst_4 : TietzeExtension Y] (f : C(X₁, Y)), ∃ g, ⇑g ∘ e = ⇑f
This is the Tietze Extension Theorem for spaces that support Tietze Extension. Given a closed embedding `e` from a nonempty topological space `X₁` into a normal topological space `X₂`, and a continuous function `f` on `X₁` with values in a `TietzeExtension` space `Y`, the theorem states that there exists a continuous function `g` from `X₂` to `Y` such that `g` composed with `e` equals `f`. In other words, `g` extends `f` from `X₁` to `X₂`. This version of the theorem is provided for convenience and backwards compatibility, phrasing the composition in terms of bare functions.
More concisely: Given a normal space X₂, a closed subspace X₁ of X₂ with a continuous function f: X₁ → Y from X₁ to a Tietze extension space Y, there exists a continuous function g: X₂ → Y such that f = g ∘ e, where e is the inclusion map of X₁ into X₂.
|
BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding
theorem BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y]
[inst_3 : Nonempty X] (f : BoundedContinuousFunction X ℝ) {e : X → Y},
ClosedEmbedding e → ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Set.Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
The **Tietze extension theorem** for real-valued bounded continuous maps states that for a given a nonempty topological space `X` embedded into a normal topological space `Y` through a closed embedding `e`, and a bounded continuous real-valued function `f` on `X`, there exists a bounded continuous function `g : Y →ᵇ ℝ` such that `g ∘ e = f`. Moreover, each value of `g` lies in a closed interval `[f x₁, f x₂]` for some `x₁` and `x₂` in `X`. This theorem allows us to extend a continuous function defined on a closed subset to a continuous function on the whole space.
More concisely: Given a nonempty subspace X of a normal topological space Y, and a bounded continuous real-valued function f on X, there exists a bounded continuous extension g of f to all of Y, such that each value of g lies in the closure of the range of f.
|
BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed
theorem BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed :
∀ {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : NormalSpace Y] {s : Set Y}
(f : BoundedContinuousFunction ↑s ℝ),
IsClosed s →
∀ {t : Set ℝ} [inst_2 : t.OrdConnected],
(∀ (x : ↑s), f x ∈ t) → t.Nonempty → ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f
This is the Tietze extension theorem for real-valued bounded continuous maps, particularly for a closed set. Given a normal topological space `Y` and a closed set `s` within this space, suppose we have a bounded continuous real-valued function `f` on set `s`. Now, let `t` be a nonempty convex set of real numbers such that all function values `f x` for `x` in `s` belong to `t`. This theorem asserts that there exists a bounded continuous real-valued function `g` on `Y` such that all its values `g y` belong to `t` and the restriction of `g` to `s` equals `f`.
More concisely: Given a normal topological space `Y`, a closed set `s` in `Y`, a bounded continuous real-valued function `f` on `s`, and a nonempty convex set `t` of real numbers containing all values of `f` on `s`, there exists a bounded continuous real-valued function `g` on `Y` such that `g|s = f` and `g(Y) ⊆ t`.
|