equal
deleted
inserted
replaced
2082 qed |
2082 qed |
2083 |
2083 |
2084 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1" |
2084 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1" |
2085 unfolding UNIV_unit by simp |
2085 unfolding UNIV_unit by simp |
2086 |
2086 |
|
2087 lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2" |
|
2088 unfolding UNIV_bool by simp |
|
2089 |
2087 |
2090 |
2088 subsubsection {* Cardinality of image *} |
2091 subsubsection {* Cardinality of image *} |
2089 |
2092 |
2090 lemma card_image_le: "finite A ==> card (f ` A) <= card A" |
2093 lemma card_image_le: "finite A ==> card (f ` A) <= card A" |
2091 apply (induct rule: finite_induct) |
2094 apply (induct rule: finite_induct) |