# HG changeset patch
# User nipkow
# Date 1573058299 -3600
# Node ID d628bbdce79a1978e13155fd78f1cfeebb11c163
# Parent  b3956a37c99476571bfda9312da927dfdfdcb6b1
moved lemma

diff -r b3956a37c994 -r d628bbdce79a src/HOL/Analysis/Elementary_Topology.thy
--- 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
diff -r b3956a37c994 -r d628bbdce79a src/HOL/Topological_Spaces.thy
--- 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