src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 66794 83bf64da6938
parent 66793 deabce3ccf1f
child 66827 c94531b5007d
equal deleted 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> {}"