src/HOL/Complete_Lattices.thy
changeset 60307 75e1aa7a450e
parent 60172 423273355b55
child 60585 48fdff264eb2
     1.1 --- a/src/HOL/Complete_Lattices.thy	Thu May 28 10:18:46 2015 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Thu May 28 14:33:35 2015 +0100
     1.3 @@ -1204,6 +1204,9 @@
     1.4    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
     1.5    by (fact Sup_image_eq)
     1.6  
     1.7 +lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
     1.8 +  by blast
     1.9 +
    1.10  lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
    1.11    using Union_iff [of _ "B ` A"] by simp
    1.12