author huffman Fri Aug 26 08:56:29 2011 -0700 (2011-08-26) changeset 44533 7abe4a59f75d parent 44532 a2e9b39df938 child 44534 002b43117115
generalize and simplify proof of continuous_within_sequentially
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.5  text {* Characterization of various kinds of continuity in terms of sequences. *}
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.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.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")