shorten proof of frontier_straddle
authorhuffman
Mon Sep 12 14:39:10 2011 -0700 (2011-09-12)
changeset 449091f5d6eb73549
parent 44908 f05bff62f8a6
child 44910 53650b655b47
shorten proof of frontier_straddle
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 13:19:10 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 14:39:10 2011 -0700
     1.3 @@ -763,50 +763,9 @@
     1.4  
     1.5  lemma frontier_straddle:
     1.6    fixes a :: "'a::metric_space"
     1.7 -  shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs")
     1.8 -proof
     1.9 -  assume "?lhs"
    1.10 -  { fix e::real
    1.11 -    assume "e > 0"
    1.12 -    let ?rhse = "(\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)"
    1.13 -    { assume "a\<in>S"
    1.14 -      have "\<exists>x\<in>S. dist a x < e" using `e>0` `a\<in>S` by(rule_tac x=a in bexI) auto
    1.15 -      moreover have "\<exists>x. x \<notin> S \<and> dist a x < e" using `?lhs` `a\<in>S`
    1.16 -        unfolding frontier_closures closure_def islimpt_def using `e>0`
    1.17 -        by (auto, erule_tac x="ball a e" in allE, auto)
    1.18 -      ultimately have ?rhse by auto
    1.19 -    }
    1.20 -    moreover
    1.21 -    { assume "a\<notin>S"
    1.22 -      hence ?rhse using `?lhs`
    1.23 -        unfolding frontier_closures closure_def islimpt_def
    1.24 -        using open_ball[of a e] `e > 0`
    1.25 -          by simp (metis centre_in_ball mem_ball open_ball) 
    1.26 -    }
    1.27 -    ultimately have ?rhse by auto
    1.28 -  }
    1.29 -  thus ?rhs by auto
    1.30 -next
    1.31 -  assume ?rhs
    1.32 -  moreover
    1.33 -  { fix T assume "a\<notin>S" and
    1.34 -    as:"\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)" "a \<notin> S" "a \<in> T" "open T"
    1.35 -    from `open T` `a \<in> T` have "\<exists>e>0. ball a e \<subseteq> T" unfolding open_contains_ball[of T] by auto
    1.36 -    then obtain e where "e>0" "ball a e \<subseteq> T" by auto
    1.37 -    then obtain y where y:"y\<in>S" "dist a y < e"  using as(1) by auto
    1.38 -    have "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> a"
    1.39 -      using `dist a y < e` `ball a e \<subseteq> T` unfolding ball_def using `y\<in>S` `a\<notin>S` by auto
    1.40 -  }
    1.41 -  hence "a \<in> closure S" unfolding closure_def islimpt_def using `?rhs` by auto
    1.42 -  moreover
    1.43 -  { fix T assume "a \<in> T"  "open T" "a\<in>S"
    1.44 -    then obtain e where "e>0" and balle: "ball a e \<subseteq> T" unfolding open_contains_ball using `?rhs` by auto
    1.45 -    obtain x where "x \<notin> S" "dist a x < e" using `?rhs` using `e>0` by auto
    1.46 -    hence "\<exists>y\<in>- S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto
    1.47 -  }
    1.48 -  hence "a islimpt (- S) \<or> a\<notin>S" unfolding islimpt_def by auto
    1.49 -  ultimately show ?lhs unfolding frontier_closures using closure_def[of "- S"] by auto
    1.50 -qed
    1.51 +  shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
    1.52 +  unfolding frontier_def closure_interior
    1.53 +  by (auto simp add: mem_interior subset_eq ball_def)
    1.54  
    1.55  lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
    1.56    by (metis frontier_def closure_closed Diff_subset)