equal
deleted
inserted
replaced
992 by blast |
992 by blast |
993 |
993 |
994 lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" |
994 lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" |
995 by blast |
995 by blast |
996 |
996 |
|
997 lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)" |
|
998 by auto |
|
999 |
997 lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" |
1000 lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" |
998 by blast |
1001 by blast |
999 |
1002 |
1000 text{*Converse inclusion requires some assumptions*} |
1003 text{*Converse inclusion requires some assumptions*} |
1001 lemma Image_INT_eq: |
1004 lemma Image_INT_eq: |
1009 by blast |
1012 by blast |
1010 |
1013 |
1011 lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}" |
1014 lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}" |
1012 by auto |
1015 by auto |
1013 |
1016 |
|
1017 lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)" |
|
1018 by auto |
|
1019 |
|
1020 lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)" |
|
1021 by auto |
1014 |
1022 |
1015 subsubsection {* Inverse image *} |
1023 subsubsection {* Inverse image *} |
1016 |
1024 |
1017 definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel" |
1025 definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel" |
1018 where |
1026 where |