Finite-dimensional topological vector spaces over ℝ satisfy the Tietze extension property

There are two main results here:

• RCLike.instTietzeExtensionTVS: finite-dimensional topological vector spaces over ℝ (or ℂ) have the Tietze extension property.
• BoundedContinuousFunction.exists_norm_eq_domRestrict_eq: when mapping into a finite-dimensional normed vector space over ℝ (or ℂ), the extension can be chosen to preserve the norm of the bounded continuous function it extends.

theorem TietzeExtension.of_tvs (𝕜 : Type v) [NontriviallyNormedField 𝕜] {E : Type w} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E] [CompleteSpace 𝕜] [TietzeExtension 𝕜] : TietzeExtension E

instance Complex.instTietzeExtension : TietzeExtension ℂ

@[instance 900]

instance RCLike.instTietzeExtension {𝕜 : Type u_1} [RCLike 𝕜] : TietzeExtension 𝕜

instance RCLike.instTietzeExtensionTVS {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E] : TietzeExtension E

instance Set.instTietzeExtensionUnitBall {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : TietzeExtension ↑(Metric.ball 0 1)

instance Set.instTietzeExtensionUnitClosedBall {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : TietzeExtension ↑(Metric.closedBall 0 1)

theorem Metric.instTietzeExtensionBall {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {r : ℝ} (hr : 0 < r) : TietzeExtension ↑(ball 0 r)

theorem Metric.instTietzeExtensionClosedBall (𝕜 : Type v) [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (y : E) {r : ℝ} (hr : 0 < r) : TietzeExtension ↑(closedBall y r)

instance unitInterval.instTietzeExtension : TietzeExtension ↑unitInterval

theorem BoundedContinuousFunction.exists_norm_eq_domRestrict_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.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.

@[deprecated BoundedContinuousFunction.exists_norm_eq_domRestrict_eq (since := "2026-07-19")]

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.domRestrict s = f

Alias of BoundedContinuousFunction.exists_norm_eq_domRestrict_eq.

---

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.