mathlib

77f264f1 - feat(data/finset/basic): add lemma `filter_eq_empty_iff` (#12104)

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`.