src/HOL/Relation.thy
changeset 54410 0a578fb7fb73
parent 54147 97a8ff4e4ac9
child 54555 e8c5e95d338b
     1.1 --- a/src/HOL/Relation.thy	Tue Nov 12 19:28:51 2013 +0100
     1.2 +++ b/src/HOL/Relation.thy	Tue Nov 12 19:28:51 2013 +0100
     1.3 @@ -994,6 +994,9 @@
     1.4  lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
     1.5    by blast
     1.6  
     1.7 +lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)"
     1.8 +  by auto
     1.9 +
    1.10  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
    1.11    by blast
    1.12  
    1.13 @@ -1011,6 +1014,11 @@
    1.14  lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
    1.15    by auto
    1.16  
    1.17 +lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)"
    1.18 +  by auto
    1.19 +
    1.20 +lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
    1.21 +  by auto
    1.22  
    1.23  subsubsection {* Inverse image *}
    1.24