# HG changeset patch # User nipkow # Date 1420893097 -3600 # Node ID a95b6f608a738aae2567b5b2fa7faa75a4ac84a5 # Parent e743ce816cf6108178ab27ed098d2078cccc56ba added lemma diff -r e743ce816cf6 -r a95b6f608a73 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Jan 10 10:40:11 2015 +0100 +++ b/src/HOL/Finite_Set.thy Sat Jan 10 13:31:37 2015 +0100 @@ -1322,6 +1322,14 @@ shows "card (A \ B) = card A + card B" using assms card_Un_Int [of A B] by simp +lemma card_Un_le: "card (A \ B) \ card A + card B" +apply(cases "finite A") + apply(cases "finite B") + using le_iff_add card_Un_Int apply blast + apply simp +apply simp +done + lemma card_Diff_subset: assumes "finite B" and "B \ A" shows "card (A - B) = card A - card B"