src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44212 4d10e7f342b1
parent 44211 bd7c586b902e
child 44213 6fb54701a11b
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 12:13:46 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 12:18:34 2011 -0700
     1.3 @@ -4211,31 +4211,35 @@
     1.4  
     1.5  text {* A uniformly convergent limit of continuous functions is continuous. *}
     1.6  
     1.7 -lemma norm_triangle_lt:
     1.8 -  fixes x y :: "'a::real_normed_vector"
     1.9 -  shows "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
    1.10 -by (rule le_less_trans [OF norm_triangle_ineq])
    1.11 -
    1.12  lemma continuous_uniform_limit:
    1.13 -  fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
    1.14 -  assumes "\<not> (trivial_limit net)"  "eventually (\<lambda>n. continuous_on s (f n)) net"
    1.15 -  "\<forall>e>0. eventually (\<lambda>n. \<forall>x \<in> s. norm(f n x - g x) < e) net"
    1.16 +  fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::metric_space"
    1.17 +  assumes "\<not> trivial_limit F"
    1.18 +  assumes "eventually (\<lambda>n. continuous_on s (f n)) F"
    1.19 +  assumes "\<forall>e>0. eventually (\<lambda>n. \<forall>x\<in>s. dist (f n x) (g x) < e) F"
    1.20    shows "continuous_on s g"
    1.21  proof-
    1.22    { fix x and e::real assume "x\<in>s" "e>0"
    1.23 -    have "eventually (\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3) net" using `e>0` assms(3)[THEN spec[where x="e/3"]] by auto
    1.24 -    then obtain n where n:"\<forall>xa\<in>s. norm (f n xa - g xa) < e / 3"  "continuous_on s (f n)"
    1.25 -      using eventually_conj_iff[of "(\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3)" "(\<lambda>n. continuous_on s (f n))" net] assms(1,2) eventually_happens by blast
    1.26 +    have "eventually (\<lambda>n. \<forall>x\<in>s. dist (f n x) (g x) < e / 3) F"
    1.27 +      using `e>0` assms(3)[THEN spec[where x="e/3"]] by auto
    1.28 +    from eventually_happens [OF eventually_conj [OF this assms(2)]]
    1.29 +    obtain n where n:"\<forall>x\<in>s. dist (f n x) (g x) < e / 3"  "continuous_on s (f n)"
    1.30 +      using assms(1) by blast
    1.31      have "e / 3 > 0" using `e>0` by auto
    1.32      then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f n x') (f n x) < e / 3"
    1.33        using n(2)[unfolded continuous_on_iff, THEN bspec[where x=x], OF `x\<in>s`, THEN spec[where x="e/3"]] by blast
    1.34 -    { fix y assume "y\<in>s" "dist y x < d"
    1.35 -      hence "dist (f n y) (f n x) < e / 3" using d[THEN bspec[where x=y]] by auto
    1.36 -      hence "norm (f n y - g x) < 2 * e / 3" using norm_triangle_lt[of "f n y - f n x" "f n x - g x" "2*e/3"]
    1.37 -        using n(1)[THEN bspec[where x=x], OF `x\<in>s`] unfolding dist_norm unfolding ab_group_add_class.ab_diff_minus by auto
    1.38 -      hence "dist (g y) (g x) < e" unfolding dist_norm using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
    1.39 -        unfolding norm_minus_cancel[of "f n y - g y", THEN sym] using norm_triangle_lt[of "f n y - g x" "g y - f n y" e] by (auto simp add: uminus_add_conv_diff)  }
    1.40 -    hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e" using `d>0` by auto  }
    1.41 +    { fix y assume "y \<in> s" and "dist y x < d"
    1.42 +      hence "dist (f n y) (f n x) < e / 3"
    1.43 +        by (rule d [rule_format])
    1.44 +      hence "dist (f n y) (g x) < 2 * e / 3"
    1.45 +        using dist_triangle [of "f n y" "g x" "f n x"]
    1.46 +        using n(1)[THEN bspec[where x=x], OF `x\<in>s`]
    1.47 +        by auto
    1.48 +      hence "dist (g y) (g x) < e"
    1.49 +        using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
    1.50 +        using dist_triangle3 [of "g y" "g x" "f n y"]
    1.51 +        by auto }
    1.52 +    hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e"
    1.53 +      using `d>0` by auto }
    1.54    thus ?thesis unfolding continuous_on_iff by auto
    1.55  qed
    1.56