update_inr_comp_inl — Mathlib

English

For any f : α ⊕ β → γ and i : β and x : γ, updating f at inr i by x does not affect its restriction to the left copy, i.e. (update f (inr i) x) ∘ inl = f ∘ inl.

Русский

Для любой функции f: α ⊕ β → γ и элемента i из β, обновление f по right-ветви не влияет на отображение левой части: (update f (inr i) x) ∘ inl = f ∘ inl.

LaTeX

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

Lean4

@[simp]
theorem update_inr_comp_inl [DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ} :
    update f (inr i) x ∘ inl = f ∘ inl :=
  (update_comp_eq_of_forall_ne _ _) fun _ ↦ inl_ne_inr

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