inverseAssociator_map_inr_inr — Mathlib

English

For f: X → Y in E, the inverse associator maps inr to inr: (inr f) ↦ inr f.

Русский

Для f: X → Y в E отображение inr сохраняется: inr f ↦ inr f.

LaTeX

$$(\operatorname{inverseAssociator}_{C,D,E}).map((\mathrm{inr}_{C}(\mathrm{Sum} D E)).map((\mathrm{inr}_{D E}).map f)) = (\mathrm{inr}_{(Sum C D)} E).map(f)$$

Lean4

@[simp]
theorem inverseAssociator_map_inr_inr {X Y : E} (f : X ⟶ Y) :
    (inverseAssociator C D E).map ((inr_ _ _).map ((inr_ _ _).map f)) = (inr_ _ _).map f :=
  rfl

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