X = trivial_topology rather than topspace X = {}

--- a/NEWS	Sat Jul 15 23:35:00 2023 +0100
+++ b/NEWS	Sun Jul 16 11:04:59 2023 +0100
@@ -334,6 +334,8 @@
 * Session "HOL-Analysis":
   - Some results reformulated to use f \<in> A\<rightarrow>B rather than f`A \<subseteq> B,
     INCOMPATIBILITY, use image_subset_iff_funcset to fix.
+  - Some results reformulated to use X = trivial_topology rather than
+    topspace X = {}, INCOMPATIBILITY, use null_topspace_iff_trivial to fix.
   - Imported the HOL Light abstract metric space library and numerous
     results in abstract topology (1200+ lemmas).
   - New material on infinite sums and integration, due to Manuel Eberl