diff -r fc78714d14e1 -r 43e8d4bfde26 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 15:00:37 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 15:46:14 2009 -0700 @@ -2720,16 +2720,30 @@ qed lemma compact_imp_bounded: - fixes s :: "(real^ _) set" + fixes s :: "'a::real_normed_vector set" (* TODO: generalize to metric_space *) shows "compact s ==> bounded s" - unfolding compact_eq_bounded_closed - by simp +proof - + assume "compact s" + hence "\f. (\t\f. open t) \ s \ \f \ (\f'\f. finite f' \ s \ \f')" + by (rule compact_imp_heine_borel) + hence "\t. infinite t \ t \ s \ (\x \ s. x islimpt t)" + using heine_borel_imp_bolzano_weierstrass[of s] by auto + thus "bounded s" + by (rule bolzano_weierstrass_imp_bounded) +qed lemma compact_imp_closed: - fixes s :: "(real ^ _) set" + fixes s :: "'a::metric_space set" shows "compact s ==> closed s" - unfolding compact_eq_bounded_closed - by simp +proof - + assume "compact s" + hence "\f. (\t\f. open t) \ s \ \f \ (\f'\f. finite f' \ s \ \f')" + by (rule compact_imp_heine_borel) + hence "\t. infinite t \ t \ s \ (\x \ s. x islimpt t)" + using heine_borel_imp_bolzano_weierstrass[of s] by auto + thus "closed s" + by (rule bolzano_weierstrass_imp_closed) +qed text{* In particular, some common special cases. *}