# HG changeset patch
# User nipkow
# Date 1575470218 -3600
# Node ID be2c2bfa54a0e43740a017a8d3dcd574d8234e02
# Parent  e9a4bd0a836e5ee142e73c39cdb27708cf68cad1# Parent  dc767054de47a4e7b6f63a0f4fe63dfee840e73e
merged

diff -r dc767054de47 -r be2c2bfa54a0 src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Wed Dec 04 14:12:59 2019 +0100
+++ b/src/HOL/Library/Equipollence.thy	Wed Dec 04 15:36:58 2019 +0100
@@ -693,4 +693,19 @@
   apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD)
   using finite.simps by auto
 
+lemma lists_lepoll_mono:
+  assumes "A \<lesssim> B" shows "lists A \<lesssim> lists B"
+proof -
+  obtain f where f: "inj_on f A" "f ` A \<subseteq> B"
+    by (meson assms lepoll_def)
+  moreover have "inj_on (map f) (lists A)"
+    using f unfolding inj_on_def
+    by clarsimp (metis list.inj_map_strong)
+  ultimately show ?thesis
+    unfolding lepoll_def by force
+qed
+
+lemma lepoll_lists: "A \<lesssim> lists A"
+  unfolding lepoll_def inj_on_def by(rule_tac x="\<lambda>x. [x]" in exI) auto
+
 end