English
Filtering commutes with subtraction: filtering p after subtracting t from s equals subtracting the filtered t from the filtered s.
Русский
Фильтрация допускает вычитание: фильтрация по p после вычитания t из s равна вычитанию фильтрованного t из фильтрованного s.
LaTeX
$$$ \\mathrm{filter} p (s - t) = \\mathrm{filter} p\\, s - \\mathrm{filter} p\\, t $$$
Lean4
@[simp]
theorem filter_sub (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s - t) = filter p s - filter p t :=
by
revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
rw [sub_cons, IH]
by_cases h : p a
· rw [filter_cons_of_pos _ h, sub_cons]
congr
by_cases m : a ∈ s
· rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h), cons_erase m]
· rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]
· rw [filter_cons_of_neg _ h]
by_cases m : a ∈ s
· rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)), cons_erase m]
· rw [erase_of_notMem m]
