--- a/NEWS Mon Nov 19 12:50:23 2018 +0100
+++ b/NEWS Mon Nov 19 15:32:12 2018 +0100
@@ -54,6 +54,8 @@
* Theory "HOL-Library.Multiset": the <Union># operator now has the same
precedence as any other prefix function symbol.
+* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
+
* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.
--- a/src/HOL/Groups_Big.thy Mon Nov 19 12:50:23 2018 +0100
+++ b/src/HOL/Groups_Big.thy Mon Nov 19 15:32:12 2018 +0100
@@ -1089,22 +1089,6 @@
qed
qed simp
-lemma card_Union_image:
- assumes "finite S"
- assumes "\<And>s. s \<in> S \<Longrightarrow> finite (f s)"
- assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) S"
- shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S"
-proof -
- have "pairwise disjnt (f ` S)"
- using assms(3)
- by (metis pairwiseD pairwise_imageI)
- then have "card (\<Union>(f ` S)) = sum card (f ` S)"
- by (subst card_Union_disjoint) (use assms in auto)
- also have "... = sum (\<lambda>x. card (f x)) S"
- by (metis (mono_tags, lifting) assms(1) assms(3) sum_card_image)
- finally show ?thesis .
-qed
-
subsubsection \<open>Cardinality of products\<close>