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:
```