src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44519 ea85d78a994e
parent 44518 219a6fe4cfae
child 44522 2f7e9d890efe
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 16:08:21 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 09:17:02 2011 -0700
     1.3 @@ -555,37 +555,58 @@
     1.4  
     1.5  subsection {* Interior of a Set *}
     1.6  
     1.7 -definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
     1.8 +definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
     1.9 +
    1.10 +lemma interiorI [intro?]:
    1.11 +  assumes "open T" and "x \<in> T" and "T \<subseteq> S"
    1.12 +  shows "x \<in> interior S"
    1.13 +  using assms unfolding interior_def by fast
    1.14 +
    1.15 +lemma interiorE [elim?]:
    1.16 +  assumes "x \<in> interior S"
    1.17 +  obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
    1.18 +  using assms unfolding interior_def by fast
    1.19 +
    1.20 +lemma open_interior [simp, intro]: "open (interior S)"
    1.21 +  by (simp add: interior_def open_Union)
    1.22 +
    1.23 +lemma interior_subset: "interior S \<subseteq> S"
    1.24 +  by (auto simp add: interior_def)
    1.25 +
    1.26 +lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
    1.27 +  by (auto simp add: interior_def)
    1.28 +
    1.29 +lemma interior_open: "open S \<Longrightarrow> interior S = S"
    1.30 +  by (intro equalityI interior_subset interior_maximal subset_refl)
    1.31  
    1.32  lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
    1.33 -  apply (simp add: set_eq_iff interior_def)
    1.34 -  apply (subst (2) open_subopen) by (safe, blast+)
    1.35 -
    1.36 -lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
    1.37 -
    1.38 -lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
    1.39 -
    1.40 -lemma open_interior[simp, intro]: "open(interior S)"
    1.41 -  apply (simp add: interior_def)
    1.42 -  apply (subst open_subopen) by blast
    1.43 -
    1.44 -lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
    1.45 -lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
    1.46 -lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
    1.47 -lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
    1.48 -lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T  \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T"
    1.49 -  by (metis equalityI interior_maximal interior_subset open_interior)
    1.50 -lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
    1.51 -  apply (simp add: interior_def)
    1.52 -  by (metis open_contains_ball centre_in_ball open_ball subset_trans)
    1.53 -
    1.54 -lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
    1.55 +  by (metis open_interior interior_open)
    1.56 +
    1.57 +lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
    1.58    by (metis interior_maximal interior_subset subset_trans)
    1.59  
    1.60 -lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
    1.61 -  apply (rule equalityI, simp)
    1.62 -  apply (metis Int_lower1 Int_lower2 subset_interior)
    1.63 -  by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
    1.64 +lemma interior_empty [simp]: "interior {} = {}"
    1.65 +  using open_empty by (rule interior_open)
    1.66 +
    1.67 +lemma interior_interior [simp]: "interior (interior S) = interior S"
    1.68 +  using open_interior by (rule interior_open)
    1.69 +
    1.70 +lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
    1.71 +  by (auto simp add: interior_def) (* TODO: rename to interior_mono *)
    1.72 +
    1.73 +lemma interior_unique:
    1.74 +  assumes "T \<subseteq> S" and "open T"
    1.75 +  assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
    1.76 +  shows "interior S = T"
    1.77 +  by (intro equalityI assms interior_subset open_interior interior_maximal)
    1.78 +
    1.79 +lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
    1.80 +  by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1
    1.81 +    Int_lower2 interior_maximal interior_subset open_Int open_interior)
    1.82 +
    1.83 +lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
    1.84 +  using open_contains_ball_eq [where S="interior S"]
    1.85 +  by (simp add: open_subset_interior)
    1.86  
    1.87  lemma interior_limit_point [intro]:
    1.88    fixes x :: "'a::perfect_space"
    1.89 @@ -599,21 +620,20 @@
    1.90  
    1.91  lemma interior_closed_Un_empty_interior:
    1.92    assumes cS: "closed S" and iT: "interior T = {}"
    1.93 -  shows "interior(S \<union> T) = interior S"
    1.94 +  shows "interior (S \<union> T) = interior S"
    1.95  proof
    1.96 -  show "interior S \<subseteq> interior (S\<union>T)"
    1.97 -    by (rule subset_interior, blast)
    1.98 +  show "interior S \<subseteq> interior (S \<union> T)"
    1.99 +    by (rule subset_interior, rule Un_upper1)
   1.100  next
   1.101    show "interior (S \<union> T) \<subseteq> interior S"
   1.102    proof
   1.103      fix x assume "x \<in> interior (S \<union> T)"
   1.104 -    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
   1.105 -      unfolding interior_def by fast
   1.106 +    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
   1.107      show "x \<in> interior S"
   1.108      proof (rule ccontr)
   1.109        assume "x \<notin> interior S"
   1.110        with `x \<in> R` `open R` obtain y where "y \<in> R - S"
   1.111 -        unfolding interior_def set_eq_iff by fast
   1.112 +        unfolding interior_def by fast
   1.113        from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
   1.114        from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
   1.115        from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
   1.116 @@ -628,15 +648,16 @@
   1.117      by (intro Sigma_mono interior_subset)
   1.118    show "open (interior A \<times> interior B)"
   1.119      by (intro open_Times open_interior)
   1.120 -  show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
   1.121 -    apply (simp add: open_prod_def, clarify)
   1.122 -    apply (drule (1) bspec, clarify, rename_tac C D)
   1.123 -    apply (simp add: interior_def, rule conjI)
   1.124 -    apply (rule_tac x=C in exI, clarsimp)
   1.125 -    apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
   1.126 -    apply (rule_tac x=D in exI, clarsimp)
   1.127 -    apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
   1.128 -    done
   1.129 +  fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
   1.130 +  proof (safe)
   1.131 +    fix x y assume "(x, y) \<in> T"
   1.132 +    then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
   1.133 +      using `open T` unfolding open_prod_def by fast
   1.134 +    hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
   1.135 +      using `T \<subseteq> A \<times> B` by auto
   1.136 +    thus "x \<in> interior A" and "y \<in> interior B"
   1.137 +      by (auto intro: interiorI)
   1.138 +  qed
   1.139  qed
   1.140  
   1.141  
   1.142 @@ -657,57 +678,33 @@
   1.143    unfolding closure_def by simp
   1.144  
   1.145  lemma closure_hull: "closure S = closed hull S"
   1.146 -proof-
   1.147 -  have "S \<subseteq> closure S"
   1.148 -    by (rule closure_subset)
   1.149 -  moreover
   1.150 -  have "closed (closure S)"
   1.151 -    by (rule closed_closure)
   1.152 -  moreover
   1.153 -  { fix t
   1.154 -    assume *:"S \<subseteq> t" "closed t"
   1.155 -    { fix x
   1.156 -      assume "x islimpt S"
   1.157 -      hence "x islimpt t" using *(1)
   1.158 -        using islimpt_subset[of x, of S, of t]
   1.159 -        by blast
   1.160 -    }
   1.161 -    with * have "closure S \<subseteq> t"
   1.162 -      unfolding closure_def
   1.163 -      using closed_limpt[of t]
   1.164 -      by auto
   1.165 -  }
   1.166 -  ultimately show ?thesis
   1.167 -    by (rule hull_unique [symmetric])
   1.168 -qed
   1.169 +  unfolding hull_def closure_interior interior_def by auto
   1.170  
   1.171  lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
   1.172 -  unfolding closure_hull
   1.173 -  using hull_eq[of closed, OF  closed_Inter, of S]
   1.174 -  by metis
   1.175 -
   1.176 -lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
   1.177 -  using closure_eq[of S]
   1.178 -  by simp
   1.179 -
   1.180 -lemma closure_closure[simp]: "closure (closure S) = closure S"
   1.181 +  unfolding closure_hull using closed_Inter by (rule hull_eq)
   1.182 +
   1.183 +lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
   1.184 +  unfolding closure_eq .
   1.185 +
   1.186 +lemma closure_closure [simp]: "closure (closure S) = closure S"
   1.187    unfolding closure_hull by (rule hull_hull)
   1.188  
   1.189  lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
   1.190    unfolding closure_hull by (rule hull_mono)
   1.191  
   1.192 -lemma closure_minimal: "S \<subseteq> T \<Longrightarrow>  closed T \<Longrightarrow> closure S \<subseteq> T"
   1.193 +lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
   1.194    unfolding closure_hull by (rule hull_minimal)
   1.195  
   1.196 -lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
   1.197 -  using hull_unique[of S T closed]
   1.198 -  unfolding closure_hull
   1.199 -  by simp
   1.200 -
   1.201 -lemma closure_empty[simp]: "closure {} = {}"
   1.202 +lemma closure_unique:
   1.203 +  assumes "S \<subseteq> T" and "closed T"
   1.204 +  assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
   1.205 +  shows "closure S = T"
   1.206 +  using assms unfolding closure_hull by (rule hull_unique)
   1.207 +
   1.208 +lemma closure_empty [simp]: "closure {} = {}"
   1.209    using closed_empty by (rule closure_closed)
   1.210  
   1.211 -lemma closure_univ[simp]: "closure UNIV = UNIV"
   1.212 +lemma closure_univ [simp]: "closure UNIV = UNIV"
   1.213    using closed_UNIV by (rule closure_closed)
   1.214  
   1.215  lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
   1.216 @@ -752,19 +749,19 @@
   1.217      by blast
   1.218  qed
   1.219  
   1.220 -lemma closure_complement: "closure(- S) = - interior(S)"
   1.221 +lemma closure_complement: "closure (- S) = - interior S"
   1.222    unfolding closure_interior by simp
   1.223  
   1.224 -lemma interior_complement: "interior(- S) = - closure(S)"
   1.225 +lemma interior_complement: "interior (- S) = - closure S"
   1.226    unfolding closure_interior by simp
   1.227  
   1.228  lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
   1.229 -proof (intro closure_unique conjI)
   1.230 +proof (rule closure_unique)
   1.231    show "A \<times> B \<subseteq> closure A \<times> closure B"
   1.232      by (intro Sigma_mono closure_subset)
   1.233    show "closed (closure A \<times> closure B)"
   1.234      by (intro closed_Times closed_closure)
   1.235 -  show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
   1.236 +  fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
   1.237      apply (simp add: closed_def open_prod_def, clarify)
   1.238      apply (rule ccontr)
   1.239      apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
   1.240 @@ -1038,8 +1035,7 @@
   1.241    assumes "x \<in> interior S"
   1.242    shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
   1.243  proof-
   1.244 -  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
   1.245 -    unfolding interior_def by fast
   1.246 +  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
   1.247    { assume "?lhs"
   1.248      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   1.249        unfolding Limits.eventually_within Limits.eventually_at_topological
   1.250 @@ -2731,8 +2727,8 @@
   1.251    fixes x :: "'a::t1_space"
   1.252    shows "closure (insert x s) = insert x (closure s)"
   1.253  apply (rule closure_unique)
   1.254 -apply (rule conjI [OF insert_mono [OF closure_subset]])
   1.255 -apply (rule conjI [OF closed_insert [OF closed_closure]])
   1.256 +apply (rule insert_mono [OF closure_subset])
   1.257 +apply (rule closed_insert [OF closed_closure])
   1.258  apply (simp add: closure_minimal)
   1.259  done
   1.260  
   1.261 @@ -3299,10 +3295,9 @@
   1.262    unfolding continuous_on by (metis subset_eq Lim_within_subset)
   1.263  
   1.264  lemma continuous_on_interior:
   1.265 -  shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
   1.266 -unfolding interior_def
   1.267 -apply simp
   1.268 -by (meson continuous_on_eq_continuous_at continuous_on_subset)
   1.269 +  shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
   1.270 +  by (erule interiorE, drule (1) continuous_on_subset,
   1.271 +    simp add: continuous_on_eq_continuous_at)
   1.272  
   1.273  lemma continuous_on_eq:
   1.274    "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
   1.275 @@ -3744,13 +3739,20 @@
   1.276  lemma interior_image_subset:
   1.277    assumes "\<forall>x. continuous (at x) f" "inj f"
   1.278    shows "interior (f ` s) \<subseteq> f ` (interior s)"
   1.279 -  apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
   1.280 -proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s" 
   1.281 -  hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
   1.282 -  thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as
   1.283 -    apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
   1.284 -  proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
   1.285 -    thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
   1.286 +proof
   1.287 +  fix x assume "x \<in> interior (f ` s)"
   1.288 +  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
   1.289 +  hence "x \<in> f ` s" by auto
   1.290 +  then obtain y where y: "y \<in> s" "x = f y" by auto
   1.291 +  have "open (vimage f T)"
   1.292 +    using assms(1) `open T` by (rule continuous_open_vimage)
   1.293 +  moreover have "y \<in> vimage f T"
   1.294 +    using `x = f y` `x \<in> T` by simp
   1.295 +  moreover have "vimage f T \<subseteq> s"
   1.296 +    using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
   1.297 +  ultimately have "y \<in> interior s" ..
   1.298 +  with `x = f y` show "x \<in> f ` interior s" ..
   1.299 +qed
   1.300  
   1.301  text {* Equality of continuous functions on closure and related results. *}
   1.302  
   1.303 @@ -4818,13 +4820,15 @@
   1.304    finally show "closed {a .. b}" .
   1.305  qed
   1.306  
   1.307 -lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
   1.308 - "interior {a .. b} = {a<..<b}" (is "?L = ?R")
   1.309 +lemma interior_closed_interval [intro]:
   1.310 +  fixes a b :: "'a::ordered_euclidean_space"
   1.311 +  shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
   1.312  proof(rule subset_antisym)
   1.313 -  show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
   1.314 +  show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
   1.315 +    by (rule interior_maximal)
   1.316  next
   1.317 -  { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
   1.318 -    then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
   1.319 +  { fix x assume "x \<in> interior {a..b}"
   1.320 +    then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
   1.321      then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
   1.322      { fix i assume i:"i<DIM('a)"
   1.323        have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
   1.324 @@ -4839,7 +4843,7 @@
   1.325        hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
   1.326          unfolding basis_component using `e>0` i by auto  }
   1.327      hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
   1.328 -  thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
   1.329 +  thus "?L \<subseteq> ?R" ..
   1.330  qed
   1.331  
   1.332  lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"