784 lemma card_eq_setsum: |
784 lemma card_eq_setsum: |
785 "card A = setsum (\<lambda>x. 1) A" |
785 "card A = setsum (\<lambda>x. 1) A" |
786 by (simp only: card_def setsum_def) |
786 by (simp only: card_def setsum_def) |
787 |
787 |
788 lemma card_UN_disjoint: |
788 lemma card_UN_disjoint: |
789 "finite I ==> (ALL i:I. finite (A i)) ==> |
789 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" |
790 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) |
790 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" |
791 ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))" |
791 shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))" |
792 apply (simp add: card_eq_setsum del: setsum_constant) |
792 proof - |
793 apply (subgoal_tac |
793 have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp |
794 "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I") |
794 with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant) |
795 apply (simp add: setsum_UN_disjoint del: setsum_constant) |
795 qed |
796 apply simp |
|
797 done |
|
798 |
796 |
799 lemma card_Union_disjoint: |
797 lemma card_Union_disjoint: |
800 "finite C ==> (ALL A:C. finite A) ==> |
798 "finite C ==> (ALL A:C. finite A) ==> |
801 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |
799 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |
802 ==> card (Union C) = setsum card C" |
800 ==> card (Union C) = setsum card C" |