English
Let f: M → N with f(0) = 0 and, for a fixed c ∈ R, v ∈ α →₀ M, and hsmul: ∀ x, f(c · x) = c · f(x). Then mapRange f hf (c · v) = c · mapRange f hf v.
Русский
Пусть f: M → N удовлетворяет f(0) = 0 и для фиксированного c ∈ R верно f(c · x) = c · f(x) для всех x; тогда mapRange f hf (c · v) = c · mapRange f hf v.
LaTeX
$$$$\\forall f hf \\colon f(0)=0,\\; c\\in R,\\; v\\in \\alpha \\to_0 M,\\; (\\forall x,\\ f(c\\cdot x)=c\\cdot f(x)) \\Rightarrow \\operatorname{mapRange}(f, hf)(c\\cdot v)=c\\cdot \\operatorname{mapRange}(f, hf)(v).$$$$
Lean4
theorem mapRange_smul [Zero M] [SMulZeroClass R M] [Zero N] [SMulZeroClass R N] {f : M → N} {hf : f 0 = 0} (c : R)
(v : α →₀ M) (hsmul : ∀ x, f (c • x) = c • f x) : mapRange f hf (c • v) = c • mapRange f hf v :=
mapRange_smul' c c v hsmul
