diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Jul 12 23:11:59 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sat Jul 15 23:34:42 2023 +0100
@@ -227,6 +227,10 @@
    "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>
 
@@ -316,6 +320,9 @@
   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 -
@@ -356,6 +363,9 @@
 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)
@@ -372,11 +382,11 @@
   "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:
@@ -441,6 +451,10 @@
 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"
@@ -1470,11 +1484,11 @@
    "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>
@@ -1633,9 +1647,9 @@
 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
@@ -1643,10 +1657,10 @@
       by (auto simp: continuous_map_def)
   next
     case False
-    then show ?thesis
-      unfolding continuous_map_def by fastforce
+    with nontriv show ?thesis
+      using continuous_map_image_subset_topspace discrete_topology_unique image_subset_iff by fastforce 
   qed
-qed (auto simp: continuous_map_on_empty)
+qed auto
 
 declare continuous_map_const [THEN iffD2, continuous_intros]
 
@@ -1788,17 +1802,16 @@
      "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"
@@ -3063,14 +3076,14 @@
   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"
@@ -3193,8 +3206,7 @@
 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"
@@ -3558,8 +3570,7 @@
 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:
@@ -3705,11 +3716,10 @@
    "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
@@ -3724,7 +3734,7 @@
     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)
@@ -3736,7 +3746,7 @@
       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)
@@ -4965,8 +4975,7 @@
   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]:
@@ -5001,11 +5010,11 @@
 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