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_restrict_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] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E] [CompleteSpace 𝕜] [TietzeExtension 𝕜] : TietzeExtension E

instance Complex.instTietzeExtension : TietzeExtension ℂ

Equations

• Complex.instTietzeExtension = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Metric.instTietzeExtensionBall {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {r : ℝ} (hr : 0 < r) : TietzeExtension ↑(Metric.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 ↑(Metric.closedBall y 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.