update_inl_apply_inr — Mathlib

English

Let f be a function on the disjoint sum α ⊕ β. If we replace its value at inl i by x, then evaluating the new function at any inr j yields the original value f(inr j).

Русский

Пусть f — функция на дизъюнктивной сумме α ⊕ β. Если заменить значение в точке inl(i) на x, то при применении к inr(j) новая функция даёт прежнее значение f(inr(j)).

LaTeX

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

Lean4

theorem update_inl_apply_inr [DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
    update f (inl i) x (inr j) = f (inr j) :=
  Function.update_of_ne inr_ne_inl ..

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