update_inr_apply_inl — Mathlib

English

For any f : α ⊕ β → γ, i : β and x : γ, applying the updated function (update f (inr i) x) to a left input inl i yields the original value on the left input: (update f (inr i) x) (inl i) = f (inl i).

Русский

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

LaTeX

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

Lean4

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

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