src/HOL/Analysis/Connected.thy
changeset 71137 3c0a26b8b49a
parent 70136 f03a01a18c6e
child 71172 575b3a818de5
--- a/src/HOL/Analysis/Connected.thy	Fri Nov 15 16:44:09 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy	Fri Nov 15 21:09:03 2019 +0100
@@ -569,9 +569,9 @@
 qed
 
 
+subsection\<open>Lemmas about components\<close>
 
-subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
-
+text  \<open>See Newman IV, 3.3 and 3.4.\<close>
 
 lemma connected_Un_clopen_in_complement:
   fixes S U :: "'a::metric_space set"