English
If predicates p and q agree on every element of a multiset s, then filtering s by p or by q yields the same multiset.
Русский
Если предикаты p и q совпадают на каждом элементе мультисета s, то фильтрация s по p и по q дает одинаковый мультисет.
LaTeX
$$$\\forall p\\,q\\,\\forall s:\\mathcal{M}(\\alpha),\\ (\\forall x\\in s\\,:\\, p x\\iff q x)\\to \\operatorname{filter} p\, s = \\operatorname{filter} q\, s.$$$
Lean4
@[congr]
theorem filter_congr {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Multiset α} :
(∀ x ∈ s, p x ↔ q x) → filter p s = filter q s :=
Quot.inductionOn s fun _l h => congr_arg ofList <| List.filter_congr <| by simpa using h
