Theorems · Theorem · general topology

BoundedContinuousFunction.exists_norm_eq_domRestrict_eq

∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X},
  IsClosed s →
    ∀ (𝕜 : Type v) [inst_2 : RCLike 𝕜] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
      [FiniteDimensional 𝕜 E] (f : BoundedContinuousFunction (↑s) E), ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict 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.

Defined in

Mathlib.Analysis.Complex.Tietze

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceRCLikeNormedAddCommGroupNormedSpaceFiniteDimensional