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"