diff -r 31f9ba85dc2e -r 501200635659 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jan 31 11:20:12 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Jan 31 11:31:22 2013 +0100 @@ -1,4 +1,3 @@ - header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} theory Cartesian_Euclidean_Space @@ -828,7 +827,7 @@ lemma compact_lemma_cart: fixes f :: "nat \ 'a::heine_borel ^ 'n" - assumes "bounded s" and "\n. f n \ s" + assumes f: "bounded (range f)" shows "\d. \l r. subseq r \ (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" @@ -842,16 +841,17 @@ thus ?case unfolding subseq_def by auto next case (insert k d) - have s': "bounded ((\x. x \$ k) ` s)" - using `bounded s` by (rule bounded_component_cart) obtain l1::"'a^'n" and r1 where r1:"subseq r1" and lr1:"\e>0. eventually (\n. \i\d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially" using insert(3) by auto - have f': "\n. f (r1 n) \$ k \ (\x. x \$ k) ` s" - using `\n. f n \ s` by simp - obtain l2 r2 where r2: "subseq r2" + have s': "bounded ((\x. x \$ k) ` range f)" using `bounded (range f)` + by (auto intro!: bounded_component_cart) + have f': "\n. f (r1 n) \$ k \ (\x. x \$ k) ` range f" by simp + have "bounded (range (\i. f (r1 i) \$ k))" + by (metis (lifting) bounded_subset image_subsetI f' s') + then obtain l2 r2 where r2: "subseq r2" and lr2: "((\i. f (r1 (r2 i)) \$ k) ---> l2) sequentially" - using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto + using bounded_imp_convergent_subsequence[of "\i. f (r1 i) \$ k"] by (auto simp: o_def) def r \ "r1 \ r2" have r: "subseq r" using r1 and r2 unfolding r_def o_def subseq_def by auto @@ -873,11 +873,11 @@ instance vec :: (heine_borel, finite) heine_borel proof - fix s :: "('a ^ 'b) set" and f :: "nat \ 'a ^ 'b" - assume s: "bounded s" and f: "\n. f n \ s" + fix f :: "nat \ 'a ^ 'b" + assume f: "bounded (range f)" then obtain l r where r: "subseq r" and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially" - using compact_lemma_cart [OF s f] by blast + using compact_lemma_cart [OF f] by blast let ?d = "UNIV::'b set" { fix e::real assume "e>0" hence "0 < e / (real_of_nat (card ?d))"