comp_whiskerRight — Mathlib

English

For morphisms f: W → X and g: X → Y and any Z, the right whiskering distributes over composition: (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z.

Русский

Пусть f: W → X, g: X → Y и Z. Правое обёртывание распределяется по композиции: (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z.

LaTeX

$$$ (f \\circ g) \\triangleleft Z = (f \\triangleleft Z) \\circ (g \\triangleleft Z) $$$

Lean4

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

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