update_inl_comp_inr — Mathlib

English

Alternative formulation: update f (inl i) x composed with inr equals f composed with inr.

Русский

Альтернативная формулировка: обновление f на inl i, затем применение к inr равно f ∘ inr.

LaTeX

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

Lean4

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

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