app_sum — Mathlib

English

The app maps commute with finite sums of natural transformations componentwise.

Русский

Применение к сумме преобразований согласуется по компонентам.

LaTeX

$$$$\\text{app_sum}: (\\sum_i \\alpha_i).\\text{app } X = \\sum_i (\\alpha_i.\\text{app } X).$$$$

Lean4

@[simp]
theorem app_sum {ι : Type*} (s : Finset ι) (X : C) (α : ι → (F ⟶ G)) : (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X := by
  simp only [← appHom_apply, map_sum]

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