sum_sym2_filter_not_isDiag — Mathlib

English

Let s be a Finset of a totally ordered type and p: Sym2 ι → M. Then sum over non-diagonal elements of s.sym2 equals the sum over i<j with i,j in s of p(i,j).

Русский

Пусть s — конечное подмножество типа с полной порядком, и p: Sym2 ι → M. Тогда сумма по не диагональным элементам s.sym2 равна сумме по i<j, где i,j принадлежат s, p(i,j).

LaTeX

$$$$ \sum_{i \in s.\mathrm{sym}^2} p(i) \;\text{где } \neg i.\mathrm{IsDiag} = \sum_{i

Lean4

theorem sum_sym2_filter_not_isDiag {ι M} [LinearOrder ι] [AddCommMonoid M] (s : Finset ι) (p : Sym2 ι → M) :
    ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2) :=
  by
  rw [Finset.offDiag_filter_lt_eq_filter_le]
  conv_rhs => rw [← Finset.sum_subtype_eq_sum_filter]
  refine (Finset.sum_equiv Sym2.sortEquiv.symm ?_ ?_).symm
  all_goals aesop

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