Documentation

Mathlib.Topology.Instances.RealVectorSpace

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 map_real_smul {E : Type u_1} [AddCommGroup E] [Module E] [TopologicalSpace E] [ContinuousSMul E] {F : Type u_2} [AddCommGroup F] [Module F] [TopologicalSpace F] [ContinuousSMul F] [T2Space F] {G : Type u_3} [FunLike G E F] [AddMonoidHomClass 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
  • f.toRealLinearMap hf = { toFun := f, map_add' := , map_smul' := , cont := hf }
Instances For
    @[simp]
    theorem AddMonoidHom.coe_toRealLinearMap {E : Type u_1} [AddCommGroup E] [Module E] [TopologicalSpace E] [ContinuousSMul E] {F : Type u_2} [AddCommGroup F] [Module F] [TopologicalSpace F] [ContinuousSMul F] [T2Space F] (f : E →+ F) (hf : Continuous f) :
    (f.toRealLinearMap hf) = f
    def AddEquiv.toRealLinearEquiv {E : Type u_1} [AddCommGroup E] [Module E] [TopologicalSpace E] [ContinuousSMul E] {F : Type u_2} [AddCommGroup F] [Module F] [TopologicalSpace F] [ContinuousSMul F] [T2Space F] (e : E ≃+ F) (h₁ : Continuous e) (h₂ : Continuous e.symm) :

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

    Equations
    • e.toRealLinearEquiv h₁ h₂ = { toFun := e.toFun, map_add' := , map_smul' := , invFun := e.invFun, left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
    Instances For
      @[instance 900]

      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.

      Equations
      • =