English
Let p be a predicate, a an element, and S a finite set. Then filtering after inserting a is: if p(a) then insert a (filter p S) else filter p S.
Русский
Пусть p — предикат, a — элемент, S — конечное множество. Тогда фильтрация после вставки a равна: если p(a), то вставить a в фильтрованное множество, иначе просто фильтрованное множество.
LaTeX
$$$\\operatorname{filter}_p(\\operatorname{insert} a\\, S) = \\begin{cases} \\operatorname{insert} a\\, (\\operatorname{filter}_p S) & p(a) \\\\ \\operatorname{filter}_p S & \\neg p(a) \\end{cases}$$$
Lean4
theorem filter_insert (a : α) (s : Finset α) :
filter p (insert a s) = if p a then insert a (filter p s) else filter p s := by grind
