mathlib3

f77d5d6f - feat(data/finset): add lemma for empty filter (#4188)

feat(data/finset): add lemma for empty filter (#4188) A little lemma, analogous to `filter_true_of_mem` to make it convenient to reduce a filter which always fails.