exchange — Mathlib

English

The interchange law for whiskering: whiskering distributes over vertical composition: (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ).

Русский

Закон обмена для горизонтальных зашивок: зашивка распределяется над вертикальной композицией: (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ (β ◫ δ).

LaTeX

$$$ (\alpha \circ \beta) \; ◫ \; (\gamma \circ \delta) = (\alpha \; ◫ \; \gamma) \circ (\beta \; ◫ \; \delta). $$$

Lean4

theorem exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :
    (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ := by cat_disch

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