src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 66447 a1f5c5c26fa6
parent 64267 b9a1486e79be
child 66804 3f9bb52082c4
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -957,7 +957,7 @@
     1.4  lemma compact_lemma_cart:
     1.5    fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
     1.6    assumes f: "bounded (range f)"
     1.7 -  shows "\<exists>l r. subseq r \<and>
     1.8 +  shows "\<exists>l r. strict_mono r \<and>
     1.9          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
    1.10      (is "?th d")
    1.11  proof -
    1.12 @@ -971,7 +971,7 @@
    1.13  proof
    1.14    fix f :: "nat \<Rightarrow> 'a ^ 'b"
    1.15    assume f: "bounded (range f)"
    1.16 -  then obtain l r where r: "subseq r"
    1.17 +  then obtain l r where r: "strict_mono r"
    1.18        and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
    1.19      using compact_lemma_cart [OF f] by blast
    1.20    let ?d = "UNIV::'b set"
    1.21 @@ -993,7 +993,7 @@
    1.22        by (rule eventually_mono)
    1.23    }
    1.24    hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp
    1.25 -  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
    1.26 +  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
    1.27  qed
    1.28  
    1.29  lemma interval_cart: