# HG changeset patch
# User paulson
# Date 1575463487 0
# Node ID e9a4bd0a836e5ee142e73c39cdb27708cf68cad1
# Parent  1249859d23dd76f6ae47aa6bd16568ff9b127fcb# Parent  9adb1e16b2a65d10ce8f9bc63404bbed5850b0eb
merged

diff -r 1249859d23dd -r e9a4bd0a836e src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Wed Dec 04 12:00:07 2019 +0100
+++ b/src/HOL/Library/Equipollence.thy	Wed Dec 04 12:44:47 2019 +0000
@@ -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