equal
deleted
inserted
replaced
189 apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) |
189 apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) |
190 prefer 2 apply assumption |
190 prefer 2 apply assumption |
191 apply blast |
191 apply blast |
192 apply (blast intro: ltI Limit_is_Ord) |
192 apply (blast intro: ltI Limit_is_Ord) |
193 done |
193 done |
194 |
|
195 lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] |
|
196 |
194 |
197 lemma singleton_in_VLimit: |
195 lemma singleton_in_VLimit: |
198 "[| a \<in> Vfrom(A,i); Limit(i) |] ==> {a} \<in> Vfrom(A,i)" |
196 "[| a \<in> Vfrom(A,i); Limit(i) |] ==> {a} \<in> Vfrom(A,i)" |
199 apply (erule Limit_VfromE, assumption) |
197 apply (erule Limit_VfromE, assumption) |
200 apply (erule singleton_in_Vfrom [THEN VfromI]) |
198 apply (erule singleton_in_Vfrom [THEN VfromI]) |