English
A variant of the previous statement with a Prime equality predicate, expressing the same idea in a different form.
Русский
Вариант предыдущего утверждения с предикатом равенства помеченным как Prime, выражающий ту же идею в другой форме.
LaTeX
$$$\\operatorname{filter} (\\operatorname{Eq} b)\\, s = \\operatorname{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 fun a => a = b) = ite (b ∈ s) { b } ∅ := by grind
