English
For f : α ⊕ β → γ and i ∈ β, x ∈ γ, the value of (update f (inr i) x) on inr j equals the value of (update (f ∘ inr) i x) on inr j, i.e. (update f (inr i) x)(inr j) = (update (f ∘ inr) i x)(inr j).
Русский
Для f: α ⊕ β → γ и i, j ∈ β, x ∈ γ, значение (update f (inr i) x) на inr j равно значению обновлённой функции на inr j.
LaTeX
$$$$ (\\operatorname{update} f (\\mathrm{inr} i)\\; x)(\\mathrm{inr} j) = (\\operatorname{update}(f \\circ \\mathrm{inr}) i\\; x)(\\mathrm{inr} j). $$$$
Lean4
@[simp]
theorem update_inr_apply_inr [DecidableEq β] [DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i j : β} {x : γ} :
update f (inr i) x (inr j) = update (f ∘ inr) i x j := by rw [← update_inr_comp_inr, Function.comp_apply]
