sum_count_of_mem_sym — Mathlib

English

Let α be a type with decidable equality and m ∈ ℕ. For k ∈ Sym α m and s: Finset α with hk ∈ s.sym m, ∑_{i∈s} count i k = m.

Русский

Пусть α — множество с разрешимой эквивалентностью, m ∈ ℕ. Для k ∈ Sym α m и s: Finset α, если hk: k ∈ s.sym m, то сумма по i∈s count i k равна m.

LaTeX

$$$$ \sum_{i\in s} \operatorname{count}(i, k) = m. $$$$

Lean4

theorem sum_count_of_mem_sym {α} [DecidableEq α] {m : ℕ} {k : Sym α m} {s : Finset α} (hk : k ∈ s.sym m) :
    (∑ i ∈ s, count i k) = m := by simp_all

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