update_inr_comp_inr — Mathlib

English

The composition of the updated function with inr equals updating the composed function on inr: (update f (inr i) x) ∘ inr = update (f ∘ inr) i x.

Русский

Компоновка обновлённой функции с inr равна обновлению композитной функции на inr: (update f (inr i) x) ∘ inr = update (f ∘ inr) i x.

LaTeX

$$$$ (\\operatorname{update} f (\\mathrm{inr} i)\\; x) \\circ \\mathrm{inr} = \\operatorname{update}(f \\circ \\mathrm{inr}) i\\; x. $$$$

Lean4

@[simp]
theorem update_inr_comp_inr [DecidableEq β] [DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ} :
    update f (inr i) x ∘ inr = update (f ∘ inr) i x :=
  update_comp_eq_of_injective _ inr_injective _ _

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