English
Let f be a family of linear maps f_i : M2 → φ_i indexed by i, and let c ∈ M2, i, j ∈ ι and b : M2 →ₗ[R] φ_i. Then the map obtained by updating f at i with b and evaluating at j satisfies (update f i b j) c = update (λ i, f_i c) i (b c) j.
Русский
Пусть f — семейство линейных отображений f_i : M2 → φ_i, индексируемое i по ι, и возьмём c ∈ M2, i, j ∈ ι, а также b : M2 →ₗ[R] φ_i. Тогда отображение, полученное обновлением f в координате i на b и последующим применением к c в координате j, удовлетворяет (update f i b j) c = update (λ i, f_i c) i (b c) j.
LaTeX
$$$$(\\mathrm{update}\\ f\\ i\\ b\\ j)\\;c = \\mathrm{update}\\bigl(\\lambda i. f_i\\,c\\bigr)\\;i\\;(b\\,c)\\;j.$$$$
Lean4
theorem update_apply (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ i) :
(update f i b j) c = update (fun i => f i c) i (b c) j :=
by
by_cases h : j = i
· rw [h, update_self, update_self]
· rw [update_of_ne h, update_of_ne h]
