English
Let f be a continuous multilinear map in the variables indexed by ι. Then for any i ∈ ι, any function m: ι → M₁ i, any scalar c ∈ R, and any x ∈ M₁ i, we have f(update(m, i, c·x)) = c·f(update(m, i, x)).
Русский
Пусть f — непрерывная многочередная отображение от набора переменных, пронумерованных индексами ι. Тогда для любого i ∈ ι, любой m: ι → M₁ i, любого скаляра c ∈ R и любого вектора x ∈ M₁ i выполняется равенство f(update(m, i, c·x)) = c·f(update(m, i, x)).
LaTeX
$$$\\forall i, \\forall m: \\prod_{j \\in ι} M_{1}(j), \\forall c \\in R, \\forall x \\in M_{1}(i), \\\\ f(\\text{update}(m,i,c\\cdot x)) = c\\cdot f(\\text{update}(m,i,x)).$$$
Lean4
@[simp]
theorem map_update_smul [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (update m i (c • x)) = c • f (update m i x) :=
f.map_update_smul' m i c x
