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
```