mathlib3 documentation

topology.instances.real_vector_space

Continuous additive maps are -linear #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that a continuous map f : E →+ F between two topological vector spaces over is -linear

theorem map_real_smul {E : Type u_1} [add_comm_group E] [module E] [topological_space E] [has_continuous_smul E] {F : Type u_2} [add_comm_group F] [module F] [topological_space F] [has_continuous_smul F] [t2_space F] {G : Type u_3} [add_monoid_hom_class G E F] (f : G) (hf : continuous f) (c : ) (x : E) :
f (c x) = c f x

A continuous additive map between two vector spaces over is -linear.

Reinterpret a continuous additive homomorphism between two real vector spaces as a continuous real-linear map.

Equations

Reinterpret a continuous additive equivalence between two real vector spaces as a continuous real-linear map.

Equations
@[protected, instance]

A topological group carries at most one structure of a topological -module, so for any topological -algebra A (e.g. A = ℂ) and any topological group that is both a topological -module and a topological A-module, these structures agree.