unop_sum — Mathlib

English

The unop functor preserves finite sums: the unop of a finite sum equals the sum of the unops.

Русский

Функтор разворота сохраняет конечные суммы: разворот суммы равен сумме разворотов.

LaTeX

$$$ (s.\\,sum\\, f)^{\\mathrm{unop}} = \\sum_{i\\in s} (f(i))^{\\mathrm{unop}} $$$

Lean4

@[simp]
theorem unop_sum (X Y : Cᵒᵖ) {ι : Type*} (s : Finset ι) (f : ι → (X ⟶ Y)) :
    (s.sum f).unop = s.sum fun i => (f i).unop :=
  map_sum (unopHom X Y) _ _

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