sum_comp' — Mathlib

English

Associativity of composing sums: (∑_{j∈s} f_j ≫ g_j) ≫ h = ∑_{j∈s} f_j ≫ g_j ≫ h.

Русский

Ассоциативность композиции с суммами: (∑_{j∈s} f_j ≫ g_j) ≫ h = ∑_{j∈s} f_j ≫ g_j ≫ h.

LaTeX

$$$ \left( \sum_{j \in s} f_j \circ g_j \right) \circ h = \sum_{j \in s} (f_j \circ g_j \circ h) $$$

Lean4

@[reassoc]
theorem sum_comp' {P Q R S : C} {J : Type*} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R)) (h : R ⟶ S) :
    (∑ j ∈ s, f j ≫ g j) ≫ h = ∑ j ∈ s, f j ≫ g j ≫ h :=
  by
  simp only [← Category.assoc]
  apply sum_comp

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