Documentation

Mathlib.Analysis.Complex.Tietze

Finite dimensional topological vector spaces over satisfy the Tietze extension property #

There are two main results here:

@[instance 900]
instance RCLike.instTietzeExtension {𝕜 : Type u_1} [RCLike 𝕜] :
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
theorem Metric.instTietzeExtensionBall {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {r : } (hr : 0 < r) :
theorem Metric.instTietzeExtensionClosedBall (𝕜 : Type v) [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (y : E) {r : } (hr : 0 < r) :
theorem BoundedContinuousFunction.exists_norm_eq_restrict_eq {X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) (𝕜 : Type v) [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : BoundedContinuousFunction (↑s) E) :
∃ (g : BoundedContinuousFunction X E), g = f g.restrict s = 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.