English
A general distributive law: f j (update g i v j) = update (λk, f k (g k)) i (f i v) j for suitable f, g, i, v, j.
Русский
Общее распределительное свойство: $f(j, update g i v j)$ равно обновлению композиции $f k (g k)$ в точке i и аргументе v.
LaTeX
$$$f j (update g i v j) = update (\\lambda k \\mapsto f k (g k)) i (f i v) j$$
Lean4
theorem apply_update {ι : Sort*} [DecidableEq ι] {α β : ι → Sort*} (f : ∀ i, α i → β i) (g : ∀ i, α i) (i : ι) (v : α i)
(j : ι) : f j (update g i v j) = update (fun k ↦ f k (g k)) i (f i v) j :=
by
by_cases h : j = i
· subst j
simp
· simp [h]