author | nipkow |
Tue, 04 Oct 2005 23:30:46 +0200 | |
changeset 17761 | 2c42d0a94f58 |
parent 17760 | 4191beda8b90 |
child 17762 | 478869f444ca |
--- a/src/HOL/Finite_Set.thy Tue Oct 04 21:39:16 2005 +0200 +++ b/src/HOL/Finite_Set.thy Tue Oct 04 23:30:46 2005 +0200 @@ -177,6 +177,9 @@ qed qed +lemma finite_Collect_subset: "finite A \<Longrightarrow> finite{x \<in> A. P x}" +using finite_subset[of "{x \<in> A. P x}" "A"] by blast + lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)