equal
deleted
inserted
replaced
939 by (fact SUP_constant) |
939 by (fact SUP_constant) |
940 |
940 |
941 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})" |
941 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})" |
942 by (fact SUP_eq) |
942 by (fact SUP_eq) |
943 |
943 |
944 lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" -- "FIXME generalize" |
944 lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" |
945 by blast |
945 by blast |
946 |
946 |
947 lemma UNION_empty_conv[simp]: |
947 lemma UNION_empty_conv[simp]: |
948 "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})" |
948 "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})" |
949 "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})" |
949 "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})" |