Filtering a finite sum of multisets

Filtering a multiset is additive, so it distributes over a finite sum of multisets. Mathlib records the binary case as Multiset.filter_add; this file records the finite-sum case, used to recover the part of a concatenated unordered tuple lying in a given set from the parts of its summands.

@[simp]

theorem Multiset.filter_sum {α : Type u_1} {ι : Type u_2} (p : α → Prop) [DecidablePred p] (s : Finset ι) (f : ι → Multiset α) : filter p (∑ i ∈ s, f i) = ∑ i ∈ s, filter p (f i)

Filtering distributes over a finite sum of multisets.