src/HOL/Analysis/Abstract_Topology.thy

 
 lemma subtopology_eq_discrete_topology_sing:
    "X = discrete_topology {a} \<longleftrightarrow> topspace X = {a}"
   by (metis discrete_topology_unique openin_topspace singletonD)
 
+abbreviation trivial_topology where "trivial_topology \<equiv> discrete_topology {}"
+
+lemma null_topspace_iff_trivial [simp]: "topspace X = {} \<longleftrightarrow> X = trivial_topology"
+  by (simp add: subtopology_eq_discrete_topology_empty)
 
 subsection \<open>Subspace topology\<close>
 
 definition\<^marker>\<open>tag important\<close> subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" 
   where "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"

 
 lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
   unfolding openin_subtopology
   by auto (metis IntD1 in_mono openin_subset)
 
+lemma subtopology_trivial_iff: "subtopology X S = trivial_topology \<longleftrightarrow> X = trivial_topology \<or> topspace X \<inter> S = {}"
+  by (auto simp flip: null_topspace_iff_trivial)
+
 lemma subtopology_subtopology:
    "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
 proof -
   have eq: "\<And>T'. (\<exists>S'. T' = S' \<inter> T \<and> (\<exists>T. openin X T \<and> S' = T \<inter> S)) = (\<exists>Sa. T' = Sa \<inter> (S \<inter> T) \<and> openin X Sa)"
     by (metis inf_assoc)

   by (simp add: subtopology_superset)
 
 lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
   by (simp add: subtopology_superset)
 
+lemma subtopology_empty_iff_trivial [simp]: "subtopology X {} = trivial_topology"
+  by (simp add: subtopology_eq_discrete_topology_empty)
+
 lemma subtopology_restrict:
    "subtopology X (topspace X \<inter> S) = subtopology X S"
   by (metis subtopology_subtopology subtopology_topspace)
 
 lemma openin_subtopology_empty:

 
 lemma closedin_subtopology_refl [simp]:
   "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
   by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
 
-lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
+lemma closedin_topspace_empty [simp]: "closedin trivial_topology S \<longleftrightarrow> S = {}"
   by (simp add: closedin_def)
 
-lemma open_in_topspace_empty:
-   "topspace X = {} \<Longrightarrow> openin X S \<longleftrightarrow> S = {}"
+lemma openin_topspace_empty [simp]:
+   "openin trivial_topology S \<longleftrightarrow> S = {}"
   by (simp add: openin_closedin_eq)
 
 lemma openin_imp_subset:
   "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
   by (metis Int_iff openin_subtopology subsetI)

 
 declare closed_closedin [symmetric, simp]
 
 lemma openin_subtopology_self [simp]: "openin (top_of_set S) S"
   by (metis openin_topspace topspace_euclidean_subtopology)
+
+lemma euclidean_nontrivial [simp]: "euclidean \<noteq> trivial_topology"
+  by (simp add: subtopology_eq_discrete_topology_empty)
+
 
 subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>
 
 abbreviation euclideanreal :: "real topology"
   where "euclideanreal \<equiv> topology open"

 
 lemma continuous_map_funspace:
    "continuous_map X Y f \<Longrightarrow> f \<in> topspace X \<rightarrow> topspace Y"
   by (auto simp: continuous_map_def)
 
-lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
+lemma continuous_map_on_empty [simp]: "continuous_map trivial_topology Y f"
   by (auto simp: continuous_map_def)
 
-lemma continuous_map_on_empty2: "topspace Y = {} \<Longrightarrow> continuous_map X Y f \<longleftrightarrow> topspace X = {}"
-  by (auto simp: continuous_map_def)
+lemma continuous_map_on_empty2 [simp]: "continuous_map X trivial_topology f \<longleftrightarrow> X = trivial_topology"
+  using continuous_map_image_subset_topspace by fastforce
 
 lemma continuous_map_closedin:
    "continuous_map X Y f \<longleftrightarrow>
          f \<in> topspace X \<rightarrow> topspace Y \<and>
          (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"

     unfolding continuous_map_def
     using assms openin_subopen topspace_def by fastforce
 qed
 
 lemma continuous_map_const [simp]:
-   "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
-proof (cases "topspace X = {}")
-  case False
+   "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> X = trivial_topology \<or> C \<in> topspace Y"
+proof (cases "X = trivial_topology")
+  case nontriv: False
   show ?thesis
   proof (cases "C \<in> topspace Y")
     case True
     with openin_subopen show ?thesis
       by (auto simp: continuous_map_def)
   next
     case False
-    then show ?thesis
-      unfolding continuous_map_def by fastforce
-  qed
-qed (auto simp: continuous_map_on_empty)
+    with nontriv show ?thesis
+      using continuous_map_image_subset_topspace discrete_topology_unique image_subset_iff by fastforce 
+  qed
+qed auto
 
 declare continuous_map_const [THEN iffD2, continuous_intros]
 
 lemma continuous_map_compose [continuous_intros]:
   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"

 
 lemma open_map_imp_subset_topspace:
      "open_map X1 X2 f \<Longrightarrow> f \<in> (topspace X1) \<rightarrow> topspace X2"
   unfolding open_map_def using openin_subset by fastforce
 
-lemma open_map_on_empty:
-   "topspace X = {} \<Longrightarrow> open_map X Y f"
-  by (metis empty_iff imageE in_mono open_map_def openin_subopen openin_subset)
+lemma open_map_on_empty [simp]: "open_map trivial_topology Y f"
+  by (simp add: open_map_def)
 
 lemma closed_map_on_empty:
-   "topspace X = {} \<Longrightarrow> closed_map X Y f"
+   "closed_map trivial_topology Y f"
   by (simp add: closed_map_def closedin_topspace_empty)
 
 lemma closed_map_const:
-   "closed_map X Y (\<lambda>x. c) \<longleftrightarrow> topspace X = {} \<or> closedin Y {c}"
-  by (metis closed_map_def closed_map_on_empty closedin_empty closedin_topspace image_constant_conv)
+   "closed_map X Y (\<lambda>x. c) \<longleftrightarrow> X = trivial_topology \<or> closedin Y {c}"
+  by (metis closed_map_def closed_map_on_empty closedin_topspace discrete_topology_unique equals0D image_constant_conv)
 
 lemma open_map_imp_subset:
     "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f \<in> S \<rightarrow> topspace X2"
   using open_map_imp_subset_topspace by fastforce
 

      "homeomorphic_map X Y f \<Longrightarrow> X homeomorphic_space Y"
   unfolding homeomorphic_map_maps
   using homeomorphic_space_def by blast
 
 lemma homeomorphic_empty_space:
-     "X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
-  by (metis homeomorphic_eq_everything_map homeomorphic_space image_is_empty)
+     "X homeomorphic_space Y \<Longrightarrow> X = trivial_topology \<longleftrightarrow> Y = trivial_topology"
+  by (meson continuous_map_on_empty2 homeomorphic_maps_def homeomorphic_space_def)
 
 lemma homeomorphic_empty_space_eq:
-  assumes "topspace X = {}"
-  shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
-  using assms
-  by (auto simp: homeomorphic_maps_def homeomorphic_space_def continuous_map_def)
+  assumes "X = trivial_topology"
+  shows "X homeomorphic_space Y \<longleftrightarrow> Y = trivial_topology"
+  using assms funcset_mem
+  by (fastforce simp:  homeomorphic_maps_def homeomorphic_space_def continuous_map_def)
 
 lemma homeomorphic_space_unfold:
   assumes "X homeomorphic_space Y"
   obtains f g where  "homeomorphic_map X Y f"  "homeomorphic_map Y X g"
     and "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> topspace Y \<Longrightarrow> f(g y) = y"

 qed
 
 lemma connectedin_empty [simp]: "connectedin X {}"
   by (simp add: connectedin)
 
-lemma connected_space_topspace_empty:
-     "topspace X = {} \<Longrightarrow> connected_space X"
+lemma connected_space_trivial_topology [simp]: "connected_space trivial_topology"
   using connectedin_topspace by fastforce
 
 lemma connectedin_sing [simp]: "connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
   by (simp add: connectedin)
 

   by (metis compactin_subspace compact_space finite_UnionD inf.absorb_iff2 order_refl topspace_subtopology)
 
 lemma compactin_empty [iff]: "compactin X {}"
   by (simp add: finite_imp_compactin)
 
-lemma compact_space_topspace_empty:
-   "topspace X = {} \<Longrightarrow> compact_space X"
+lemma compact_space_trivial_topology [simp]: "compact_space trivial_topology"
   by (simp add: compact_space_def)
 
 lemma finite_imp_compactin_eq:
    "finite S \<Longrightarrow> (compactin X S \<longleftrightarrow> S \<subseteq> topspace X)"
   using compactin_subset_topspace finite_imp_compactin by blast

 
 proposition compact_space_fip:
    "compact_space X \<longleftrightarrow>
     (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
    (is "_ = ?rhs")
-proof (cases "topspace X = {}")
+proof (cases "X = trivial_topology")
   case True
   then show ?thesis
-    unfolding compact_space_def
-    by (metis Sup_bot_conv(1) closedin_topspace_empty compactin_empty finite.emptyI finite_UnionD order_refl)
+    by (metis Pow_iff closedin_topspace_empty compact_space_trivial_topology finite.emptyI finite_Pow_iff finite_subset subsetI)
 next
   case False
   show ?thesis
   proof safe
     fix \<U> :: "'a set set"

       by (auto simp: \<V>_def)
     moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
     ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
       by (auto simp: ex_finite_subset_image \<V>_def)
     moreover have "\<F> \<noteq> {}"
-      using \<F> \<open>topspace X \<noteq> {}\<close> by blast
+      using \<F> False by force
     ultimately show "False"
       using * [of \<F>]
       by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
   next
     assume R [rule_format]: ?rhs

       unfolding compact_space_alt
     proof clarify
       fix \<U> :: "'a set set"
       define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
       assume "\<forall>C\<in>\<U>. openin X C" and "topspace X \<subseteq> \<Union>\<U>"
-      with \<open>topspace X \<noteq> {}\<close> have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
+      with False have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
         by (auto simp: \<V>_def)
       show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>"
       proof (rule ccontr; simp)
         assume "\<forall>\<F>\<subseteq>\<U>. finite \<F> \<longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>"
         then have "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<V> \<longrightarrow> \<Inter>\<F> \<noteq> {}"

     with f show ?thesis
       by (auto simp: proper_map_def)
   qed
 qed (simp add: proper_imp_closed_map)
 
-lemma proper_map_on_empty:
-   "topspace X = {} \<Longrightarrow> proper_map X Y f"
+lemma proper_map_on_empty [simp]: "proper_map trivial_topology Y f"
   by (auto simp: proper_map_def closed_map_on_empty)
 
 lemma proper_map_id [simp]:
    "proper_map X X id"
 proof (clarsimp simp: proper_map_alt closed_map_id)

       using f [OF g [OF that]] by auto
   qed
 qed
 
 lemma proper_map_const:
-   "proper_map X Y (\<lambda>x. c) \<longleftrightarrow> compact_space X \<and> (topspace X = {} \<or> closedin Y {c})"
-proof (cases "topspace X = {}")
+   "proper_map X Y (\<lambda>x. c) \<longleftrightarrow> compact_space X \<and> (X = trivial_topology \<or> closedin Y {c})"
+proof (cases "X = trivial_topology")
   case True
   then show ?thesis
-    by (simp add: compact_space_topspace_empty proper_map_on_empty)
+    by simp
 next
   case False
   have *: "compactin X {x \<in> topspace X. c = y}" if "compact_space X" for y
     using that unfolding compact_space_def
     by (metis (mono_tags, lifting) compactin_empty empty_subsetI mem_Collect_eq subsetI subset_antisym)