sum_comp — Mathlib

English

Composition distributes over sums on the left: (∑_{j∈s} f_j) ≫ g = ∑_{j∈s} (f_j ≫ g).

Русский

Композиция распределяется по сумме слева: (∑_{j∈s} f_j) ∘ g = ∑_{j∈s} (f_j ∘ g).

LaTeX

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

Lean4

@[reassoc]
theorem sum_comp {P Q R : C} {J : Type*} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R) :
    (∑ j ∈ s, f j) ≫ g = ∑ j ∈ s, f j ≫ g :=
  map_sum (rightComp P g) _ _

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