count_bind — Mathlib

English

count_bind [DecidableEq α] : count a (bind m f) = sum (m.map (count a ∘ f)).

Русский

count_bind: подсчёт по связыванию: count a (bind m f) = sum (m.map (count a ∘ f)).

LaTeX

$$$\\mathrm{count}\\ a (\\mathrm{bind}\\ m f) = \\mathrm{sum}(m.map (\\mathrm{count}\\ a \\circ f))$$$

Lean4

theorem count_bind [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} :
    count a (bind m f) = sum (m.map fun b => count a <| f b) :=
  count_sum

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