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))"