English
Dually, updating the right branch in a sum-recursion is equivalent to updating the recursion on the right branch: Sum.rec f (update g b x) = update (Sum.rec f g) (inr b) x.
Русский
Аналогично обновление правой ветви в рекурсивном определении суммы эквивалентно обновлению рекурсии справа: Sum.rec f (update g b x) = update (Sum.rec f g) (inr b) x.
LaTeX
$$$$ \\operatorname{Sum.rec} f (\\operatorname{update} g b x) = \\operatorname{update}(\\operatorname{Sum.rec} f g) (\\mathrm{inr} b) x. $$$$
Lean4
@[simp]
theorem rec_update_right {γ : α ⊕ β → Sort*} [DecidableEq α] [DecidableEq β] (f : ∀ a, γ (.inl a)) (g : ∀ b, γ (.inr b))
(b : β) (x : γ (.inr b)) : Sum.rec f (update g b x) = update (Sum.rec f g) (.inr b) x :=
Function.rec_update Sum.inr_injective (Sum.rec f) (fun _ _ => rfl)
(fun
| _, _, .inr _, h => (h _ rfl).elim
| _, _, .inl _, _ => rfl)
_ _ _
