English
A two-argument version of the update lemma: f j (update g i v j) (update h i w j) equals update of f by i with the value f i v w.
Русский
Две версии априорного обновления: $f j (update g i v j) (update h i w j)$ равняется обновлению $f$ по $i$ с значением $f i v w$.
LaTeX
$$$f j (update g i v j) (update h i w j) = update (\\lambda k \\mapsto f k (g k) (h k)) i (f i v w) j$$
Lean4
theorem apply_update₂ {ι : Sort*} [DecidableEq ι] {α β γ : ι → Sort*} (f : ∀ i, α i → β i → γ i) (g : ∀ i, α i)
(h : ∀ i, β i) (i : ι) (v : α i) (w : β i) (j : ι) :
f j (update g i v j) (update h i w j) = update (fun k ↦ f k (g k) (h k)) i (f i v w) j :=
by
by_cases h : j = i
· subst j
simp
· simp [h]
