# HG changeset patch
# User nipkow
# Date 1578555721 -3600
# Node ID ce45299cce44a7e6ea4ce83f8f3875bb7694825d
# Parent  15c6f253b9f345731b3b85997367900e589805b3
added lemma

diff -r 15c6f253b9f3 -r ce45299cce44 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Jan 07 17:12:54 2020 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Jan 09 08:42:01 2020 +0100
@@ -1187,6 +1187,29 @@
     using assms card_eq_0_iff finite_UnionD by fastforce
 qed
 
+lemma card_Union_le_sum_card:
+  fixes U :: "'a set set"
+  assumes "\<forall>u \<in> U. finite u"
+  shows "card (\<Union>U) \<le> sum card U"
+proof (cases "finite U")
+  case False
+  then show "card (\<Union>U) \<le> sum card U"
+    using card_eq_0_iff finite_UnionD by auto
+next
+  case True
+  then show "card (\<Union>U) \<le> sum card U"
+  proof (induct U rule: finite_induct)
+    case empty
+    then show ?case by auto
+  next
+    case (insert x F)
+    then have "card(\<Union>(insert x F)) \<le> card(x) + card (\<Union>F)" using card_Un_le by auto
+    also have "... \<le> card(x) + sum card F" using insert.hyps by auto
+    also have "... = sum card (insert x F)" using sum.insert_if and insert.hyps by auto
+    finally show ?case .
+  qed
+qed
+
 lemma card_UN_le:
   assumes "finite I"
   shows "card(\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. card(A i))"