whisker_exchange — Mathlib

English

For W, X, Y, Z, with f: W → X and g: Y → Z, the mixed whiskering satisfies W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g.

Русский

Для W, X, Y, Z, f: W → X, g: Y → Z, смешанная обёртка удовлетворяет W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g.

LaTeX

$$$ W \\triangleleft g \\; \\circ \\; f \\triangleleft Z = f \\triangleleft Y \\circ X \\triangleleft g $$$

Lean4

@[reassoc]
theorem whisker_exchange {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g := by
  simp [← id_tensorHom, ← tensorHom_id]

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