mapWhiskerLeft_comp — Mathlib

English

Whiskering respects composition on the left: mapWhiskerLeft H (α ≫ β) = mapWhiskerLeft H α ≫ mapWhiskerLeft H β.

Русский

Ослабление слева уважает композицию: mapWhiskerLeft H (α ≫ β) = mapWhiskerLeft H α ≫ mapWhiskerLeft H β.

LaTeX

$$$ mapWhiskerLeft H (α \;\; β) = mapWhiskerLeft H α \;\circ\; mapWhiskerLeft H β $$$

Lean4

@[simp]
theorem mapWhiskerLeft_comp {Fᵣ : D ⥤ E'} {Gᵣ : D ⥤ E'} {Hᵣ : D ⥤ E'} (H : C ⥤ E) (α : Fᵣ ⟶ Gᵣ) (β : Gᵣ ⟶ Hᵣ) :
    mapWhiskerLeft H (α ≫ β) = mapWhiskerLeft H α ≫ mapWhiskerLeft H β := by cat_disch

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