English
For a Finset s and an element b, filtering by equality to b yields either the singleton {b} if b ∈ s, or the empty set otherwise.
Русский
Для конечного множества s и элемента b фильтрация по равенству b дает либо {b}, если b ∈ s, либо пустое множество иначе.
LaTeX
$$$\\operatorname{filter} (\\operatorname{Eq} b)\\, s = \\mathrm{ite} (b \\in s)\\ { b } \\ emptyset$$$
Lean4
/-- After filtering out everything that does not equal a given value, at most that value remains.
This is equivalent to `filter_eq'` with the equality the other way.
-/
theorem filter_eq [DecidableEq β] (s : Finset β) (b : β) : s.filter (Eq b) = ite (b ∈ s) { b } ∅ := by grind
