English
Let E and F be real vector spaces equipped with compatible topologies making them real topological vector spaces. If f: E →+ F is a continuous additive group homomorphism, then there exists a continuous ℝ-linear map f̂: E → F whose underlying function equals f.
Русский
Пусть E и F — вещественные векторные пространства с совместимыми топологиями, делающими их вещественными топологическими векторами. Если f: E →+ F непрерывен как аддитивный гомоморфизм группы, то существует непрерывное линейное отображение над ℝ, f̂: E → F, чья функция-образ равна f.
LaTeX
$$$\\exists! \\, T: E \\to F \\text{ such that } T \\text{ is } \\mathbb{R}\\text{-linear},\\ T \\text{ is continuous},\\ T(x)=f(x) \\text{ for all } x \\in E.$$$
Lean4
/-- Reinterpret a continuous additive homomorphism between two real vector spaces
as a continuous real-linear map. -/
def toRealLinearMap (f : E →+ F) (hf : Continuous f) : E →L[ℝ] F :=
⟨{ toFun := f
map_add' := f.map_add
map_smul' := map_real_smul f hf }, hf⟩
