ιTensorObj₄_eq — Mathlib

English

A naturality-like statement for ιTensorObj3′ with respect to the associator's hom component.

Русский

Натурализованное утверждение для ιTensorObj3′ относительно компонента гомо-ассоциатора.

LaTeX

$$$ιTensorObj_3' X_1 X_2 X_3 i_1 i_2 i_3 j h ≫ (associator X_1 X_2 X_3).hom j = (\alpha_\_\_\_).hom ≫ ιTensorObj_3 X_1 X_2 X_3 i_1 i_2 i_3 j h.$$$

Lean4

theorem ιTensorObj₄_eq (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j) (i₂₃₄ : I) (hi : i₂ + i₃ + i₄ = i₂₃₄) :
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
      (_ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ _ hi) ≫
        ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j (by rw [← hi, ← add_assoc, ← add_assoc, h]) :=
  by
  subst hi
  rfl

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