| changeset 71063 | d628bbdce79a |
| parent 70749 | 5d06b7bb9d22 |
| child 71827 | 5e315defb038 |
--- a/src/HOL/Topological_Spaces.thy Wed Nov 06 16:38:58 2019 +0100 +++ b/src/HOL/Topological_Spaces.thy Wed Nov 06 17:38:19 2019 +0100 @@ -49,6 +49,9 @@ ultimately show "open S" by simp qed +lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" +by (auto intro: openI) + lemma closed_empty [continuous_intros, intro, simp]: "closed {}" unfolding closed_def by simp