English
A continuous additive map between real vector spaces is ℝ-linear.
Русский
Непрерывное аддитивное отображение между вещественными векторами линейно по отношению к ℝ.
LaTeX
$$$f: G \to F$ непрерывно, $G,F$ — вещественные векторные пространства, тогда $f(c\cdot x) = c\cdot f(x)$$$
Lean4
/-- A continuous additive map between two vector spaces over `ℝ` is `ℝ`-linear. -/
theorem map_real_smul {G} [FunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf : Continuous f) (c : ℝ) (x : E) :
f (c • x) = c • f x :=
suffices (fun c : ℝ => f (c • x)) = fun c : ℝ => c • f x from congr_fun this c
Rat.isDenseEmbedding_coe_real.dense.equalizer (hf.comp <| continuous_id.smul continuous_const)
(continuous_id.smul continuous_const) (funext fun r => map_ratCast_smul f ℝ ℝ r x)
