equal
deleted
inserted
replaced
233 apply (subst Diff_insert) |
233 apply (subst Diff_insert) |
234 apply (case_tac "a : A - B") |
234 apply (case_tac "a : A - B") |
235 apply (rule finite_insert [symmetric, THEN trans]) |
235 apply (rule finite_insert [symmetric, THEN trans]) |
236 apply (subst insert_Diff, simp_all) |
236 apply (subst insert_Diff, simp_all) |
237 done |
237 done |
|
238 |
|
239 lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A" |
|
240 by simp |
238 |
241 |
239 |
242 |
240 text {* Image and Inverse Image over Finite Sets *} |
243 text {* Image and Inverse Image over Finite Sets *} |
241 |
244 |
242 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" |
245 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" |