src/HOL/Library/Topology_Euclidean_Space.thy
 changeset 31532 43e8d4bfde26 parent 31531 fc78714d14e1 child 31533 2cce9283ba72
equal inserted replaced
31531:fc78714d14e1 31532:43e8d4bfde26
`  2718 next`
`  2718 next`
`  2719   assume ?rhs thus ?lhs using bounded_closed_imp_compact by auto`
`  2719   assume ?rhs thus ?lhs using bounded_closed_imp_compact by auto`
`  2720 qed`
`  2720 qed`
`  2721 `
`  2721 `
`  2722 lemma compact_imp_bounded:`
`  2722 lemma compact_imp_bounded:`
`  2723   fixes s :: "(real^ _) set"`
`  2723   fixes s :: "'a::real_normed_vector set" (* TODO: generalize to metric_space *)`
`  2724   shows "compact s ==> bounded s"`
`  2724   shows "compact s ==> bounded s"`
`  2725   unfolding compact_eq_bounded_closed`
`  2725 proof -`
`  2726   by simp`
`  2726   assume "compact s"`
`       `
`  2727   hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"`
`       `
`  2728     by (rule compact_imp_heine_borel)`
`       `
`  2729   hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"`
`       `
`  2730     using heine_borel_imp_bolzano_weierstrass[of s] by auto`
`       `
`  2731   thus "bounded s"`
`       `
`  2732     by (rule bolzano_weierstrass_imp_bounded)`
`       `
`  2733 qed`
`  2727 `
`  2734 `
`  2728 lemma compact_imp_closed:`
`  2735 lemma compact_imp_closed:`
`  2729   fixes s :: "(real ^ _) set"`
`  2736   fixes s :: "'a::metric_space set"`
`  2730   shows "compact s ==> closed s"`
`  2737   shows "compact s ==> closed s"`
`  2731   unfolding compact_eq_bounded_closed`
`  2738 proof -`
`  2732   by simp`
`  2739   assume "compact s"`
`       `
`  2740   hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"`
`       `
`  2741     by (rule compact_imp_heine_borel)`
`       `
`  2742   hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"`
`       `
`  2743     using heine_borel_imp_bolzano_weierstrass[of s] by auto`
`       `
`  2744   thus "closed s"`
`       `
`  2745     by (rule bolzano_weierstrass_imp_closed)`
`       `
`  2746 qed`
`  2733 `
`  2747 `
`  2734 text{* In particular, some common special cases. *}`
`  2748 text{* In particular, some common special cases. *}`
`  2735 `
`  2749 `
`  2736 lemma compact_empty[simp]:`
`  2750 lemma compact_empty[simp]:`
`  2737  "compact {}"`
`  2751  "compact {}"`