diff -r 6ebe97815275 -r 11065b70407d src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Wed Mar 06 21:44:30 2019 +0100
+++ b/src/HOL/Library/Equipollence.thy	Thu Mar 07 14:08:05 2019 +0000
@@ -82,7 +82,6 @@
   apply (simp add: infinite_countable_subset)
   using infinite_iff_countable_subset by blast
 
-
 lemma bij_betw_iff_bijections:
   "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
   (is "?lhs = ?rhs")
@@ -114,9 +113,23 @@
     using * by (auto simp: image_def)
 qed
 
+lemma singleton_lepoll: "{x} \<lesssim> insert y A"
+  by (force simp: lepoll_def)
+
+lemma singleton_eqpoll: "{x} \<approx> {y}"
+  by (blast intro: lepoll_antisym singleton_lepoll)
+
+lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}"
+proof safe
+  show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
+    using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
+  show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
+  by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
+qed
+
+
 subsection\<open>The strict relation\<close>
 
-
 lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)"
   by (simp add: lepoll_antisym lesspoll_def)