associator_inv_fst_snd — Mathlib

English

The inverse associator composed with fst then snd equals snd then fst.

Русский

Обратное ассоциатора, составленное через fst затем через snd, равно snd затем fst.

LaTeX

$$(α_X Y Z).inv ≫ fst _ _ ≫ snd _ _ = snd _ _ ≫ fst _ _$$

Lean4

@[reassoc (attr := simp)]
theorem associator_inv_fst_snd (X Y Z : C) : (α_ X Y Z).inv ≫ fst _ _ ≫ snd _ _ = snd _ _ ≫ fst _ _ := by
  simp [fst_def, ← whiskerLeft_rightUnitor_assoc, -whiskerLeft_rightUnitor]

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