generalize and simplify proof of continuous_within_sequentially
authorhuffman
Fri Aug 26 08:56:29 2011 -0700 (2011-08-26)
changeset 445337abe4a59f75d
parent 44532 a2e9b39df938
child 44534 002b43117115
generalize and simplify proof of continuous_within_sequentially
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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")