English
For a fixed c in M, function f with values in α, and i in ι with x in αi, updating the i-th value after scaling equals scaling the update: update (c • f) i (c • x) = c • update f i x.
Русский
Пусть f: ι → α, c∈M, i∈ι, x∈α_i. Тогда обновление в точке i после масштабирования на c эквивалентно масштабированию обновления: update (c•f) i (c•x) = c•update f i x.
LaTeX
$$$\text{update}(c\cdot f)\, i\, (c\cdot x) = c\cdot\text{update}\, f\, i\, x.$$$
Lean4
@[to_additive]
theorem update_smul [∀ i, SMul M (α i)] [DecidableEq ι] (c : M) (f₁ : ∀ i, α i) (i : ι) (x₁ : α i) :
update (c • f₁) i (c • x₁) = c • update f₁ i x₁ :=
funext fun j => (apply_update (β := α) (fun _ ↦ (c • ·)) f₁ i x₁ j).symm
