count_apply — Mathlib

English

The additive version countP_apply states that the homomorphic image equals the list count: l.countP p = l.toList.countP p.

Русский

Аддитивная версия: значения countP_apply равны числу элементов списка, удовлетворяющих p.

LaTeX

$$$\\operatorname{countP\\,apply}(p, l) = \\operatorname{List.countP}(\\lambda b. \\mathrm{decide}(p\,b), l.\\mathrm{toList})$$$

Lean4

theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
    count x l = Multiplicative.ofAdd (l.toList.count x) :=
  rfl

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