Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed the theorem name "closed_imp_fip_compact"
authorpaulson <lp15@cam.ac.uk>
Mon, 09 Oct 2017 16:14:18 +0100
changeset 66794 83bf64da6938
parent 66793 deabce3ccf1f
child 66795 420d0080545f
Fixed the theorem name "closed_imp_fip_compact"
src/HOL/Analysis/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions 
--- 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;
isabelle