# HG changeset patch
# User traytel
# Date 1573071823 -3600
# Node ID 98ac9a4323a2faa3944f71d7aaea73124fe9c3e9
# Parent  c9c1a64eeb6912591422beb9b9b679a85fafaefd# Parent  d628bbdce79a1978e13155fd78f1cfeebb11c163
merged

diff -r c9c1a64eeb69 -r 98ac9a4323a2 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Nov 06 16:57:51 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Nov 06 21:23:43 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
diff -r c9c1a64eeb69 -r 98ac9a4323a2 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Nov 06 16:57:51 2019 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Nov 06 21:23:43 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