elim_update_left — Mathlib

English

Let f and g be functions with DecidableEq domains. Then Sum.elim (update f a x) g = update (Sum.elim f g) (inl a) x.

Русский

Пусть f и g заданы на соответствующих доменах; тогда Sum.elim (update f a x) g = update (Sum.elim f g) (inl a) x.

LaTeX

$$$$ \\mathrm{Sum.elim} (\\operatorname{update} f a x)\\; g = \\operatorname{update}(\\mathrm{Sum.elim} f g)\\; (\\mathrm{inl} a)\\; x. $$$$

Lean4

@[simp]
theorem elim_update_left {γ : Sort*} [DecidableEq α] [DecidableEq β] (f : α → γ) (g : β → γ) (a : α) (x : γ) :
    Sum.elim (update f a x) g = update (Sum.elim f g) (.inl a) x :=
  rec_update_left _ _ _ _

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