generalize lemma islimpt_finite to class t1_space
authorhuffman
Mon Jan 14 19:28:39 2013 -0800 (2013-01-14)
changeset 50897078590669527
parent 50896 fb0fcd278ac5
child 50898 ebd9b82537e0
generalize lemma islimpt_finite to class t1_space
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 13:46:19 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 19:28:39 2013 -0800
     1.3 @@ -917,21 +917,8 @@
     1.4    ultimately show ?case by blast
     1.5  qed
     1.6  
     1.7 -lemma islimpt_finite:
     1.8 -  fixes S :: "'a::metric_space set"
     1.9 -  assumes fS: "finite S" shows "\<not> a islimpt S"
    1.10 -  unfolding islimpt_approachable
    1.11 -  using finite_set_avoid[OF fS, of a] by (metis dist_commute  not_le)
    1.12 -
    1.13  lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
    1.14 -  apply (rule iffI)
    1.15 -  defer
    1.16 -  apply (metis Un_upper1 Un_upper2 islimpt_subset)
    1.17 -  unfolding islimpt_def
    1.18 -  apply (rule ccontr, clarsimp, rename_tac A B)
    1.19 -  apply (drule_tac x="A \<inter> B" in spec)
    1.20 -  apply (auto simp add: open_Int)
    1.21 -  done
    1.22 +  by (simp add: islimpt_iff_eventually eventually_conj_iff)
    1.23  
    1.24  lemma discrete_imp_closed:
    1.25    fixes S :: "'a::metric_space set"
    1.26 @@ -2497,11 +2484,16 @@
    1.27      by (rule islimpt_subset) auto
    1.28  qed
    1.29  
    1.30 +lemma islimpt_finite:
    1.31 +  fixes x :: "'a::t1_space"
    1.32 +  shows "finite s \<Longrightarrow> \<not> x islimpt s"
    1.33 +by (induct set: finite, simp_all add: islimpt_insert)
    1.34 +
    1.35  lemma islimpt_union_finite:
    1.36    fixes x :: "'a::t1_space"
    1.37    shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
    1.38 -by (induct set: finite, simp_all add: islimpt_insert)
    1.39 - 
    1.40 +by (simp add: islimpt_Un islimpt_finite)
    1.41 +
    1.42  lemma sequence_unique_limpt:
    1.43    fixes f :: "nat \<Rightarrow> 'a::t2_space"
    1.44    assumes "(f ---> l) sequentially" and "l' islimpt (range f)"