Commit 2020-09-20 23:55 f77d5d6f
View on Github →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.
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.