count_map — Mathlib

English

The count of a value b in the mapped multiset equals the number of elements in s that map to b under f.

Русский

Счёт b в отображённом мультиете равен числу элементов s, которые отображаются в b под f.

LaTeX

$$$\operatorname{count} b (\operatorname{map} f s) = \operatorname{card} (s.filter (\lambda a. b = f a))$$$

Lean4

theorem count_map {α β : Type*} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) :
    count b (map f s) = card (s.filter fun a => b = f a) := by simp [count, countP_map]

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