src/HOL/Analysis/Topology_Euclidean_Space.thy
 changeset 66794 83bf64da6938 parent 66793 deabce3ccf1f child 66827 c94531b5007d
equal inserted replaced
66793:deabce3ccf1f 66794:83bf64da6938
` 10749      apply (simp add: clof)`
` 10749      apply (simp add: clof)`
` 10750     by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)`
` 10750     by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)`
` 10751   then show ?thesis by blast`
` 10751   then show ?thesis by blast`
` 10752 qed`
` 10752 qed`
` 10753 `
` 10753 `
` 10754 lemma clconnected_closedin_eqosed_imp_fip_compact:`
` 10754 lemma closed_imp_fip_compact:`
` 10755   fixes S :: "'a::heine_borel set"`
` 10755   fixes S :: "'a::heine_borel set"`
` 10756   shows`
` 10756   shows`
` 10757    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;`
` 10757    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;`
` 10758      \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>`
` 10758      \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>`
` 10759         \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"`
` 10759         \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"`