English
Under an injectivity condition on f over the support of s, for each x∈s, count of f x in map f s equals count of x in s.
Русский
При условии инъективности f на поддержке s для каждого x∈s выполняется: count (f x) (map f s) = count x s.
LaTeX
$$$f \text{ injective on } \{x : \alpha | x \in s\} \Rightarrow \forall x\in s, \operatorname{count} (f x) (\operatorname{map} f s) = \operatorname{count} x s$$$
Lean4
/-- `Multiset.map f` preserves `count` if `f` is injective on the set of elements contained in
the multiset -/
theorem count_map_eq_count [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Set.InjOn f {x : α | x ∈ s}) (x)
(H : x ∈ s) : (s.map f).count (f x) = s.count x :=
by
suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s)
by
rw [count, countP_map, ← this]
exact count_filter_of_pos <| rfl
· rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
· simp only [count_replicate, if_true, card_replicate]
· simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]
