src/HOL/Complete_Lattices.thy

--- a/src/HOL/Complete_Lattices.thy	Tue May 17 08:40:24 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Tue May 17 17:05:35 2016 +0200
@@ -1276,6 +1276,8 @@
 lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
   by blast
 
+lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on (op ` f) A"
+  unfolding inj_on_def by blast
 
 subsubsection \<open>Distributive laws\<close>