equal
deleted
inserted
replaced
955 done |
955 done |
956 |
956 |
957 lemma compact_lemma_cart: |
957 lemma compact_lemma_cart: |
958 fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n" |
958 fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n" |
959 assumes f: "bounded (range f)" |
959 assumes f: "bounded (range f)" |
960 shows "\<exists>l r. subseq r \<and> |
960 shows "\<exists>l r. strict_mono r \<and> |
961 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
961 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
962 (is "?th d") |
962 (is "?th d") |
963 proof - |
963 proof - |
964 have "\<forall>d' \<subseteq> d. ?th d'" |
964 have "\<forall>d' \<subseteq> d. ?th d'" |
965 by (rule compact_lemma_general[where unproj=vec_lambda]) |
965 by (rule compact_lemma_general[where unproj=vec_lambda]) |
969 |
969 |
970 instance vec :: (heine_borel, finite) heine_borel |
970 instance vec :: (heine_borel, finite) heine_borel |
971 proof |
971 proof |
972 fix f :: "nat \<Rightarrow> 'a ^ 'b" |
972 fix f :: "nat \<Rightarrow> 'a ^ 'b" |
973 assume f: "bounded (range f)" |
973 assume f: "bounded (range f)" |
974 then obtain l r where r: "subseq r" |
974 then obtain l r where r: "strict_mono r" |
975 and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially" |
975 and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially" |
976 using compact_lemma_cart [OF f] by blast |
976 using compact_lemma_cart [OF f] by blast |
977 let ?d = "UNIV::'b set" |
977 let ?d = "UNIV::'b set" |
978 { fix e::real assume "e>0" |
978 { fix e::real assume "e>0" |
979 hence "0 < e / (real_of_nat (card ?d))" |
979 hence "0 < e / (real_of_nat (card ?d))" |
991 } |
991 } |
992 ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially" |
992 ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially" |
993 by (rule eventually_mono) |
993 by (rule eventually_mono) |
994 } |
994 } |
995 hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp |
995 hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp |
996 with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto |
996 with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto |
997 qed |
997 qed |
998 |
998 |
999 lemma interval_cart: |
999 lemma interval_cart: |
1000 fixes a :: "real^'n" |
1000 fixes a :: "real^'n" |
1001 shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" |
1001 shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" |