# HG changeset patch
# User huffman
# Date 1358220519 28800
# Node ID 0785906695276381efa35d514e05d4011d7dc525
# Parent  fb0fcd278ac5534d6510875d62201986c5063f63
generalize lemma islimpt_finite to class t1_space

diff -r fb0fcd278ac5 -r 078590669527 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 13:46:19 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 19:28:39 2013 -0800
@@ -917,21 +917,8 @@
   ultimately show ?case by blast
 qed
 
-lemma islimpt_finite:
-  fixes S :: "'a::metric_space set"
-  assumes fS: "finite S" shows "\<not> a islimpt S"
-  unfolding islimpt_approachable
-  using finite_set_avoid[OF fS, of a] by (metis dist_commute  not_le)
-
 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
-  apply (rule iffI)
-  defer
-  apply (metis Un_upper1 Un_upper2 islimpt_subset)
-  unfolding islimpt_def
-  apply (rule ccontr, clarsimp, rename_tac A B)
-  apply (drule_tac x="A \<inter> B" in spec)
-  apply (auto simp add: open_Int)
-  done
+  by (simp add: islimpt_iff_eventually eventually_conj_iff)
 
 lemma discrete_imp_closed:
   fixes S :: "'a::metric_space set"
@@ -2497,11 +2484,16 @@
     by (rule islimpt_subset) auto
 qed
 
+lemma islimpt_finite:
+  fixes x :: "'a::t1_space"
+  shows "finite s \<Longrightarrow> \<not> x islimpt s"
+by (induct set: finite, simp_all add: islimpt_insert)
+
 lemma islimpt_union_finite:
   fixes x :: "'a::t1_space"
   shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
-by (induct set: finite, simp_all add: islimpt_insert)
- 
+by (simp add: islimpt_Un islimpt_finite)
+
 lemma sequence_unique_limpt:
   fixes f :: "nat \<Rightarrow> 'a::t2_space"
   assumes "(f ---> l) sequentially" and "l' islimpt (range f)"