Continuous additive maps are ℝ-linear
In this file we prove that a continuous map f : E →+ F between two topological vector spaces
over ℝ is ℝ-linear
theorem
add_monoid_hom.map_real_smul
{E : Type u_1}
[add_comm_group E]
[vector_space ℝ E]
[topological_space E]
[topological_vector_space ℝ E]
{F : Type u_2}
[add_comm_group F]
[vector_space ℝ F]
[topological_space F]
[topological_vector_space ℝ F]
[t2_space F]
(f : E →+ F)
(hf : continuous ⇑f)
(c : ℝ)
(x : E) :
A continuous additive map between two vector spaces over ℝ is ℝ-linear.
def
add_monoid_hom.to_real_linear_map
{E : Type u_1}
[add_comm_group E]
[vector_space ℝ E]
[topological_space E]
[topological_vector_space ℝ E]
{F : Type u_2}
[add_comm_group F]
[vector_space ℝ F]
[topological_space F]
[topological_vector_space ℝ F]
[t2_space F]
(f : E →+ F) :
continuous ⇑f → (E →L[ℝ] F)
Reinterpret a continuous additive homomorphism between two real vector spaces as a continuous real-linear map.
Equations
- f.to_real_linear_map hf = {to_linear_map := {to_fun := ⇑f, map_add' := _, map_smul' := _}, cont := hf}
@[simp]
theorem
add_monoid_hom.coe_to_real_linear_map
{E : Type u_1}
[add_comm_group E]
[vector_space ℝ E]
[topological_space E]
[topological_vector_space ℝ E]
{F : Type u_2}
[add_comm_group F]
[vector_space ℝ F]
[topological_space F]
[topological_vector_space ℝ F]
[t2_space F]
(f : E →+ F)
(hf : continuous ⇑f) :
⇑(f.to_real_linear_map hf) = ⇑f