818 done |
818 done |
819 |
819 |
820 lemma compact_lemma_cart: |
820 lemma compact_lemma_cart: |
821 fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n" |
821 fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n" |
822 assumes f: "bounded (range f)" |
822 assumes f: "bounded (range f)" |
823 shows "\<forall>d. |
823 shows "\<exists>l r. subseq r \<and> |
824 \<exists>l r. subseq r \<and> |
|
825 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
824 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
826 proof |
825 (is "?th d") |
827 fix d :: "'n set" |
826 proof - |
828 have "finite d" by simp |
827 have "\<forall>d' \<subseteq> d. ?th d'" |
829 thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and> |
828 by (rule compact_lemma_general[where unproj=vec_lambda]) |
830 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
829 (auto intro!: f bounded_component_cart simp: vec_lambda_eta) |
831 proof (induct d) |
830 then show "?th d" by simp |
832 case empty |
|
833 thus ?case unfolding subseq_def by auto |
|
834 next |
|
835 case (insert k d) |
|
836 obtain l1::"'a^'n" and r1 where r1:"subseq r1" |
|
837 and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" |
|
838 using insert(3) by auto |
|
839 have s': "bounded ((\<lambda>x. x $ k) ` range f)" using \<open>bounded (range f)\<close> |
|
840 by (auto intro!: bounded_component_cart) |
|
841 have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp |
|
842 have "bounded (range (\<lambda>i. f (r1 i) $ k))" |
|
843 by (metis (lifting) bounded_subset image_subsetI f' s') |
|
844 then obtain l2 r2 where r2: "subseq r2" |
|
845 and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) \<longlongrightarrow> l2) sequentially" |
|
846 using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def) |
|
847 def r \<equiv> "r1 \<circ> r2" |
|
848 have r: "subseq r" |
|
849 using r1 and r2 unfolding r_def o_def subseq_def by auto |
|
850 moreover |
|
851 def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n" |
|
852 { fix e :: real assume "e > 0" |
|
853 from lr1 \<open>e>0\<close> have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" |
|
854 by blast |
|
855 from lr2 \<open>e>0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" |
|
856 by (rule tendstoD) |
|
857 from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially" |
|
858 by (rule eventually_subseq) |
|
859 have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially" |
|
860 using N1' N2 by (rule eventually_elim2, simp add: l_def r_def) |
|
861 } |
|
862 ultimately show ?case by auto |
|
863 qed |
|
864 qed |
831 qed |
865 |
832 |
866 instance vec :: (heine_borel, finite) heine_borel |
833 instance vec :: (heine_borel, finite) heine_borel |
867 proof |
834 proof |
868 fix f :: "nat \<Rightarrow> 'a ^ 'b" |
835 fix f :: "nat \<Rightarrow> 'a ^ 'b" |