TietzeExtension.of_tvs

theorem TietzeExtension.of_tvs : ∀ (𝕜 : Type v) [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousSMul 𝕜 E] [inst_6 : T2Space E] [inst_7 : FiniteDimensional 𝕜 E] [inst_8 : CompleteSpace 𝕜] [inst : TietzeExtension 𝕜], TietzeExtension E

This theorem, called TietzeExtension.of_tvs, states that for any type '𝕜' where '𝕜' is a nontrivially normed field, given a type 'E' with the properties of being an additive commutative group, a '𝕜'-module, a topological space, a topological additive group, has continuous scalar multiplication with '𝕜', is T2 (has the Hausdorff property), is finite dimensional over '𝕜', and '𝕜' is a complete space, then 'E' has the property of the Tietze Extension. The Tietze Extension property is a concept from topology and functional analysis that concerns the extension of bounded real-valued functions defined on a subset of a topological space to the whole space.

More concisely: Given a nontrivially normed field '𝕜' and a topological space 'E' that is a finite-dimensional '𝕜'-module, additive commutative group, topological additive group, has continuous scalar multiplication, is T2, and '𝕜' is complete, then every bounded real-valued function on a dense subset of 'E' can be extended to a continuous real-valued function on all of 'E'.