English
Let β be a type with decidable equality, s a Finset α, f : α → Multiset β, and b ∈ β. Then the count of b in s.sup f equals the supremum over a ∈ α of the counts of b in f(a): count b (s.sup f) = s.sup (λ a, count b (f a)).
Русский
Пусть β имеет разрешимое равенство, s ⊆ α конечно, f : α → Multiset β, b ∈ β. Тогда количество элемента b в s.sup f равно максимальному количеству b в множествах f( a ) по a ∈ α.
LaTeX
$$$\\operatorname{count}_b( s.\\mathrm{sup}\\ f) = s.\\mathrm{sup}\\ (\\lambda a. \\operatorname{count}_b( f(a) )).$$$
Lean4
theorem count_finset_sup [DecidableEq β] (s : Finset α) (f : α → Multiset β) (b : β) :
count b (s.sup f) = s.sup fun a => count b (f a) :=
by
letI := Classical.decEq α
refine s.induction ?_ ?_
· exact count_zero _
· intro i s _ ih
rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
