map_real_smul

theorem map_real_smul : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousSMul ℝ E] {F : Type u_2} [inst_4 : AddCommGroup F] [inst_5 : Module ℝ F] [inst_6 : TopologicalSpace F] [inst_7 : ContinuousSMul ℝ F] [inst_8 : T2Space F] {G : Type u_3} [inst_9 : FunLike G E F] [inst_10 : AddMonoidHomClass G E F] (f : G), Continuous ⇑f → ∀ (c : ℝ) (x : E), f (c • x) = c • f x

This theorem states that, for any continuous additive map `f` between two real vector spaces `E` and `F`, the map obeys the property of real-linearity. More specifically, if `E` and `F` are both real vector spaces that are equipped with a topology and have a continuous scalar multiplication operation, and `f` is a function from `E` to `F` that behaves like a function (according to the `FunLike` type class) and also behaves like an additive monoid homomorphism (according to the `AddMonoidHomClass` type class), then if `f` is continuous, it will map scalar multiplication in `E` to scalar multiplication in `F`. In more mathematical terms, for all real numbers `c` and all elements `x` of `E`, `f` applied to `c` times `x` in `E` is the same as `c` times `f` applied to `x` in `F`.

More concisely: If `f` is a continuous, additive map between real vector spaces `E` and `F` that respects scalar multiplication, then for all real numbers `c` and elements `x` of `E`, `f(cx) = c(f(x))`.