English
Let s be a finite set and p, q predicates. Then filtering by p ∧ ¬q equals the difference between filtering by p and filtering by q: s.filter (fun a => p a ∧ ¬ q a) = s.filter p \\ s.filter q.
Русский
Пусть s — конечное множество, а p, q — предикаты. Тогда фильтрация по p ∧ ¬q равна разности фильтрации по p и по q: s.filter (p ∧ ¬q) = s.filter p \\ s.filter q.
LaTeX
$$$\\operatorname{filter} (\\lambda a. p a \\wedge \\neg q a)\\, s = \\operatorname{filter} p\\, s \\setminus \\operatorname{filter} q\\, s$$
Lean4
theorem filter_and_not (s : Finset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
s.filter (fun a ↦ p a ∧ ¬q a) = s.filter p \ s.filter q := by grind
