# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1575463478 0
# Node ID 9adb1e16b2a65d10ce8f9bc63404bbed5850b0eb
# Parent  54a7ad860a765ecbf13b78ca4fe1e7232eb7984d
two new theorems

diff -r 54a7ad860a76 -r 9adb1e16b2a6 src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Tue Dec 03 16:51:53 2019 +0100
+++ b/src/HOL/Library/Equipollence.thy	Wed Dec 04 12:44:38 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