tweaked a definition
authorpaulson <lp15@cam.ac.uk>
Fri May 03 15:43:02 2019 +0100 (6 months ago)
changeset 70235b0680d8b0608
parent 70233 778366b0f519
child 70236 498ae040d47b
tweaked a definition
src/HOL/Analysis/Abstract_Topology.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Thu May 02 15:40:57 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri May 03 15:43:02 2019 +0100
     1.3 @@ -13,8 +13,7 @@
     1.4  subsection \<open>General notion of a topology as a value\<close>
     1.5  
     1.6  definition\<^marker>\<open>tag important\<close> istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
     1.7 -"istopology L \<longleftrightarrow>
     1.8 -  L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
     1.9 +  "istopology L \<equiv> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>\<K>. (\<forall>K\<in>\<K>. L K) \<longrightarrow> L (\<Union>\<K>))"
    1.10  
    1.11  typedef\<^marker>\<open>tag important\<close> 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    1.12    morphisms "openin" "topology"
    1.13 @@ -55,7 +54,7 @@
    1.14      "openin U {}"
    1.15      "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
    1.16      "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
    1.17 -  using openin[of U] unfolding istopology_def mem_Collect_eq by fast+
    1.18 +  using openin[of U] unfolding istopology_def by auto
    1.19  
    1.20  lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
    1.21    unfolding topspace_def by blast