Theorems · Theorem · general topology

BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding

• 1000+ list: Tietze extension theorem

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) {e : X → Y}, Topology.IsClosedEmbedding e → ∃ g, ‖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.

Defined in

Mathlib.Topology.TietzeExtension

Cited by

2 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceNormalSpace