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