tensor_comp — Mathlib

English

Associator naturality in the localized monoidal structure.

Русский

Естественность ассоциатора в локализованной монойдной структуре.

LaTeX

$$$\\forall f_1,f_2,f_3:\\; (f_1 \\otimes f_2) \\otimes f_3 \\to f_1 \\otimes (f_2 \\otimes f_3)$ respects associativity$$

Lean4

@[reassoc]
theorem tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
    (g₂ : Y₂ ⟶ Z₂) : (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) = (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) := by simp [monoidalCategoryStruct]

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