src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 66794 83bf64da6938
parent 66793 deabce3ccf1f
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 09 15:34:23 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 09 16:14:18 2017 +0100
     1.3 @@ -10751,7 +10751,7 @@
     1.4    then show ?thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma clconnected_closedin_eqosed_imp_fip_compact:
     1.8 +lemma closed_imp_fip_compact:
     1.9    fixes S :: "'a::heine_borel set"
    1.10    shows
    1.11     "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;