--- a/src/HOL/Analysis/Elementary_Topology.thy Wed Nov 06 16:38:58 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Wed Nov 06 17:38:19 2019 +0100
@@ -16,11 +16,6 @@
section \<open>Elementary Topology\<close>
-subsection \<open>TODO: move?\<close>
-
-lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
- using openI by auto
-
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>
@@ -49,7 +44,6 @@
by (simp add: field_simps)
-
subsection \<open>Topological Basis\<close>
context topological_space
--- 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