author nipkow Thu, 09 Jan 2020 08:42:01 +0100 changeset 71356 ce45299cce44 parent 71355 15c6f253b9f3 child 71357 7f2cd237ee4f
 src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions
--- 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))"