author huffman Mon Sep 12 14:39:10 2011 -0700 (2011-09-12) changeset 44909 1f5d6eb73549 parent 44908 f05bff62f8a6 child 44910 53650b655b47
shorten proof of frontier_straddle
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.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.55  lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
1.56    by (metis frontier_def closure_closed Diff_subset)