src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44632 076a45f65e12
parent 44628 bd17b7543af1
child 44647 e4de7750cdeb
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 10:42:31 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 13:28:29 2011 -0700
     1.3 @@ -2242,6 +2242,8 @@
     1.4      unfolding convergent_def by auto
     1.5  qed
     1.6  
     1.7 +instance euclidean_space \<subseteq> banach ..
     1.8 +
     1.9  lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
    1.10  proof(simp add: complete_def, rule, rule)
    1.11    fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
    1.12 @@ -2276,21 +2278,13 @@
    1.13  
    1.14  lemma convergent_eq_cauchy:
    1.15    fixes s :: "nat \<Rightarrow> 'a::complete_space"
    1.16 -  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
    1.17 -proof
    1.18 -  assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
    1.19 -  thus ?rhs using convergent_imp_cauchy by auto
    1.20 -next
    1.21 -  assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto
    1.22 -qed
    1.23 +  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s"
    1.24 +  unfolding Cauchy_convergent_iff convergent_def ..
    1.25  
    1.26  lemma convergent_imp_bounded:
    1.27    fixes s :: "nat \<Rightarrow> 'a::metric_space"
    1.28 -  shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
    1.29 -  using convergent_imp_cauchy[of s]
    1.30 -  using cauchy_imp_bounded[of s]
    1.31 -  unfolding image_def
    1.32 -  by auto
    1.33 +  shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
    1.34 +  by (intro cauchy_imp_bounded convergent_imp_cauchy)
    1.35  
    1.36  subsubsection{* Total boundedness *}
    1.37  
    1.38 @@ -2943,7 +2937,7 @@
    1.39            "\<forall>n. (s n \<noteq> {})"
    1.40            "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
    1.41            "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
    1.42 -  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s n"
    1.43 +  shows "\<exists>a::'a::complete_space. \<forall>n::nat. a \<in> s n"
    1.44  proof-
    1.45    have "\<forall>n. \<exists> x. x\<in>s n" using assms(2) by auto
    1.46    hence "\<exists>t. \<forall>n. t n \<in> s n" using choice[of "\<lambda> n x. x \<in> s n"] by auto
    1.47 @@ -2972,7 +2966,7 @@
    1.48  text {* Strengthen it to the intersection actually being a singleton. *}
    1.49  
    1.50  lemma decreasing_closed_nest_sing:
    1.51 -  fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
    1.52 +  fixes s :: "nat \<Rightarrow> 'a::complete_space set"
    1.53    assumes "\<forall>n. closed(s n)"
    1.54            "\<forall>n. s n \<noteq> {}"
    1.55            "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
    1.56 @@ -5864,10 +5858,6 @@
    1.57    ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
    1.58  qed
    1.59  
    1.60 -
    1.61 -(** TODO move this someplace else within this theory **)
    1.62 -instance euclidean_space \<subseteq> banach ..
    1.63 -
    1.64  declare tendsto_const [intro] (* FIXME: move *)
    1.65  
    1.66  end