Commit 2022-02-18 07:37 77f264f1
View on Github →feat(data/finset/basic): add lemma filter_eq_empty_iff (#12104)
Add filter_eq_empty_iff : (s.filter p = ∅) ↔ ∀ x ∈ s, ¬ p x
We already have the right-to-left direction of this in filter_false_of_mem.