whiskerLeft_comp

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp

English

Left whiskering distributes over composition: ψ ◁ (θ ≫ θ') = (ψ ◁ θ) ≫ (ψ ◁ θ').

Русский

Левый whisker распространяется на композицию: ψ ◁ (θ ≫ θ') = (ψ ◁ θ) ≫ (ψ ◁ θ').

LaTeX

$$$ ψ \triangleleft (θ \circ θ') = (ψ \triangleleft θ) \circ (ψ \triangleleft θ') $$$

Lean4

@[simp, reassoc]
theorem whiskerLeft_comp : ψ ◁ (θ ≫ θ') = (ψ ◁ θ) ≫ (ψ ◁ θ') := by cat_disch

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru