added lemma

--- a/src/HOL/List.thy	Tue Nov 09 19:47:24 2021 +0100
+++ b/src/HOL/List.thy	Wed Nov 10 08:36:50 2021 +0100
@@ -1545,6 +1545,8 @@
 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
 by (induct xs) simp_all
 
+lemmas empty_filter_conv = filter_empty_conv[THEN eq_iff_swap]
+
 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
 proof (induct xs)
   case (Cons x xs)