update_inl_comp_inl — Mathlib

English

Equality of compositions: (update f (inl i) x) ∘ inl = update (f ∘ inl) i x ∘ inl.

Русский

Равенство композиций: (update f (inl i) x) ∘ inl = update (f ∘ inl) i x ∘ inl.

LaTeX

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

Lean4

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

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