English
Let f: M → N with f(0) = 0, and v ∈ α →₀ M be a finitely supported M-valued function. If there are c ∈ R and d ∈ S such that f(c · x) = d · f(x) for every x ∈ M, then mapRange f hf (c · v) = d · mapRange f hf v.
Русский
Пусть f: M → N удовлетворяет f(0) = 0, и v ∈ α →₀ M — конечно-поддерживающая функция. Если существуют c ∈ R и d ∈ S такие, что ∀ x ∈ M выполняется f(c · x) = d · f(x), то mapRange f hf (c · v) = d · mapRange f hf v.
LaTeX
$$$$\\forall f hf \\colon f(0)=0,\\; c\\in R,\\; d\\in S,\\; v\\in \\alpha \\to_0 M,\\; (\\forall x,\\ f(c\\cdot x)=d\\cdot f(x)) \\Rightarrow \\operatorname{mapRange}(f, hf)(c\\cdot v)=d\\cdot \\operatorname{mapRange}(f, hf)(v).$$$$
Lean4
theorem mapRange_smul' [Zero M] [SMulZeroClass R M] [Zero N] [SMulZeroClass S N] {f : M → N} {hf : f 0 = 0} (c : R)
(d : S) (v : α →₀ M) (hsmul : ∀ x, f (c • x) = d • f x) : mapRange f hf (c • v) = d • mapRange f hf v :=
by
ext
simp [hsmul]
