changeset 35844 | 65258d2c3214 |
parent 35056 | d97b5c3af6d5 |
child 40786 | 0a54cfc9add3 |
--- a/src/HOL/Library/Infinite_Set.thy Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Sat Mar 20 02:23:41 2010 +0100 @@ -52,6 +52,9 @@ lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)" by simp +lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" + by simp + lemma infinite_super: assumes T: "S \<subseteq> T" and S: "infinite S" shows "infinite T"