src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
 changeset 50998 501200635659 parent 50526 899c9c4e4a4c child 51489 f738e6dbd844
```     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 31 11:20:12 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 31 11:31:22 2013 +0100
1.3 @@ -1,4 +1,3 @@
1.4 -
1.5  header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
1.6
1.7  theory Cartesian_Euclidean_Space
1.8 @@ -828,7 +827,7 @@
1.9
1.10  lemma compact_lemma_cart:
1.11    fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
1.12 -  assumes "bounded s" and "\<forall>n. f n \<in> s"
1.13 +  assumes f: "bounded (range f)"
1.14    shows "\<forall>d.
1.15          \<exists>l r. subseq r \<and>
1.16          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)"
1.17 @@ -842,16 +841,17 @@
1.18      thus ?case unfolding subseq_def by auto
1.19    next
1.20      case (insert k d)
1.21 -    have s': "bounded ((\<lambda>x. x \$ k) ` s)"
1.22 -      using `bounded s` by (rule bounded_component_cart)
1.23      obtain l1::"'a^'n" and r1 where r1:"subseq r1"
1.24        and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially"
1.25        using insert(3) by auto
1.26 -    have f': "\<forall>n. f (r1 n) \$ k \<in> (\<lambda>x. x \$ k) ` s"
1.27 -      using `\<forall>n. f n \<in> s` by simp
1.28 -    obtain l2 r2 where r2: "subseq r2"
1.29 +    have s': "bounded ((\<lambda>x. x \$ k) ` range f)" using `bounded (range f)`
1.30 +      by (auto intro!: bounded_component_cart)
1.31 +    have f': "\<forall>n. f (r1 n) \$ k \<in> (\<lambda>x. x \$ k) ` range f" by simp
1.32 +    have "bounded (range (\<lambda>i. f (r1 i) \$ k))"
1.33 +      by (metis (lifting) bounded_subset image_subsetI f' s')
1.34 +    then obtain l2 r2 where r2: "subseq r2"
1.35        and lr2: "((\<lambda>i. f (r1 (r2 i)) \$ k) ---> l2) sequentially"
1.36 -      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
1.37 +      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \$ k"] by (auto simp: o_def)
1.38      def r \<equiv> "r1 \<circ> r2"
1.39      have r: "subseq r"
1.40        using r1 and r2 unfolding r_def o_def subseq_def by auto
1.41 @@ -873,11 +873,11 @@
1.42
1.43  instance vec :: (heine_borel, finite) heine_borel
1.44  proof
1.45 -  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
1.46 -  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
1.47 +  fix f :: "nat \<Rightarrow> 'a ^ 'b"
1.48 +  assume f: "bounded (range f)"
1.49    then obtain l r where r: "subseq r"
1.50        and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially"
1.51 -    using compact_lemma_cart [OF s f] by blast
1.52 +    using compact_lemma_cart [OF f] by blast
1.53    let ?d = "UNIV::'b set"
1.54    { fix e::real assume "e>0"
1.55      hence "0 < e / (real_of_nat (card ?d))"
```