moved lemma
authornipkow
Wed Nov 06 17:38:19 2019 +0100 (8 days ago ago)
changeset 71262d628bbdce79a
parent 71260 b3956a37c994
child 71263 98ac9a4323a2
child 71264 114db2b5a5f8
moved lemma
src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Nov 06 16:38:58 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Nov 06 17:38:19 2019 +0100
     1.3 @@ -16,11 +16,6 @@
     1.4  
     1.5  section \<open>Elementary Topology\<close>
     1.6  
     1.7 -subsection \<open>TODO: move?\<close>
     1.8 -
     1.9 -lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
    1.10 -  using openI by auto
    1.11 -
    1.12  
    1.13  subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>
    1.14  
    1.15 @@ -49,7 +44,6 @@
    1.16    by (simp add: field_simps)
    1.17  
    1.18  
    1.19 -
    1.20  subsection \<open>Topological Basis\<close>
    1.21  
    1.22  context topological_space
     2.1 --- a/src/HOL/Topological_Spaces.thy	Wed Nov 06 16:38:58 2019 +0100
     2.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Nov 06 17:38:19 2019 +0100
     2.3 @@ -49,6 +49,9 @@
     2.4    ultimately show "open S" by simp
     2.5  qed
     2.6  
     2.7 +lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
     2.8 +by (auto intro: openI)
     2.9 +
    2.10  lemma closed_empty [continuous_intros, intro, simp]: "closed {}"
    2.11    unfolding closed_def by simp
    2.12