--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 16:08:21 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 25 09:17:02 2011 -0700
@@ -555,37 +555,58 @@
subsection {* Interior of a Set *}
-definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
+definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+
+lemma interiorI [intro?]:
+ assumes "open T" and "x \<in> T" and "T \<subseteq> S"
+ shows "x \<in> interior S"
+ using assms unfolding interior_def by fast
+
+lemma interiorE [elim?]:
+ assumes "x \<in> interior S"
+ obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
+ using assms unfolding interior_def by fast
+
+lemma open_interior [simp, intro]: "open (interior S)"
+ by (simp add: interior_def open_Union)
+
+lemma interior_subset: "interior S \<subseteq> S"
+ by (auto simp add: interior_def)
+
+lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
+ by (auto simp add: interior_def)
+
+lemma interior_open: "open S \<Longrightarrow> interior S = S"
+ by (intro equalityI interior_subset interior_maximal subset_refl)
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
- apply (simp add: set_eq_iff interior_def)
- apply (subst (2) open_subopen) by (safe, blast+)
-
-lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
-
-lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
-
-lemma open_interior[simp, intro]: "open(interior S)"
- apply (simp add: interior_def)
- apply (subst open_subopen) by blast
-
-lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
-lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
-lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
-lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
-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"
- by (metis equalityI interior_maximal interior_subset open_interior)
-lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
- apply (simp add: interior_def)
- by (metis open_contains_ball centre_in_ball open_ball subset_trans)
-
-lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
+ by (metis open_interior interior_open)
+
+lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
by (metis interior_maximal interior_subset subset_trans)
-lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
- apply (rule equalityI, simp)
- apply (metis Int_lower1 Int_lower2 subset_interior)
- by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
+lemma interior_empty [simp]: "interior {} = {}"
+ using open_empty by (rule interior_open)
+
+lemma interior_interior [simp]: "interior (interior S) = interior S"
+ using open_interior by (rule interior_open)
+
+lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+ by (auto simp add: interior_def) (* TODO: rename to interior_mono *)
+
+lemma interior_unique:
+ assumes "T \<subseteq> S" and "open T"
+ assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
+ shows "interior S = T"
+ by (intro equalityI assms interior_subset open_interior interior_maximal)
+
+lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+ by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1
+ Int_lower2 interior_maximal interior_subset open_Int open_interior)
+
+lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+ using open_contains_ball_eq [where S="interior S"]
+ by (simp add: open_subset_interior)
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
@@ -599,21 +620,20 @@
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S" and iT: "interior T = {}"
- shows "interior(S \<union> T) = interior S"
+ shows "interior (S \<union> T) = interior S"
proof
- show "interior S \<subseteq> interior (S\<union>T)"
- by (rule subset_interior, blast)
+ show "interior S \<subseteq> interior (S \<union> T)"
+ by (rule subset_interior, rule Un_upper1)
next
show "interior (S \<union> T) \<subseteq> interior S"
proof
fix x assume "x \<in> interior (S \<union> T)"
- then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
- unfolding interior_def by fast
+ then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
show "x \<in> interior S"
proof (rule ccontr)
assume "x \<notin> interior S"
with `x \<in> R` `open R` obtain y where "y \<in> R - S"
- unfolding interior_def set_eq_iff by fast
+ unfolding interior_def by fast
from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -628,15 +648,16 @@
by (intro Sigma_mono interior_subset)
show "open (interior A \<times> interior B)"
by (intro open_Times open_interior)
- show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
- apply (simp add: open_prod_def, clarify)
- apply (drule (1) bspec, clarify, rename_tac C D)
- apply (simp add: interior_def, rule conjI)
- apply (rule_tac x=C in exI, clarsimp)
- apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
- apply (rule_tac x=D in exI, clarsimp)
- apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
- done
+ fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+ proof (safe)
+ fix x y assume "(x, y) \<in> T"
+ then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
+ using `open T` unfolding open_prod_def by fast
+ hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+ using `T \<subseteq> A \<times> B` by auto
+ thus "x \<in> interior A" and "y \<in> interior B"
+ by (auto intro: interiorI)
+ qed
qed
@@ -657,57 +678,33 @@
unfolding closure_def by simp
lemma closure_hull: "closure S = closed hull S"
-proof-
- have "S \<subseteq> closure S"
- by (rule closure_subset)
- moreover
- have "closed (closure S)"
- by (rule closed_closure)
- moreover
- { fix t
- assume *:"S \<subseteq> t" "closed t"
- { fix x
- assume "x islimpt S"
- hence "x islimpt t" using *(1)
- using islimpt_subset[of x, of S, of t]
- by blast
- }
- with * have "closure S \<subseteq> t"
- unfolding closure_def
- using closed_limpt[of t]
- by auto
- }
- ultimately show ?thesis
- by (rule hull_unique [symmetric])
-qed
+ unfolding hull_def closure_interior interior_def by auto
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
- unfolding closure_hull
- using hull_eq[of closed, OF closed_Inter, of S]
- by metis
-
-lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
- using closure_eq[of S]
- by simp
-
-lemma closure_closure[simp]: "closure (closure S) = closure S"
+ unfolding closure_hull using closed_Inter by (rule hull_eq)
+
+lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
+ unfolding closure_eq .
+
+lemma closure_closure [simp]: "closure (closure S) = closure S"
unfolding closure_hull by (rule hull_hull)
lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
unfolding closure_hull by (rule hull_mono)
-lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
+lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
unfolding closure_hull by (rule hull_minimal)
-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"
- using hull_unique[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_empty[simp]: "closure {} = {}"
+lemma closure_unique:
+ assumes "S \<subseteq> T" and "closed T"
+ assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+ shows "closure S = T"
+ using assms unfolding closure_hull by (rule hull_unique)
+
+lemma closure_empty [simp]: "closure {} = {}"
using closed_empty by (rule closure_closed)
-lemma closure_univ[simp]: "closure UNIV = UNIV"
+lemma closure_univ [simp]: "closure UNIV = UNIV"
using closed_UNIV by (rule closure_closed)
lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
@@ -752,19 +749,19 @@
by blast
qed
-lemma closure_complement: "closure(- S) = - interior(S)"
+lemma closure_complement: "closure (- S) = - interior S"
unfolding closure_interior by simp
-lemma interior_complement: "interior(- S) = - closure(S)"
+lemma interior_complement: "interior (- S) = - closure S"
unfolding closure_interior by simp
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
-proof (intro closure_unique conjI)
+proof (rule closure_unique)
show "A \<times> B \<subseteq> closure A \<times> closure B"
by (intro Sigma_mono closure_subset)
show "closed (closure A \<times> closure B)"
by (intro closed_Times closed_closure)
- show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
+ fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
apply (simp add: closed_def open_prod_def, clarify)
apply (rule ccontr)
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
@@ -1038,8 +1035,7 @@
assumes "x \<in> interior S"
shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
proof-
- from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
- unfolding interior_def by fast
+ from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
unfolding Limits.eventually_within Limits.eventually_at_topological
@@ -2731,8 +2727,8 @@
fixes x :: "'a::t1_space"
shows "closure (insert x s) = insert x (closure s)"
apply (rule closure_unique)
-apply (rule conjI [OF insert_mono [OF closure_subset]])
-apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
apply (simp add: closure_minimal)
done
@@ -3299,10 +3295,9 @@
unfolding continuous_on by (metis subset_eq Lim_within_subset)
lemma continuous_on_interior:
- shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
-unfolding interior_def
-apply simp
-by (meson continuous_on_eq_continuous_at continuous_on_subset)
+ shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
+ by (erule interiorE, drule (1) continuous_on_subset,
+ simp add: continuous_on_eq_continuous_at)
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
@@ -3744,13 +3739,20 @@
lemma interior_image_subset:
assumes "\<forall>x. continuous (at x) f" "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
- apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
-proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s"
- hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
- 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
- apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
- proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
- thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
+proof
+ fix x assume "x \<in> interior (f ` s)"
+ then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
+ hence "x \<in> f ` s" by auto
+ then obtain y where y: "y \<in> s" "x = f y" by auto
+ have "open (vimage f T)"
+ using assms(1) `open T` by (rule continuous_open_vimage)
+ moreover have "y \<in> vimage f T"
+ using `x = f y` `x \<in> T` by simp
+ moreover have "vimage f T \<subseteq> s"
+ using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
+ ultimately have "y \<in> interior s" ..
+ with `x = f y` show "x \<in> f ` interior s" ..
+qed
text {* Equality of continuous functions on closure and related results. *}
@@ -4818,13 +4820,15 @@
finally show "closed {a .. b}" .
qed
-lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
- "interior {a .. b} = {a<..<b}" (is "?L = ?R")
+lemma interior_closed_interval [intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
- show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
+ show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+ by (rule interior_maximal)
next
- { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
- then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
+ { fix x assume "x \<in> interior {a..b}"
+ then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
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
{ fix i assume i:"i<DIM('a)"
have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
@@ -4839,7 +4843,7 @@
hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
unfolding basis_component using `e>0` i by auto }
hence "x \<in> {a<..<b}" unfolding mem_interval by auto }
- thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
+ thus "?L \<subseteq> ?R" ..
qed
lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"