Fixed the theorem name "closed_imp_fip_compact"
authorpaulson <lp15@cam.ac.uk>
Mon Oct 09 16:14:18 2017 +0100 (19 months ago)
changeset 6679483bf64da6938
parent 66793 deabce3ccf1f
child 66795 420d0080545f
Fixed the theorem name "closed_imp_fip_compact"
src/HOL/Analysis/Topology_Euclidean_Space.thy
     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;