--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 17:37:31 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 18:55:18 2010 -0700
@@ -1200,7 +1200,7 @@
text{* Another limit point characterization. *}
lemma islimpt_sequential:
- fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
+ fixes x :: "'a::metric_space"
shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
(is "?lhs = ?rhs")
proof
@@ -1537,40 +1537,41 @@
qed
lemma Lim_transform_eventually:
- "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+ "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
apply (rule topological_tendstoI)
apply (drule (2) topological_tendstoD)
apply (erule (1) eventually_elim2, simp)
done
lemma Lim_transform_within:
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
- "(f ---> l) (at x within S)"
- shows "(g ---> l) (at x within S)"
- using assms(1,3) unfolding Lim_within
- apply -
- apply (clarify, rename_tac e)
- apply (drule_tac x=e in spec, clarsimp, rename_tac r)
- apply (rule_tac x="min d r" in exI, clarsimp, rename_tac y)
- apply (drule_tac x=y in bspec, assumption, clarsimp)
- apply (simp add: assms(2))
- done
+ assumes "0 < d" and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+ and "(f ---> l) (at x within S)"
+ shows "(g ---> l) (at x within S)"
+proof (rule Lim_transform_eventually)
+ show "eventually (\<lambda>x. f x = g x) (at x within S)"
+ unfolding eventually_within
+ using assms(1,2) by auto
+ show "(f ---> l) (at x within S)" by fact
+qed
lemma Lim_transform_at:
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
- (f ---> l) (at x) ==> (g ---> l) (at x)"
- apply (subst within_UNIV[symmetric])
- using Lim_transform_within[of d UNIV x f g l]
- by (auto simp add: within_UNIV)
+ assumes "0 < d" and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+ and "(f ---> l) (at x)"
+ shows "(g ---> l) (at x)"
+proof (rule Lim_transform_eventually)
+ show "eventually (\<lambda>x. f x = g x) (at x)"
+ unfolding eventually_at
+ using assms(1,2) by auto
+ show "(f ---> l) (at x)" by fact
+qed
text{* Common case assuming being away from some crucial point like 0. *}
+text {* TODO: generalize the next few lemmas to T1 spaces. *}
+
lemma Lim_transform_away_within:
fixes a b :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
+ assumes "a \<noteq> b" and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and "(f ---> l) (at a within S)"
shows "(g ---> l) (at a within S)"
proof-
@@ -1581,7 +1582,6 @@
lemma Lim_transform_away_at:
fixes a b :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and fl: "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
@@ -1591,15 +1591,14 @@
text{* Alternatively, within an open set. *}
lemma Lim_transform_within_open:
- fixes a :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- assumes "open S" "a \<in> S" "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x" "(f ---> l) (at a)"
+ assumes "open S" and "a \<in> S" and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
+ and "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
-proof-
- from assms(1,2) obtain e::real where "e>0" and e:"ball a e \<subseteq> S" unfolding open_contains_ball by auto
- hence "\<forall>x'. 0 < dist x' a \<and> dist x' a < e \<longrightarrow> f x' = g x'" using assms(3)
- unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_commute)
- thus ?thesis using Lim_transform_at[of e a f g l] `e>0` assms(4) by auto
+proof (rule Lim_transform_eventually)
+ show "eventually (\<lambda>x. f x = g x) (at a)"
+ unfolding eventually_at_topological
+ using assms(1,2,3) by auto
+ show "(f ---> l) (at a)" by fact
qed
text{* A congruence rule allowing us to transform limits assuming not at point. *}
@@ -1607,21 +1606,21 @@
(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
lemma Lim_cong_within(*[cong add]*):
- fixes a :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
- by (simp add: Lim_within dist_nz[symmetric])
-
-lemma Lim_cong_at[cong add]:
- fixes a :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
- by (simp add: Lim_at dist_nz[symmetric])
+ assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+ shows "((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
+ unfolding tendsto_def Limits.eventually_within eventually_at_topological
+ using assms by simp
+
+lemma Lim_cong_at(*[cong add]*):
+ assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+ shows "((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a))"
+ unfolding tendsto_def eventually_at_topological
+ using assms by simp
text{* Useful lemmas on closure and set of possible sequential limits.*}
lemma closure_sequential:
- fixes l :: "'a::metric_space" (* TODO: generalize *)
+ fixes l :: "'a::metric_space"
shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
proof
assume "?lhs" moreover
@@ -2911,7 +2910,7 @@
qed
lemma closed_sing [simp]:
- fixes a :: "'a::metric_space"
+ fixes a :: "'a::metric_space" (* TODO: generalize to t1_space *)
shows "closed {a}"
apply (clarsimp simp add: closed_def open_dist)
apply (rule ccontr)
@@ -3252,7 +3251,7 @@
by (rule Lim_trivial_limit)
next
case False
- hence "netlimit (at x) = x"
+ hence 1: "netlimit (at x) = x"
using netlimit_within [of x UNIV]
by (simp add: within_UNIV)
with * show ?thesis by simp
@@ -3411,38 +3410,28 @@
text{* The usual transformation theorems. *}
lemma continuous_transform_within:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
"continuous (at x within s) f"
shows "continuous (at x within s) g"
-proof-
- { fix e::real assume "e>0"
- then obtain d' where d':"d'>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(4) unfolding continuous_within Lim_within by auto
- { fix x' assume "x'\<in>s" "0 < dist x' x" "dist x' x < (min d d')"
- hence "dist (f x') (g x) < e" using assms(2,3) apply(erule_tac x=x in ballE) using d' by auto }
- hence "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
- hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto }
- hence "(f ---> g x) (at x within s)" unfolding Lim_within using assms(1) by auto
- thus ?thesis unfolding continuous_within using Lim_transform_within[of d s x f g "g x"] using assms by blast
+unfolding continuous_within
+proof (rule Lim_transform_within)
+ show "0 < d" by fact
+ show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+ using assms(3) by auto
+ have "f x = g x"
+ using assms(1,2,3) by auto
+ thus "(f ---> g x) (at x within s)"
+ using assms(4) unfolding continuous_within by simp
qed
lemma continuous_transform_at:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
"continuous (at x) f"
shows "continuous (at x) g"
-proof-
- { fix e::real assume "e>0"
- then obtain d' where d':"d'>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(3) unfolding continuous_at Lim_at by auto
- { fix x' assume "0 < dist x' x" "dist x' x < (min d d')"
- hence "dist (f x') (g x) < e" using assms(2) apply(erule_tac x=x in allE) using d' by auto
- }
- hence "\<forall>xa. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
- hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto
- }
- hence "(f ---> g x) (at x)" unfolding Lim_at using assms(1) by auto
- thus ?thesis unfolding continuous_at using Lim_transform_at[of d x f g "g x"] using assms by blast
-qed
+ using continuous_transform_within [of d x UNIV f g] assms
+ by (simp add: within_UNIV)
text{* Combination results for pointwise continuity. *}