op_sum — Mathlib

English

The opposite of a sum equals the sum of opposites: (s.sum f).op = s.sum (f(i).op).

Русский

Равенство противоположности суммы и суммы противоположностей: (s.sum f).op = s.sum (f(i).op).

LaTeX

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

Lean4

@[simp]
theorem op_sum (X Y : C) {ι : Type*} (s : Finset ι) (f : ι → (X ⟶ Y)) : (s.sum f).op = s.sum fun i => (f i).op :=
  map_sum (opHom X Y) _ _

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