equal
deleted
inserted
replaced
3796 |
3796 |
3797 instance prod :: (heine_borel, heine_borel) heine_borel |
3797 instance prod :: (heine_borel, heine_borel) heine_borel |
3798 proof |
3798 proof |
3799 fix f :: "nat \<Rightarrow> 'a \<times> 'b" |
3799 fix f :: "nat \<Rightarrow> 'a \<times> 'b" |
3800 assume f: "bounded (range f)" |
3800 assume f: "bounded (range f)" |
3801 from f have s1: "bounded (range (fst \<circ> f))" |
3801 then have "bounded (fst ` range f)" |
3802 unfolding image_comp by (rule bounded_fst) |
3802 by (rule bounded_fst) |
|
3803 then have s1: "bounded (range (fst \<circ> f))" |
|
3804 by (simp add: image_comp) |
3803 obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1" |
3805 obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1" |
3804 using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast |
3806 using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast |
3805 from f have s2: "bounded (range (snd \<circ> f \<circ> r1))" |
3807 from f have s2: "bounded (range (snd \<circ> f \<circ> r1))" |
3806 by (auto simp add: image_comp intro: bounded_snd bounded_subset) |
3808 by (auto simp add: image_comp intro: bounded_snd bounded_subset) |
3807 obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially" |
3809 obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially" |