src/HOL/List.thy
changeset 15303 eedbb8d22ca2
parent 15302 a643fcbc3468
child 15304 3514ca74ac54
--- a/src/HOL/List.thy	Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/List.thy	Sun Nov 21 15:44:20 2004 +0100
@@ -507,6 +507,12 @@
 lemma inj_map[iff]: "inj (map f) = inj f"
 by (blast dest: inj_mapD intro: inj_mapI)
 
+lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
+apply(rule inj_onI)
+apply(erule map_inj_on)
+apply(blast intro:inj_onI dest:inj_onD)
+done
+
 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
 by (induct xs, auto)