comp_sum — Mathlib

English

Composition distributes over finite sums on the right: for any finite set s, any f : P → Q and g : J → Q → R, we have f ≫ ∑_{j∈s} g_j = ∑_{j∈s} (f ≫ g_j).

Русский

Композиция распределяется по конечной сумме справа: для конечного множества s выполняется f ≫ ∑_{j∈s} g_j = ∑_{j∈s} (f ≫ g_j).

LaTeX

$$$ f \circ \sum_{j \in s} g_j = \sum_{j \in s} (f \circ g_j) $$$

Lean4

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

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