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 𝕜]
:
@[instance 900]
instance
RCLike.instTietzeExtensionTVS
{𝕜 : Type v}
[RCLike 𝕜]
{E : Type w}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[T2Space E]
[FiniteDimensional 𝕜 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 ↑(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)
:
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.