elim_update_right — Mathlib

English

Similarly, Sum.elim f (update g b x) = update (Sum.elim f g) (inr b) x.

Русский

Аналогично Sum.elim f (update g b x) = update (Sum.elim f g) (inr b) x.

LaTeX

$$$$ \\mathrm{Sum.elim} f (\\operatorname{update} g b x) = \\operatorname{update}(\\mathrm{Sum.elim} f g) (\\mathrm{inr} b) x. $$$$

Lean4

@[simp]
theorem elim_update_right {γ : Sort*} [DecidableEq α] [DecidableEq β] (f : α → γ) (g : β → γ) (b : β) (x : γ) :
    Sum.elim f (update g b x) = update (Sum.elim f g) (.inr b) x :=
  rec_update_right _ _ _ _

Похожие утверждения