# HG changeset patch
# User huffman
# Date 1244672945 25200
# Node ID 88347c12e2674d1dbf445e8344e3893b4eccaf45
# Parent  ca9e56897403ac17e59b25b60ef75917b3085f21
heine_borel instance for products

diff -r ca9e56897403 -r 88347c12e267 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 10 11:54:00 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 10 15:29:05 2009 -0700
@@ -6,7 +6,7 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Euclidean_Space
+imports SEQ Euclidean_Space Product_Vector
 begin
 
 declare fstcart_pastecart[simp] sndcart_pastecart[simp]
@@ -2424,6 +2424,54 @@
   with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
 qed
 
+lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
+unfolding bounded_def
+apply clarify
+apply (rule_tac x="a" in exI)
+apply (rule_tac x="e" in exI)
+apply clarsimp
+apply (drule (1) bspec)
+apply (simp add: dist_Pair_Pair)
+apply (erule order_trans [OF real_sqrt_sum_squares_ge1])
+done
+
+lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
+unfolding bounded_def
+apply clarify
+apply (rule_tac x="b" in exI)
+apply (rule_tac x="e" in exI)
+apply clarsimp
+apply (drule (1) bspec)
+apply (simp add: dist_Pair_Pair)
+apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
+done
+
+instance "*" :: (heine_borel, heine_borel) heine_borel
+proof
+  fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b"
+  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+  from s have s1: "bounded (fst ` s)" by (rule bounded_fst)
+  from f have f1: "\<forall>n. fst (f n) \<in> fst ` s" by simp
+  obtain l1 r1 where r1: "subseq r1"
+    and l1: "((\<lambda>n. fst (f (r1 n))) ---> l1) sequentially"
+    using bounded_imp_convergent_subsequence [OF s1 f1]
+    unfolding o_def by fast
+  from s have s2: "bounded (snd ` s)" by (rule bounded_snd)
+  from f have f2: "\<forall>n. snd (f (r1 n)) \<in> snd ` s" by simp
+  obtain l2 r2 where r2: "subseq r2"
+    and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially"
+    using bounded_imp_convergent_subsequence [OF s2 f2]
+    unfolding o_def by fast
+  have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
+    using lim_subseq [OF r2 l1] unfolding o_def .
+  have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially"
+    using tendsto_Pair [OF l1' l2] unfolding o_def by simp
+  have r: "subseq (r1 \<circ> r2)"
+    using r1 r2 unfolding subseq_def by simp
+  show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+    using l r by fast
+qed
+
 subsection{* Completeness. *}
 
 lemma cauchy_def: