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.5  subsection {* Interior of a Set *}
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.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.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.87  lemma interior_limit_point [intro]:
1.88    fixes x :: "'a::perfect_space"
1.89 @@ -599,21 +620,20 @@
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.142 @@ -657,57 +678,33 @@
1.143    unfolding closure_def by simp
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.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.176 -lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
1.177 -  using closure_eq[of S]
1.178 -  by simp
1.180 -lemma closure_closure[simp]: "closure (closure S) = closure S"
1.181 +  unfolding closure_hull using closed_Inter by (rule hull_eq)
1.183 +lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
1.184 +  unfolding closure_eq .
1.186 +lemma closure_closure [simp]: "closure (closure S) = closure S"
1.187    unfolding closure_hull by (rule hull_hull)
1.189  lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
1.190    unfolding closure_hull by (rule hull_mono)
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.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.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.208 +lemma closure_empty [simp]: "closure {} = {}"
1.209    using closed_empty by (rule closure_closed)
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.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.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.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.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.261 @@ -3299,10 +3295,9 @@
1.262    unfolding continuous_on by (metis subset_eq Lim_within_subset)
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.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.301  text {* Equality of continuous functions on closure and related results. *}
1.303 @@ -4818,13 +4820,15 @@
1.304    finally show "closed {a .. b}" .
1.305  qed
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.332  lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"