1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 08:12:38 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 08:56:29 2011 -0700
1.3 @@ -3309,56 +3309,41 @@
1.4
1.5 text {* Characterization of various kinds of continuity in terms of sequences. *}
1.6
1.7 -(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
1.8 lemma continuous_within_sequentially:
1.9 - fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
1.10 + fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
1.11 shows "continuous (at a within s) f \<longleftrightarrow>
1.12 (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
1.13 --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
1.14 proof
1.15 assume ?lhs
1.16 - { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
1.17 - fix e::real assume "e>0"
1.18 - from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
1.19 - from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
1.20 - hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
1.21 - apply(rule_tac x=N in exI) using N d apply auto using x(1)
1.22 - apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
1.23 - apply(erule_tac x="x n" in ballE) apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
1.24 + { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
1.25 + fix T::"'b set" assume "open T" and "f a \<in> T"
1.26 + with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
1.27 + unfolding continuous_within tendsto_def eventually_within by auto
1.28 + have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
1.29 + using x(2) `d>0` by simp
1.30 + hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
1.31 + proof (rule eventually_elim1)
1.32 + fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
1.33 + using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
1.34 + qed
1.35 }
1.36 - thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
1.37 + thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
1.38 next
1.39 - assume ?rhs
1.40 - { fix e::real assume "e>0"
1.41 - assume "\<not> (\<exists>d>0. \<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e)"
1.42 - hence "\<forall>d. \<exists>x. d>0 \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)" by blast
1.43 - then obtain x where x:"\<forall>d>0. x d \<in> s \<and> (0 < dist (x d) a \<and> dist (x d) a < d \<and> \<not> dist (f (x d)) (f a) < e)"
1.44 - using choice[of "\<lambda>d x.0<d \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)"] by auto
1.45 - { fix d::real assume "d>0"
1.46 - hence "\<exists>N::nat. inverse (real (N + 1)) < d" using real_arch_inv[of d] by (auto, rule_tac x="n - 1" in exI)auto
1.47 - then obtain N::nat where N:"inverse (real (N + 1)) < d" by auto
1.48 - { fix n::nat assume n:"n\<ge>N"
1.49 - hence "dist (x (inverse (real (n + 1)))) a < inverse (real (n + 1))" using x[THEN spec[where x="inverse (real (n + 1))"]] by auto
1.50 - moreover have "inverse (real (n + 1)) < d" using N n by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
1.51 - ultimately have "dist (x (inverse (real (n + 1)))) a < d" by auto
1.52 - }
1.53 - hence "\<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < d" by auto
1.54 - }
1.55 - hence "(\<forall>n::nat. x (inverse (real (n + 1))) \<in> s) \<and> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto
1.56 - hence "\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (f (x (inverse (real (n + 1))))) (f a) < e" using `?rhs`[THEN spec[where x="\<lambda>n::nat. x (inverse (real (n+1)))"], unfolded Lim_sequentially] by auto
1.57 - hence "False" apply(erule_tac x=e in allE) using `e>0` using x by auto
1.58 - }
1.59 - thus ?lhs unfolding continuous_within unfolding Lim_within unfolding Lim_sequentially by blast
1.60 + assume ?rhs thus ?lhs
1.61 + unfolding continuous_within tendsto_def [where l="f a"]
1.62 + by (simp add: sequentially_imp_eventually_within)
1.63 qed
1.64
1.65 lemma continuous_at_sequentially:
1.66 - fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
1.67 + fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
1.68 shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
1.69 --> ((f o x) ---> f a) sequentially)"
1.70 - using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
1.71 + using continuous_within_sequentially[of a UNIV f]
1.72 + unfolding within_UNIV by auto
1.73
1.74 lemma continuous_on_sequentially:
1.75 - fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
1.76 + fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
1.77 shows "continuous_on s f \<longleftrightarrow>
1.78 (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
1.79 --> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")