# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1539782347 -3600
# Node ID f13b82281715b09ca46a571a68bf7d57ba1ebe20
# Parent  5acb1eece41bbc3fb66147a488f9f531ee648be2
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml

diff -r 5acb1eece41b -r f13b82281715 src/HOL/Analysis/Abstract_Topology.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -0,0 +1,2884 @@
+(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light]
+*)
+
+section \<open>Operators involving abstract topology\<close>
+
+theory Abstract_Topology
+  imports Topology_Euclidean_Space Path_Connected
+begin
+
+
+subsection\<open>Derived set (set of limit points)\<close>
+
+definition derived_set_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "derived'_set'_of" 80)
+  where "X derived_set_of S \<equiv>
+         {x \<in> topspace X.
+                (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
+
+lemma derived_set_of_restrict:
+   "X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
+  by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
+
+lemma in_derived_set_of:
+   "x \<in> X derived_set_of S \<longleftrightarrow> x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))"
+  by (simp add: derived_set_of_def)
+
+lemma derived_set_of_subset_topspace:
+   "X derived_set_of S \<subseteq> topspace X"
+  by (auto simp add: derived_set_of_def)
+
+lemma derived_set_of_subtopology:
+   "(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
+  by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast
+
+lemma derived_set_of_subset_subtopology:
+   "(subtopology X S) derived_set_of T \<subseteq> S"
+  by (simp add: derived_set_of_subtopology)
+
+lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}"
+  by (auto simp: derived_set_of_def)
+
+lemma derived_set_of_mono:
+   "S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
+  unfolding derived_set_of_def by blast
+
+lemma derived_set_of_union:
+   "X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (clarsimp simp: in_derived_set_of)
+    by (metis IntE IntI openin_Int)
+  show "?rhs \<subseteq> ?lhs"
+    by (simp add: derived_set_of_mono)
+qed
+
+lemma derived_set_of_unions:
+   "finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
+proof (induction \<F> rule: finite_induct)
+  case (insert S \<F>)
+  then show ?case
+    by (simp add: derived_set_of_union)
+qed auto
+
+lemma derived_set_of_topspace:
+  "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
+  apply (auto simp: in_derived_set_of)
+  by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)
+
+lemma discrete_topology_unique_derived_set:
+     "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
+  by (auto simp: discrete_topology_unique derived_set_of_topspace)
+
+lemma subtopology_eq_discrete_topology_eq:
+   "subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
+  using discrete_topology_unique_derived_set [of U "subtopology X U"]
+  by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)
+
+lemma subtopology_eq_discrete_topology:
+   "S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
+        \<Longrightarrow> subtopology X S = discrete_topology S"
+  by (simp add: subtopology_eq_discrete_topology_eq)
+
+lemma subtopology_eq_discrete_topology_gen:
+   "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
+  by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
+
+lemma openin_Int_derived_set_of_subset:
+   "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
+  by (auto simp: derived_set_of_def)
+
+lemma openin_Int_derived_set_of_eq:
+  "openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
+  apply auto
+   apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
+  by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)
+
+
+subsection\<open> Closure with respect to a topological space\<close>
+
+definition closure_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "closure'_of" 80)
+  where "X closure_of S \<equiv> {x \<in> topspace X. \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y \<in> S. y \<in> T)}"
+
+lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
+  unfolding closure_of_def
+  apply safe
+  apply (meson IntI openin_subset subset_iff)
+  by auto
+
+lemma in_closure_of:
+   "x \<in> X closure_of S \<longleftrightarrow>
+    x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
+  by (auto simp: closure_of_def)
+
+lemma closure_of: "X closure_of S = topspace X \<inter> (S \<union> X derived_set_of S)"
+  by (fastforce simp: in_closure_of in_derived_set_of)
+
+lemma closure_of_alt: "X closure_of S = topspace X \<inter> S \<union> X derived_set_of S"
+  using derived_set_of_subset_topspace [of X S]
+  unfolding closure_of_def in_derived_set_of
+  by safe (auto simp: in_derived_set_of)
+
+lemma derived_set_of_subset_closure_of:
+   "X derived_set_of S \<subseteq> X closure_of S"
+  by (fastforce simp: closure_of_def in_derived_set_of)
+
+lemma closure_of_subtopology:
+  "(subtopology X U) closure_of S = U \<inter> (X closure_of (U \<inter> S))"
+  unfolding closure_of_def topspace_subtopology openin_subtopology
+  by safe (metis (full_types) IntI Int_iff inf.commute)+
+
+lemma closure_of_empty [simp]: "X closure_of {} = {}"
+  by (simp add: closure_of_alt)
+
+lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"
+  by (simp add: closure_of)
+
+lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"
+  by (simp add: closure_of)
+
+lemma closure_of_subset_topspace: "X closure_of S \<subseteq> topspace X"
+  by (simp add: closure_of)
+
+lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T \<subseteq> S"
+  by (simp add: closure_of_subtopology)
+
+lemma closure_of_mono: "S \<subseteq> T \<Longrightarrow> X closure_of S \<subseteq> X closure_of T"
+  by (fastforce simp add: closure_of_def)
+
+lemma closure_of_subtopology_subset:
+   "(subtopology X U) closure_of S \<subseteq> (X closure_of S)"
+  unfolding closure_of_subtopology
+  by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2)
+
+lemma closure_of_subtopology_mono:
+   "T \<subseteq> U \<Longrightarrow> (subtopology X T) closure_of S \<subseteq> (subtopology X U) closure_of S"
+  unfolding closure_of_subtopology
+  by auto (meson closure_of_mono inf_mono subset_iff)
+
+lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
+  by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_union inf_sup_distrib1)
+
+lemma closure_of_Union:
+   "finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
+by (induction \<F> rule: finite_induct) auto
+
+lemma closure_of_subset: "S \<subseteq> topspace X \<Longrightarrow> S \<subseteq> X closure_of S"
+  by (auto simp: closure_of_def)
+
+lemma closure_of_subset_Int: "topspace X \<inter> S \<subseteq> X closure_of S"
+  by (auto simp: closure_of_def)
+
+lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
+proof (cases "S \<subseteq> topspace X")
+  case True
+  then have "\<forall>x. x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<in>S. y \<in> T)) \<longrightarrow> x \<in> S
+             \<Longrightarrow> openin X (topspace X - S)"
+    apply (subst openin_subopen, safe)
+    by (metis DiffI subset_eq openin_subset [of X])
+  then show ?thesis
+    by (auto simp: closedin_def closure_of_def)
+next
+  case False
+  then show ?thesis
+    by (simp add: closedin_def)
+qed
+
+lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
+proof (cases "S \<subseteq> topspace X")
+  case True
+  then show ?thesis
+    by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
+next
+  case False
+  then show ?thesis
+    using closure_of closure_of_subset_eq by fastforce
+qed
+
+lemma closedin_contains_derived_set:
+   "closedin X S \<longleftrightarrow> X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X"
+proof (intro iffI conjI)
+  show "closedin X S \<Longrightarrow> X derived_set_of S \<subseteq> S"
+    using closure_of_eq derived_set_of_subset_closure_of by fastforce
+  show "closedin X S \<Longrightarrow> S \<subseteq> topspace X"
+    using closedin_subset by blast
+  show "X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X \<Longrightarrow> closedin X S"
+    by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
+qed
+
+lemma derived_set_subset_gen:
+   "X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X (topspace X \<inter> S)"
+  by (simp add: closedin_contains_derived_set derived_set_of_restrict derived_set_of_subset_topspace)
+
+lemma derived_set_subset: "S \<subseteq> topspace X \<Longrightarrow> (X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X S)"
+  by (simp add: closedin_contains_derived_set)
+
+lemma closedin_derived_set:
+     "closedin (subtopology X T) S \<longleftrightarrow>
+      S \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> S)"
+  by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)
+
+lemma closedin_Int_closure_of:
+     "closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
+  by (metis Int_left_absorb closure_of_eq closure_of_subtopology)
+
+lemma closure_of_closedin: "closedin X S \<Longrightarrow> X closure_of S = S"
+  by (simp add: closure_of_eq)
+
+lemma closure_of_eq_diff: "X closure_of S = topspace X - \<Union>{T. openin X T \<and> disjnt S T}"
+  by (auto simp: closure_of_def disjnt_iff)
+
+lemma closedin_closure_of [simp]: "closedin X (X closure_of S)"
+  unfolding closure_of_eq_diff by blast
+
+lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S"
+  by (simp add: closure_of_eq)
+
+lemma closure_of_hull:
+  assumes "S \<subseteq> topspace X" shows "X closure_of S = (closedin X) hull S"
+proof (rule hull_unique [THEN sym])
+  show "S \<subseteq> X closure_of S"
+    by (simp add: closure_of_subset assms)
+next
+  show "closedin X (X closure_of S)"
+    by simp
+  show "\<And>T. \<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> X closure_of S \<subseteq> T"
+    by (metis closure_of_eq closure_of_mono)
+qed
+
+lemma closure_of_minimal:
+   "\<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T"
+  by (metis closure_of_eq closure_of_mono)
+
+lemma closure_of_minimal_eq:
+   "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T \<longleftrightarrow> S \<subseteq> T"
+  by (meson closure_of_minimal closure_of_subset subset_trans)
+
+lemma closure_of_unique:
+   "\<lbrakk>S \<subseteq> T; closedin X T;
+     \<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
+    \<Longrightarrow> X closure_of S = T"
+  by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)
+
+lemma closure_of_eq_empty_gen: "X closure_of S = {} \<longleftrightarrow> disjnt (topspace X) S"
+  unfolding disjnt_def closure_of_restrict [where S=S]
+  using closure_of by fastforce
+
+lemma closure_of_eq_empty: "S \<subseteq> topspace X \<Longrightarrow> X closure_of S = {} \<longleftrightarrow> S = {}"
+  using closure_of_subset by fastforce
+
+lemma openin_Int_closure_of_subset:
+  assumes "openin X S"
+  shows "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
+proof -
+  have "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
+    by (meson assms openin_Int_derived_set_of_eq)
+  moreover have "S \<inter> (S \<inter> T) = S \<inter> T"
+    by fastforce
+  ultimately show ?thesis
+    by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1)
+qed
+
+lemma closure_of_openin_Int_closure_of:
+  assumes "openin X S"
+  shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)"
+proof
+  show "X closure_of (S \<inter> X closure_of T) \<subseteq> X closure_of (S \<inter> T)"
+    by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
+next
+  show "X closure_of (S \<inter> T) \<subseteq> X closure_of (S \<inter> X closure_of T)"
+    by (metis Int_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
+qed
+
+lemma openin_Int_closure_of_eq:
+  "openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
+  apply (rule equalityI)
+   apply (simp add: openin_Int_closure_of_subset)
+  by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)
+
+lemma openin_Int_closure_of_eq_empty:
+   "openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
+  apply (subst openin_Int_closure_of_eq, auto)
+  by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)
+
+lemma closure_of_openin_Int_superset:
+   "openin X S \<and> S \<subseteq> X closure_of T
+        \<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
+  by (metis closure_of_openin_Int_closure_of inf.orderE)
+
+lemma closure_of_openin_subtopology_Int_closure_of:
+  assumes S: "openin (subtopology X U) S" and "T \<subseteq> U"
+  shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
+proof
+  obtain S0 where S0: "openin X S0" "S = S0 \<inter> U"
+    using assms by (auto simp: openin_subtopology)
+  show "?lhs \<subseteq> ?rhs"
+  proof -
+    have "S0 \<inter> X closure_of T = S0 \<inter> X closure_of (S0 \<inter> T)"
+      by (meson S0(1) openin_Int_closure_of_eq)
+    moreover have "S0 \<inter> T = S0 \<inter> U \<inter> T"
+      using \<open>T \<subseteq> U\<close> by fastforce
+    ultimately have "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
+      using S0(2) by auto
+    then show ?thesis
+      by (meson closedin_closure_of closure_of_minimal)
+  qed
+next
+  show "?rhs \<subseteq> ?lhs"
+  proof -
+    have "T \<inter> S \<subseteq> T \<union> X derived_set_of T"
+      by force
+    then show ?thesis
+      by (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
+  qed
+qed
+
+lemma closure_of_subtopology_open:
+     "openin X U \<or> S \<subseteq> U \<Longrightarrow> (subtopology X U) closure_of S = U \<inter> X closure_of S"
+  by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq)
+
+lemma discrete_topology_closure_of:
+     "(discrete_topology U) closure_of S = U \<inter> S"
+  by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)
+
+
+text\<open> Interior with respect to a topological space.                             \<close>
+
+definition interior_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "interior'_of" 80)
+  where "X interior_of S \<equiv> {x. \<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> S}"
+
+lemma interior_of_restrict:
+   "X interior_of S = X interior_of (topspace X \<inter> S)"
+  using openin_subset by (auto simp: interior_of_def)
+
+lemma interior_of_eq: "(X interior_of S = S) \<longleftrightarrow> openin X S"
+  unfolding interior_of_def  using openin_subopen by blast
+
+lemma interior_of_openin: "openin X S \<Longrightarrow> X interior_of S = S"
+  by (simp add: interior_of_eq)
+
+lemma interior_of_empty [simp]: "X interior_of {} = {}"
+  by (simp add: interior_of_eq)
+
+lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X"
+  by (simp add: interior_of_eq)
+
+lemma openin_interior_of [simp]: "openin X (X interior_of S)"
+  unfolding interior_of_def
+  using openin_subopen by fastforce
+
+lemma interior_of_interior_of [simp]:
+   "X interior_of X interior_of S = X interior_of S"
+  by (simp add: interior_of_eq)
+
+lemma interior_of_subset: "X interior_of S \<subseteq> S"
+  by (auto simp: interior_of_def)
+
+lemma interior_of_subset_closure_of: "X interior_of S \<subseteq> X closure_of S"
+  by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset)
+
+lemma subset_interior_of_eq: "S \<subseteq> X interior_of S \<longleftrightarrow> openin X S"
+  by (metis interior_of_eq interior_of_subset subset_antisym)
+
+lemma interior_of_mono: "S \<subseteq> T \<Longrightarrow> X interior_of S \<subseteq> X interior_of T"
+  by (auto simp: interior_of_def)
+
+lemma interior_of_maximal: "\<lbrakk>T \<subseteq> S; openin X T\<rbrakk> \<Longrightarrow> T \<subseteq> X interior_of S"
+  by (auto simp: interior_of_def)
+
+lemma interior_of_maximal_eq: "openin X T \<Longrightarrow> T \<subseteq> X interior_of S \<longleftrightarrow> T \<subseteq> S"
+  by (meson interior_of_maximal interior_of_subset order_trans)
+
+lemma interior_of_unique:
+   "\<lbrakk>T \<subseteq> S; openin X T; \<And>T'. \<lbrakk>T' \<subseteq> S; openin X T'\<rbrakk> \<Longrightarrow> T' \<subseteq> T\<rbrakk> \<Longrightarrow> X interior_of S = T"
+  by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym)
+
+lemma interior_of_subset_topspace: "X interior_of S \<subseteq> topspace X"
+  by (simp add: openin_subset)
+
+lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
+  by (meson openin_imp_subset openin_interior_of)
+
+lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
+  apply (rule equalityI)
+   apply (simp add: interior_of_mono)
+  apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
+  done
+
+lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
+  by (simp add: INT_greatest Inf_lower interior_of_mono)
+
+lemma union_interior_of_subset:
+   "X interior_of S \<union> X interior_of T \<subseteq> X interior_of (S \<union> T)"
+  by (simp add: interior_of_mono)
+
+lemma interior_of_eq_empty:
+   "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<subseteq> S \<longrightarrow> T = {})"
+  by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of)
+
+lemma interior_of_eq_empty_alt:
+   "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> T - S \<noteq> {})"
+  by (auto simp: interior_of_eq_empty)
+
+lemma interior_of_Union_openin_subsets:
+   "\<Union>{T. openin X T \<and> T \<subseteq> S} = X interior_of S"
+  by (rule interior_of_unique [symmetric]) auto
+
+lemma interior_of_complement:
+   "X interior_of (topspace X - S) = topspace X - X closure_of S"
+  by (auto simp: interior_of_def closure_of_def)
+
+lemma interior_of_closure_of:
+   "X interior_of S = topspace X - X closure_of (topspace X - S)"
+  unfolding interior_of_complement [symmetric]
+  by (metis Diff_Diff_Int interior_of_restrict)
+
+lemma closure_of_interior_of:
+   "X closure_of S = topspace X - X interior_of (topspace X - S)"
+  by (simp add: interior_of_complement Diff_Diff_Int closure_of)
+
+lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S"
+  unfolding interior_of_def closure_of_def
+  by (blast dest: openin_subset)
+
+lemma interior_of_eq_empty_complement:
+  "X interior_of S = {} \<longleftrightarrow> X closure_of (topspace X - S) = topspace X"
+  using interior_of_subset_topspace [of X S] closure_of_complement by fastforce
+
+lemma closure_of_eq_topspace:
+   "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
+  using closure_of_subset_topspace [of X S] interior_of_complement by fastforce
+
+lemma interior_of_subtopology_subset:
+     "U \<inter> X interior_of S \<subseteq> (subtopology X U) interior_of S"
+  by (auto simp: interior_of_def openin_subtopology)
+
+lemma interior_of_subtopology_subsets:
+   "T \<subseteq> U \<Longrightarrow> T \<inter> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
+  by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)
+
+lemma interior_of_subtopology_mono:
+   "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
+  by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets)
+
+lemma interior_of_subtopology_open:
+  assumes "openin X U"
+  shows "(subtopology X U) interior_of S = U \<inter> X interior_of S"
+proof -
+  have "\<forall>A. U \<inter> X closure_of (U \<inter> A) = U \<inter> X closure_of A"
+    using assms openin_Int_closure_of_eq by blast
+  then have "topspace X \<inter> U - U \<inter> X closure_of (topspace X \<inter> U - S) = U \<inter> (topspace X - X closure_of (topspace X - S))"
+    by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
+  then show ?thesis
+    unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
+    using openin_Int_closure_of_eq [OF assms]
+    by (metis assms closure_of_subtopology_open)
+qed
+
+lemma dense_intersects_open:
+   "X closure_of S = topspace X \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
+proof -
+  have "X closure_of S = topspace X \<longleftrightarrow> (topspace X - X interior_of (topspace X - S) = topspace X)"
+    by (simp add: closure_of_interior_of)
+  also have "\<dots> \<longleftrightarrow> X interior_of (topspace X - S) = {}"
+    by (simp add: closure_of_complement interior_of_eq_empty_complement)
+  also have "\<dots> \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
+    unfolding interior_of_eq_empty_alt
+    using openin_subset by fastforce
+  finally show ?thesis .
+qed
+
+lemma interior_of_closedin_union_empty_interior_of:
+  assumes "closedin X S" and disj: "X interior_of T = {}"
+  shows "X interior_of (S \<union> T) = X interior_of S"
+proof -
+  have "X closure_of (topspace X - T) = topspace X"
+    by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of)
+  then show ?thesis
+    unfolding interior_of_closure_of
+    by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset)
+qed
+
+lemma interior_of_union_eq_empty:
+   "closedin X S
+        \<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
+             X interior_of S = {} \<and> X interior_of T = {})"
+  by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)
+
+lemma discrete_topology_interior_of [simp]:
+    "(discrete_topology U) interior_of S = U \<inter> S"
+  by (simp add: interior_of_restrict [of _ S] interior_of_eq)
+
+
+subsection \<open>Frontier with respect to topological space \<close>
+
+definition frontier_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "frontier'_of" 80)
+  where "X frontier_of S \<equiv> X closure_of S - X interior_of S"
+
+lemma frontier_of_closures:
+     "X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
+  by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)
+
+
+lemma interior_of_union_frontier_of [simp]:
+     "X interior_of S \<union> X frontier_of S = X closure_of S"
+  by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)
+
+lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X \<inter> S)"
+  by (metis closure_of_restrict frontier_of_def interior_of_restrict)
+
+lemma closedin_frontier_of: "closedin X (X frontier_of S)"
+  by (simp add: closedin_Int frontier_of_closures)
+
+lemma frontier_of_subset_topspace: "X frontier_of S \<subseteq> topspace X"
+  by (simp add: closedin_frontier_of closedin_subset)
+
+lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T \<subseteq> S"
+  by (metis (no_types) closedin_derived_set closedin_frontier_of)
+
+lemma frontier_of_subtopology_subset:
+  "U \<inter> (subtopology X U) frontier_of S \<subseteq> (X frontier_of S)"
+proof -
+  have "U \<inter> X interior_of S - subtopology X U interior_of S = {}"
+    by (simp add: interior_of_subtopology_subset)
+  moreover have "X closure_of S \<inter> subtopology X U closure_of S = subtopology X U closure_of S"
+    by (meson closure_of_subtopology_subset inf.absorb_iff2)
+  ultimately show ?thesis
+    unfolding frontier_of_def
+    by blast
+qed
+
+lemma frontier_of_subtopology_mono:
+   "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X T) frontier_of S \<subseteq> (subtopology X U) frontier_of S"
+    by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono)
+
+lemma clopenin_eq_frontier_of:
+   "closedin X S \<and> openin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> X frontier_of S = {}"
+proof (cases "S \<subseteq> topspace X")
+  case True
+  then show ?thesis
+    by (metis Diff_eq_empty_iff closure_of_eq closure_of_subset_eq frontier_of_def interior_of_eq interior_of_subset interior_of_union_frontier_of sup_bot_right)
+next
+  case False
+  then show ?thesis
+    by (simp add: frontier_of_closures openin_closedin_eq)
+qed
+
+lemma frontier_of_eq_empty:
+     "S \<subseteq> topspace X \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> closedin X S \<and> openin X S)"
+  by (simp add: clopenin_eq_frontier_of)
+
+lemma frontier_of_openin:
+     "openin X S \<Longrightarrow> X frontier_of S = X closure_of S - S"
+  by (metis (no_types) frontier_of_def interior_of_eq)
+
+lemma frontier_of_openin_straddle_Int:
+  assumes "openin X U" "U \<inter> X frontier_of S \<noteq> {}"
+  shows "U \<inter> S \<noteq> {}" "U - S \<noteq> {}"
+proof -
+  have "U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}"
+    using assms by (simp add: frontier_of_closures)
+  then show "U \<inter> S \<noteq> {}"
+    using assms openin_Int_closure_of_eq_empty by fastforce
+  show "U - S \<noteq> {}"
+  proof -
+    have "\<exists>A. X closure_of (A - S) \<inter> U \<noteq> {}"
+      using \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> by blast
+    then have "\<not> U \<subseteq> S"
+      by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty)
+    then show ?thesis
+      by blast
+  qed
+qed
+
+lemma frontier_of_subset_closedin: "closedin X S \<Longrightarrow> (X frontier_of S) \<subseteq> S"
+  using closure_of_eq frontier_of_def by fastforce
+
+lemma frontier_of_empty [simp]: "X frontier_of {} = {}"
+  by (simp add: frontier_of_def)
+
+lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"
+  by (simp add: frontier_of_def)
+
+lemma frontier_of_subset_eq:
+  assumes "S \<subseteq> topspace X"
+  shows "(X frontier_of S) \<subseteq> S \<longleftrightarrow> closedin X S"
+proof
+  show "X frontier_of S \<subseteq> S \<Longrightarrow> closedin X S"
+    by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff)
+  show "closedin X S \<Longrightarrow> X frontier_of S \<subseteq> S"
+    by (simp add: frontier_of_subset_closedin)
+qed
+
+lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S"
+  by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute)
+
+lemma frontier_of_disjoint_eq:
+  assumes "S \<subseteq> topspace X"
+  shows "((X frontier_of S) \<inter> S = {} \<longleftrightarrow> openin X S)"
+proof
+  assume "X frontier_of S \<inter> S = {}"
+  then have "closedin X (topspace X - S)"
+    using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce
+  then show "openin X S"
+    using assms by (simp add: openin_closedin)
+next
+  show "openin X S \<Longrightarrow> X frontier_of S \<inter> S = {}"
+    by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute)
+qed
+
+lemma frontier_of_disjoint_eq_alt:
+  "S \<subseteq> (topspace X - X frontier_of S) \<longleftrightarrow> openin X S"
+proof (cases "S \<subseteq> topspace X")
+  case True
+  show ?thesis
+    using True frontier_of_disjoint_eq by auto
+next
+  case False
+  then show ?thesis
+    by (meson Diff_subset openin_subset subset_trans)
+qed
+
+lemma frontier_of_Int:
+     "X frontier_of (S \<inter> T) =
+      X closure_of (S \<inter> T) \<inter> (X frontier_of S \<union> X frontier_of T)"
+proof -
+  have *: "U \<subseteq> S \<and> U \<subseteq> T \<Longrightarrow> U \<inter> (S \<inter> A \<union> T \<inter> B) = U \<inter> (A \<union> B)" for U S T A B :: "'a set"
+    by blast
+  show ?thesis
+    by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un)
+qed
+
+lemma frontier_of_Int_subset: "X frontier_of (S \<inter> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
+  by (simp add: frontier_of_Int)
+
+lemma frontier_of_Int_closedin:
+  "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> X frontier_of(S \<inter> T) = X frontier_of S \<inter> T \<union> S \<inter> X frontier_of T"
+  apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
+  using frontier_of_subset_closedin by blast
+
+lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
+  by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)
+
+lemma frontier_of_Union_subset:
+   "finite \<F> \<Longrightarrow> X frontier_of (\<Union>\<F>) \<subseteq> (\<Union>T \<in> \<F>. X frontier_of T)"
+proof (induction \<F> rule: finite_induct)
+  case (insert A \<F>)
+  then show ?case
+    using frontier_of_Un_subset by fastforce
+qed simp
+
+lemma frontier_of_frontier_of_subset:
+     "X frontier_of (X frontier_of S) \<subseteq> X frontier_of S"
+  by (simp add: closedin_frontier_of frontier_of_subset_closedin)
+
+lemma frontier_of_subtopology_open:
+     "openin X U \<Longrightarrow> (subtopology X U) frontier_of S = U \<inter> X frontier_of S"
+  by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open)
+
+lemma discrete_topology_frontier_of [simp]:
+     "(discrete_topology U) frontier_of S = {}"
+  by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
+
+
+subsection\<open>Continuous maps\<close>
+
+definition continuous_map where
+  "continuous_map X Y f \<equiv>
+     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+     (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+
+lemma continuous_map:
+   "continuous_map X Y f \<longleftrightarrow>
+        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+  by (auto simp: continuous_map_def)
+
+lemma continuous_map_image_subset_topspace:
+   "continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
+  by (auto simp: continuous_map_def)
+
+lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
+  by (auto simp: continuous_map_def)
+
+lemma continuous_map_closedin:
+   "continuous_map X Y f \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
+proof -
+  have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
+        (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
+    if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+  proof -
+    have eq: "{x \<in> topspace X. f x \<in> topspace Y \<and> f x \<notin> C} = (topspace X - {x \<in> topspace X. f x \<in> C})" for C
+      using that by blast
+    show ?thesis
+    proof (intro iffI allI impI)
+      fix C
+      assume "\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}" and "closedin Y C"
+      then have "openin X {x \<in> topspace X. f x \<in> topspace Y - C}" by blast
+      then show "closedin X {x \<in> topspace X. f x \<in> C}"
+        by (auto simp add: closedin_def eq)
+    next
+      fix U
+      assume "\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}" and "openin Y U"
+      then have "closedin X {x \<in> topspace X. f x \<in> topspace Y - U}" by blast
+      then show "openin X {x \<in> topspace X. f x \<in> U}"
+        by (auto simp add: openin_closedin_eq eq)
+    qed
+  qed
+  then show ?thesis
+    by (auto simp: continuous_map_def)
+qed
+
+lemma openin_continuous_map_preimage:
+   "\<lbrakk>continuous_map X Y f; openin Y U\<rbrakk> \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+  by (simp add: continuous_map_def)
+
+lemma closedin_continuous_map_preimage:
+   "\<lbrakk>continuous_map X Y f; closedin Y C\<rbrakk> \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}"
+  by (simp add: continuous_map_closedin)
+
+lemma openin_continuous_map_preimage_gen:
+  assumes "continuous_map X Y f" "openin X U" "openin Y V"
+  shows "openin X {x \<in> U. f x \<in> V}"
+proof -
+  have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
+    using assms(2) openin_closedin_eq by fastforce
+  show ?thesis
+    unfolding eq
+    using assms openin_continuous_map_preimage by fastforce
+qed
+
+lemma closedin_continuous_map_preimage_gen:
+  assumes "continuous_map X Y f" "closedin X U" "closedin Y V"
+  shows "closedin X {x \<in> U. f x \<in> V}"
+proof -
+  have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
+    using assms(2) closedin_def by fastforce
+  show ?thesis
+    unfolding eq
+    using assms closedin_continuous_map_preimage by fastforce
+qed
+
+lemma continuous_map_image_closure_subset:
+  assumes "continuous_map X Y f"
+  shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
+proof -
+  have *: "f ` (topspace X) \<subseteq> topspace Y"
+    by (meson assms continuous_map)
+  have "X closure_of T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of (f ` T)}" if "T \<subseteq> topspace X" for T
+  proof (rule closure_of_minimal)
+    show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
+      using closure_of_subset * that  by (fastforce simp: in_closure_of)
+  next
+    show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
+      using assms closedin_continuous_map_preimage_gen by fastforce
+  qed
+  then have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (f ` (topspace X \<inter> S))"
+    by blast
+  also have "\<dots> \<subseteq> Y closure_of (topspace Y \<inter> f ` S)"
+    using * by (blast intro!: closure_of_mono)
+  finally have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (topspace Y \<inter> f ` S)" .
+  then show ?thesis
+    by (metis closure_of_restrict)
+qed
+
+lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
+       (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+  using continuous_map_image_closure_subset by blast
+
+lemma continuous_map_subset_aux2:
+  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
+  shows "continuous_map X Y f"
+  unfolding continuous_map_closedin
+proof (intro conjI ballI allI impI)
+  fix x
+  assume "x \<in> topspace X"
+  then show "f x \<in> topspace Y"
+    using assms closure_of_subset_topspace by fastforce
+next
+  fix C
+  assume "closedin Y C"
+  then show "closedin X {x \<in> topspace X. f x \<in> C}"
+  proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
+    fix x
+    assume x: "x \<in> X closure_of {x \<in> topspace X. f x \<in> C}"
+      and "C \<subseteq> topspace Y" and "Y closure_of C \<subseteq> C"
+    show "x \<in> topspace X"
+      by (meson x in_closure_of)
+    have "{a \<in> topspace X. f a \<in> C} \<subseteq> topspace X"
+      by simp
+    moreover have "Y closure_of f ` {a \<in> topspace X. f a \<in> C} \<subseteq> C"
+      by (simp add: \<open>closedin Y C\<close> closure_of_minimal image_subset_iff)
+    ultimately have "f ` (X closure_of {a \<in> topspace X. f a \<in> C}) \<subseteq> C"
+      using assms by blast
+    then show "f x \<in> C"
+      using x by auto
+  qed
+qed
+
+lemma continuous_map_eq_image_closure_subset:
+     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+  using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
+
+lemma continuous_map_eq_image_closure_subset_alt:
+     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+  using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
+
+lemma continuous_map_eq_image_closure_subset_gen:
+     "continuous_map X Y f \<longleftrightarrow>
+        f ` (topspace X) \<subseteq> topspace Y \<and>
+        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+  using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
+
+lemma continuous_map_closure_preimage_subset:
+   "continuous_map X Y f
+        \<Longrightarrow> X closure_of {x \<in> topspace X. f x \<in> T}
+            \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
+  unfolding continuous_map_closedin
+  by (rule closure_of_minimal) (use in_closure_of in \<open>fastforce+\<close>)
+
+
+lemma continuous_map_frontier_frontier_preimage_subset:
+  assumes "continuous_map X Y f"
+  shows "X frontier_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y frontier_of T}"
+proof -
+  have eq: "topspace X - {x \<in> topspace X. f x \<in> T} = {x \<in> topspace X. f x \<in> topspace Y - T}"
+    using assms unfolding continuous_map_def by blast
+  have "X closure_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
+    by (simp add: assms continuous_map_closure_preimage_subset)
+  moreover
+  have "X closure_of (topspace X - {x \<in> topspace X. f x \<in> T}) \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of (topspace Y - T)}"
+    using continuous_map_closure_preimage_subset [OF assms] eq by presburger
+  ultimately show ?thesis
+    by (auto simp: frontier_of_closures)
+qed
+
+lemma continuous_map_id [simp]: "continuous_map X X id"
+  unfolding continuous_map_def  using openin_subopen topspace_def by fastforce
+
+lemma topology_finer_continuous_id:
+  "topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
+  unfolding continuous_map_def
+  apply auto
+  using openin_subopen openin_subset apply fastforce
+  using openin_subopen topspace_def by fastforce
+
+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
+  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)
+
+lemma continuous_map_compose:
+  assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
+  shows "continuous_map X X'' (g \<circ> f)"
+  unfolding continuous_map_def
+proof (intro conjI ballI allI impI)
+  fix x
+  assume "x \<in> topspace X"
+  then show "(g \<circ> f) x \<in> topspace X''"
+    using assms unfolding continuous_map_def by force
+next
+  fix U
+  assume "openin X'' U"
+  have eq: "{x \<in> topspace X. (g \<circ> f) x \<in> U} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U}}"
+    by auto (meson f continuous_map_def)
+  show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
+    unfolding eq
+    using assms unfolding continuous_map_def
+    using \<open>openin X'' U\<close> by blast
+qed
+
+lemma continuous_map_eq:
+  assumes "continuous_map X X' f" and "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x" shows "continuous_map X X' g"
+proof -
+  have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
+    using assms by auto
+  show ?thesis
+    using assms by (simp add: continuous_map_def eq)
+qed
+
+lemma restrict_continuous_map [simp]:
+     "topspace X \<subseteq> S \<Longrightarrow> continuous_map X X' (restrict f S) \<longleftrightarrow> continuous_map X X' f"
+  by (auto simp: elim!: continuous_map_eq)
+
+lemma continuous_map_in_subtopology:
+  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
+  (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  show ?rhs
+  proof -
+    have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
+      by (meson L continuous_map_image_closure_subset)
+    then show ?thesis
+      by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset dual_order.trans)
+  qed
+next
+  assume R: ?rhs
+  then have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. f x \<in> U \<and> f x \<in> S}" for U
+    by auto
+  show ?lhs
+    using R
+    unfolding continuous_map
+    by (auto simp: topspace_subtopology openin_subtopology eq)
+qed
+
+
+lemma continuous_map_from_subtopology:
+     "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
+  by (auto simp: continuous_map topspace_subtopology openin_subtopology)
+
+lemma continuous_map_into_fulltopology:
+   "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
+  by (auto simp: continuous_map_in_subtopology)
+
+lemma continuous_map_into_subtopology:
+   "\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
+  by (auto simp: continuous_map_in_subtopology)
+
+lemma continuous_map_from_subtopology_mono:
+     "\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
+      \<Longrightarrow> continuous_map (subtopology X S) X' f"
+  by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)
+
+lemma continuous_map_from_discrete_topology [simp]:
+  "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
+  by (auto simp: continuous_map_def)
+
+lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g"
+  by (force simp: continuous_map openin_subtopology continuous_on_open_invariant)
+
+
+subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
+
+definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where "open_map X1 X2 f \<equiv> \<forall>U. openin X1 U \<longrightarrow> openin X2 (f ` U)"
+
+definition closed_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"
+
+lemma open_map_imp_subset_topspace:
+     "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
+  unfolding open_map_def by (simp add: openin_subset)
+
+lemma open_map_imp_subset:
+    "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
+  by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
+
+lemma topology_finer_open_id:
+     "(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
+  unfolding open_map_def by auto
+
+lemma open_map_id: "open_map X X id"
+  unfolding open_map_def by auto
+
+lemma open_map_eq:
+     "\<lbrakk>open_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> open_map X X' g"
+  unfolding open_map_def
+  by (metis image_cong openin_subset subset_iff)
+
+lemma open_map_inclusion_eq:
+  "open_map (subtopology X S) X id \<longleftrightarrow> openin X (topspace X \<inter> S)"
+proof -
+  have *: "openin X (T \<inter> S)" if "openin X (S \<inter> topspace X)" "openin X T" for T
+  proof -
+    have "T \<subseteq> topspace X"
+      using that by (simp add: openin_subset)
+    with that show "openin X (T \<inter> S)"
+      by (metis inf.absorb1 inf.left_commute inf_commute openin_Int)
+  qed
+  show ?thesis
+    by (fastforce simp add: open_map_def Int_commute openin_subtopology_alt intro: *)
+qed
+
+lemma open_map_inclusion:
+     "openin X S \<Longrightarrow> open_map (subtopology X S) X id"
+  by (simp add: open_map_inclusion_eq openin_Int)
+
+lemma open_map_compose:
+     "\<lbrakk>open_map X X' f; open_map X' X'' g\<rbrakk> \<Longrightarrow> open_map X X'' (g \<circ> f)"
+  by (metis (no_types, lifting) image_comp open_map_def)
+
+lemma closed_map_imp_subset_topspace:
+     "closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
+  by (simp add: closed_map_def closedin_subset)
+
+lemma closed_map_imp_subset:
+     "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
+  using closed_map_imp_subset_topspace by blast
+
+lemma topology_finer_closed_id:
+    "(\<forall>S. closedin X S \<longrightarrow> closedin X' S) \<longleftrightarrow> closed_map X X' id"
+  by (simp add: closed_map_def)
+
+lemma closed_map_id: "closed_map X X id"
+  by (simp add: closed_map_def)
+
+lemma closed_map_eq:
+   "\<lbrakk>closed_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> closed_map X X' g"
+  unfolding closed_map_def
+  by (metis image_cong closedin_subset subset_iff)
+
+lemma closed_map_compose:
+    "\<lbrakk>closed_map X X' f; closed_map X' X'' g\<rbrakk> \<Longrightarrow> closed_map X X'' (g \<circ> f)"
+  by (metis (no_types, lifting) closed_map_def image_comp)
+
+lemma closed_map_inclusion_eq:
+   "closed_map (subtopology X S) X id \<longleftrightarrow>
+        closedin X (topspace X \<inter> S)"
+proof -
+  have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
+  proof -
+    have "T \<subseteq> topspace X"
+      using that by (simp add: closedin_subset)
+    with that show "closedin X (T \<inter> S)"
+      by (metis inf.absorb1 inf.left_commute inf_commute closedin_Int)
+  qed
+  show ?thesis
+    by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *)
+qed
+
+lemma closed_map_inclusion: "closedin X S \<Longrightarrow> closed_map (subtopology X S) X id"
+  by (simp add: closed_map_inclusion_eq closedin_Int)
+
+lemma open_map_into_subtopology:
+    "\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
+  unfolding open_map_def openin_subtopology
+  using openin_subset by fastforce
+
+lemma closed_map_into_subtopology:
+    "\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
+  unfolding closed_map_def closedin_subtopology
+  using closedin_subset by fastforce
+
+lemma open_map_into_discrete_topology:
+    "open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
+  unfolding open_map_def openin_discrete_topology using openin_subset by blast
+
+lemma closed_map_into_discrete_topology:
+    "closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
+  unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast
+
+lemma bijective_open_imp_closed_map:
+     "\<lbrakk>open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> closed_map X X' f"
+  unfolding open_map_def closed_map_def closedin_def
+  by auto (metis Diff_subset inj_on_image_set_diff)
+
+lemma bijective_closed_imp_open_map:
+     "\<lbrakk>closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> open_map X X' f"
+  unfolding closed_map_def open_map_def openin_closedin_eq
+  by auto (metis Diff_subset inj_on_image_set_diff)
+
+lemma open_map_from_subtopology:
+     "\<lbrakk>open_map X X' f; openin X U\<rbrakk> \<Longrightarrow> open_map (subtopology X U) X' f"
+  unfolding open_map_def openin_subtopology_alt by blast
+
+lemma closed_map_from_subtopology:
+     "\<lbrakk>closed_map X X' f; closedin X U\<rbrakk> \<Longrightarrow> closed_map (subtopology X U) X' f"
+  unfolding closed_map_def closedin_subtopology_alt by blast
+
+lemma open_map_restriction:
+     "\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
+      \<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
+  unfolding open_map_def openin_subtopology_alt
+  apply clarify
+  apply (rename_tac T)
+  apply (rule_tac x="f ` T" in image_eqI)
+  using openin_closedin_eq by force+
+
+lemma closed_map_restriction:
+     "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
+      \<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
+  unfolding closed_map_def closedin_subtopology_alt
+  apply clarify
+  apply (rename_tac T)
+  apply (rule_tac x="f ` T" in image_eqI)
+  using closedin_def by force+
+
+subsection\<open>Quotient maps\<close>
+                                      
+definition quotient_map where
+ "quotient_map X X' f \<longleftrightarrow>
+        f ` (topspace X) = topspace X' \<and>
+        (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (openin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> openin X' U))"
+
+lemma quotient_map_eq:
+  assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
+  shows "quotient_map X X' g"
+proof -
+  have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
+    using assms by auto
+  show ?thesis
+  using assms
+  unfolding quotient_map_def
+  by (metis (mono_tags, lifting) eq image_cong)
+qed
+
+lemma quotient_map_compose:
+  assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
+  shows "quotient_map X X'' (g \<circ> f)"
+  unfolding quotient_map_def
+proof (intro conjI allI impI)
+  show "(g \<circ> f) ` topspace X = topspace X''"
+    using assms image_comp unfolding quotient_map_def by force
+next
+  fix U''
+  assume "U'' \<subseteq> topspace X''"
+  define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}"
+  have "U' \<subseteq> topspace X'"
+    by (auto simp add: U'_def)
+  then have U': "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
+    using assms unfolding quotient_map_def by simp
+  have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''} = {x \<in> topspace X. (g \<circ> f) x \<in> U''}"
+    using f quotient_map_def by fastforce
+  have "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X {x \<in> topspace X. f x \<in> U'}"
+    using assms  by (simp add: quotient_map_def U'_def eq)
+  also have "\<dots> = openin X'' U''"
+    using U'_def \<open>U'' \<subseteq> topspace X''\<close> U' g quotient_map_def by fastforce
+  finally show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X'' U''" .
+qed
+
+lemma quotient_map_from_composition:
+  assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \<circ> f)"
+  shows  "quotient_map X' X'' g"
+  unfolding quotient_map_def
+proof (intro conjI allI impI)
+  show "g ` topspace X' = topspace X''"
+    using assms unfolding continuous_map_def quotient_map_def by fastforce
+next
+  fix U'' :: "'c set"
+  assume U'': "U'' \<subseteq> topspace X''"
+  have eq: "{x \<in> topspace X. g (f x) \<in> U''} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U''}}"
+    using continuous_map_def f by fastforce
+  show "openin X' {x \<in> topspace X'. g x \<in> U''} = openin X'' U''"
+    using assms unfolding continuous_map_def quotient_map_def
+    by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq)
+qed
+
+lemma quotient_imp_continuous_map:
+    "quotient_map X X' f \<Longrightarrow> continuous_map X X' f"
+  by (simp add: continuous_map openin_subset quotient_map_def)
+
+lemma quotient_imp_surjective_map:
+    "quotient_map X X' f \<Longrightarrow> f ` (topspace X) = topspace X'"
+  by (simp add: quotient_map_def)
+
+lemma quotient_map_closedin:
+  "quotient_map X X' f \<longleftrightarrow>
+        f ` (topspace X) = topspace X' \<and>
+        (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (closedin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> closedin X' U))"
+proof -
+  have eq: "(topspace X - {x \<in> topspace X. f x \<in> U'}) = {x \<in> topspace X. f x \<in> topspace X' \<and> f x \<notin> U'}"
+    if "f ` topspace X = topspace X'" "U' \<subseteq> topspace X'" for U'
+      using that by auto
+  have "(\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U) =
+          (\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U)"
+    if "f ` topspace X = topspace X'"
+  proof (rule iffI; intro allI impI subsetI)
+    fix U'
+    assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
+      and U': "U' \<subseteq> topspace X'"
+    show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
+      using U'  by (auto simp add: closedin_def Diff_subset simp flip: * [of "topspace X' - U'"] eq [OF that])
+  next
+    fix U' :: "'b set"
+    assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
+      and U': "U' \<subseteq> topspace X'"
+    show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
+      using U'  by (auto simp add: openin_closedin_eq Diff_subset simp flip: * [of "topspace X' - U'"] eq [OF that])
+  qed
+  then show ?thesis
+    unfolding quotient_map_def by force
+qed
+
+lemma continuous_open_imp_quotient_map:
+  assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
+  shows "quotient_map X X' f"
+proof -
+  { fix U
+    assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
+    then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
+      using om unfolding open_map_def by blast
+    then have "openin X' U"
+      using U feq by (subst openin_subopen) force
+  }
+  moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
+    using that assms unfolding continuous_map_def by blast
+  ultimately show ?thesis
+    unfolding quotient_map_def using assms by blast
+qed
+
+lemma continuous_closed_imp_quotient_map:
+  assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'"
+  shows "quotient_map X X' f"
+proof -
+  have "f ` {x \<in> topspace X. f x \<in> U} = U" if "U \<subseteq> topspace X'" for U
+    using that feq by auto
+  with assms show ?thesis
+    unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto
+qed
+
+lemma continuous_open_quotient_map:
+   "\<lbrakk>continuous_map X X' f; open_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
+  by (meson continuous_open_imp_quotient_map quotient_map_def)
+
+lemma continuous_closed_quotient_map:
+     "\<lbrakk>continuous_map X X' f; closed_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
+  by (meson continuous_closed_imp_quotient_map quotient_map_def)
+
+lemma injective_quotient_map:
+  assumes "inj_on f (topspace X)"
+  shows "quotient_map X X' f \<longleftrightarrow>
+         continuous_map X X' f \<and> open_map X X' f \<and> closed_map X X' f \<and> f ` (topspace X) = topspace X'"
+         (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  have "open_map X X' f"
+  proof (clarsimp simp add: open_map_def)
+    fix U
+    assume "openin X U"
+    then have "U \<subseteq> topspace X"
+      by (simp add: openin_subset)
+    moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
+      using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
+    ultimately show "openin X' (f ` U)"
+      using L unfolding quotient_map_def
+      by (metis (no_types, lifting) Collect_cong \<open>openin X U\<close> image_mono)
+  qed
+  moreover have "closed_map X X' f"
+  proof (clarsimp simp add: closed_map_def)
+    fix U
+    assume "closedin X U"
+    then have "U \<subseteq> topspace X"
+      by (simp add: closedin_subset)
+    moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
+      using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
+    ultimately show "closedin X' (f ` U)"
+      using L unfolding quotient_map_closedin
+      by (metis (no_types, lifting) Collect_cong \<open>closedin X U\<close> image_mono)
+  qed
+  ultimately show ?rhs
+    using L by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
+next
+  assume ?rhs
+  then show ?lhs
+    by (simp add: continuous_closed_imp_quotient_map)
+qed
+
+lemma continuous_compose_quotient_map:
+  assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
+  shows "continuous_map X' X'' g"
+  unfolding quotient_map_def continuous_map_def
+proof (intro conjI ballI allI impI)
+  show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
+    using assms unfolding quotient_map_def
+    by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
+next
+  fix U'' :: "'c set"
+  assume U'': "openin X'' U''"
+  have "f ` topspace X = topspace X'"
+    by (simp add: f quotient_imp_surjective_map)
+  then have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U} = {x \<in> topspace X. g (f x) \<in> U}" for U
+    by auto
+  have "openin X {x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''}"
+    unfolding eq using U'' g openin_continuous_map_preimage by fastforce
+  then have *: "openin X {x \<in> topspace X. f x \<in> {x \<in> topspace X'. g x \<in> U''}}"
+    by auto
+  show "openin X' {x \<in> topspace X'. g x \<in> U''}"
+    using f unfolding quotient_map_def
+    by (metis (no_types) Collect_subset *)
+qed
+
+lemma continuous_compose_quotient_map_eq:
+   "quotient_map X X' f \<Longrightarrow> continuous_map X X'' (g \<circ> f) \<longleftrightarrow> continuous_map X' X'' g"
+  using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast
+
+lemma quotient_map_compose_eq:
+   "quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
+  apply safe
+  apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
+  by (simp add: quotient_map_compose)
+
+lemma quotient_map_restriction:
+  assumes quo: "quotient_map X Y f" and U: "{x \<in> topspace X. f x \<in> V} = U" and disj: "openin Y V \<or> closedin Y V"
+ shows "quotient_map (subtopology X U) (subtopology Y V) f"
+  using disj
+proof
+  assume V: "openin Y V"
+  with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
+    by (auto simp: openin_subset)
+  have fim: "f ` topspace X = topspace Y"
+     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
+    using quo unfolding quotient_map_def by auto
+  have "openin X U"
+    using U V Y sub(2) by blast
+  show ?thesis
+    unfolding quotient_map_def
+  proof (intro conjI allI impI)
+    show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
+      using sub U fim by (auto simp: topspace_subtopology)
+  next
+    fix Y' :: "'b set"
+    assume "Y' \<subseteq> topspace (subtopology Y V)"
+    then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
+      by (simp_all add: topspace_subtopology)
+    then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
+      using U by blast
+    then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
+      using U V Y \<open>openin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
+      by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
+  qed
+next
+  assume V: "closedin Y V"
+  with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
+    by (auto simp: closedin_subset)
+  have fim: "f ` topspace X = topspace Y"
+     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U} = closedin Y U"
+    using quo unfolding quotient_map_closedin by auto
+  have "closedin X U"
+    using U V Y sub(2) by blast
+  show ?thesis
+    unfolding quotient_map_closedin
+  proof (intro conjI allI impI)
+    show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
+      using sub U fim by (auto simp: topspace_subtopology)
+  next
+    fix Y' :: "'b set"
+    assume "Y' \<subseteq> topspace (subtopology Y V)"
+    then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
+      by (simp_all add: topspace_subtopology)
+    then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
+      using U by blast
+    then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
+      using U V Y \<open>closedin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
+      by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
+  qed
+qed
+
+lemma quotient_map_saturated_open:
+     "quotient_map X Y f \<longleftrightarrow>
+        continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
+        (\<forall>U. openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> openin Y (f ` U))"
+     (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then have fim: "f ` topspace X = topspace Y"
+    and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin Y U = openin X {x \<in> topspace X. f x \<in> U}"
+    unfolding quotient_map_def by auto
+  show ?rhs
+  proof (intro conjI allI impI)
+    show "continuous_map X Y f"
+      by (simp add: L quotient_imp_continuous_map)
+    show "f ` topspace X = topspace Y"
+      by (simp add: fim)
+  next
+    fix U :: "'a set"
+    assume U: "openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
+    then have sub:  "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
+      using fim openin_subset by fastforce+
+    show "openin Y (f ` U)"
+      by (simp add: sub Y eq U)
+  qed
+next
+  assume ?rhs
+  then have YX: "\<And>U. openin Y U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+       and fim: "f ` topspace X = topspace Y"
+       and XY: "\<And>U. \<lbrakk>openin X U; {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U\<rbrakk> \<Longrightarrow> openin Y (f ` U)"
+    by (auto simp: quotient_map_def continuous_map_def)
+  show ?lhs
+  proof (simp add: quotient_map_def fim, intro allI impI iffI)
+    fix U :: "'b set"
+    assume "U \<subseteq> topspace Y" and X: "openin X {x \<in> topspace X. f x \<in> U}"
+    have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
+      using \<open>U \<subseteq> topspace Y\<close> fim by auto
+    show "openin Y U"
+      using XY [OF X] by (simp add: feq)
+  next
+    fix U :: "'b set"
+    assume "U \<subseteq> topspace Y" and Y: "openin Y U"
+    show "openin X {x \<in> topspace X. f x \<in> U}"
+      by (metis YX [OF Y])
+  qed
+qed
+
+subsection\<open> Separated Sets\<close>
+
+definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  where "separatedin X S T \<equiv>
+           S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
+           S \<inter> X closure_of T = {} \<and> T \<inter> X closure_of S = {}"
+
+lemma separatedin_empty [simp]:
+     "separatedin X S {} \<longleftrightarrow> S \<subseteq> topspace X"
+     "separatedin X {} S \<longleftrightarrow> S \<subseteq> topspace X"
+  by (simp_all add: separatedin_def)
+
+lemma separatedin_refl [simp]:
+     "separatedin X S S \<longleftrightarrow> S = {}"
+proof -
+  have "\<And>x. \<lbrakk>separatedin X S S; x \<in> S\<rbrakk> \<Longrightarrow> False"
+    by (metis all_not_in_conv closure_of_subset inf.orderE separatedin_def)
+  then show ?thesis
+    by auto
+qed
+
+lemma separatedin_sym:
+     "separatedin X S T \<longleftrightarrow> separatedin X T S"
+  by (auto simp: separatedin_def)
+
+lemma separatedin_imp_disjoint:
+     "separatedin X S T \<Longrightarrow> disjnt S T"
+  by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def)
+
+lemma separatedin_mono:
+   "\<lbrakk>separatedin X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separatedin X S' T'"
+  unfolding separatedin_def
+  using closure_of_mono by blast
+
+lemma separatedin_open_sets:
+     "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
+  unfolding disjnt_def separatedin_def
+  by (auto simp: openin_Int_closure_of_eq_empty openin_subset)
+
+lemma separatedin_closed_sets:
+     "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
+  by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)
+
+lemma separatedin_subtopology:
+     "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
+  apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
+  apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
+  done
+
+lemma separatedin_discrete_topology:
+     "separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
+  by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology)
+
+lemma separated_eq_distinguishable:
+   "separatedin X {x} {y} \<longleftrightarrow>
+        x \<in> topspace X \<and> y \<in> topspace X \<and>
+        (\<exists>U. openin X U \<and> x \<in> U \<and> (y \<notin> U)) \<and>
+        (\<exists>v. openin X v \<and> y \<in> v \<and> (x \<notin> v))"
+  by (force simp: separatedin_def closure_of_def)
+
+lemma separatedin_Un [simp]:
+   "separatedin X S (T \<union> U) \<longleftrightarrow> separatedin X S T \<and> separatedin X S U"
+   "separatedin X (S \<union> T) U \<longleftrightarrow> separatedin X S U \<and> separatedin X T U"
+  by (auto simp: separatedin_def)
+
+lemma separatedin_Union:
+  "finite \<F> \<Longrightarrow> separatedin X S (\<Union>\<F>) \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<forall>T \<in> \<F>. separatedin X S T)"
+  "finite \<F> \<Longrightarrow> separatedin X (\<Union>\<F>) S \<longleftrightarrow> (\<forall>T \<in> \<F>. separatedin X S T) \<and> S \<subseteq> topspace X"
+  by (auto simp: separatedin_def closure_of_Union)
+
+lemma separatedin_openin_diff:
+   "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
+  unfolding separatedin_def
+  apply (intro conjI)
+  apply (meson Diff_subset openin_subset subset_trans)+
+  using openin_Int_closure_of_eq_empty by fastforce+
+
+lemma separatedin_closedin_diff:
+     "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
+  apply (simp add: separatedin_def Diff_Int_distrib2 Diff_subset closure_of_minimal inf_absorb2)
+  apply (meson Diff_subset closedin_subset subset_trans)
+  done
+
+lemma separation_closedin_Un_gen:
+     "separatedin X S T \<longleftrightarrow>
+        S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
+        closedin (subtopology X (S \<union> T)) S \<and>
+        closedin (subtopology X (S \<union> T)) T"
+  apply (simp add: separatedin_def closedin_Int_closure_of disjnt_iff)
+  using closure_of_subset apply blast
+  done
+
+lemma separation_openin_Un_gen:
+     "separatedin X S T \<longleftrightarrow>
+        S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
+        openin (subtopology X (S \<union> T)) S \<and>
+        openin (subtopology X (S \<union> T)) T"
+  unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
+  by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)
+
+
+subsection\<open>Homeomorphisms\<close>
+text\<open>(1-way and 2-way versions may be useful in places)\<close>
+
+definition homeomorphic_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where
+ "homeomorphic_map X Y f \<equiv> quotient_map X Y f \<and> inj_on f (topspace X)"
+
+definition homeomorphic_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
+  where
+ "homeomorphic_maps X Y f g \<equiv>
+    continuous_map X Y f \<and> continuous_map Y X g \<and>
+     (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
+
+
+lemma homeomorphic_map_eq:
+   "\<lbrakk>homeomorphic_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> homeomorphic_map X Y g"
+  by (meson homeomorphic_map_def inj_on_cong quotient_map_eq)
+
+lemma homeomorphic_maps_eq:
+     "\<lbrakk>homeomorphic_maps X Y f g;
+       \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
+      \<Longrightarrow> homeomorphic_maps X Y f' g'"
+  apply (simp add: homeomorphic_maps_def)
+  by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
+
+lemma homeomorphic_maps_sym:
+     "homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
+  by (auto simp: homeomorphic_maps_def)
+
+lemma homeomorphic_maps_id:
+     "homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
+  (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then have "topspace X = topspace Y"
+    by (auto simp: homeomorphic_maps_def continuous_map_def)
+  with L show ?rhs
+    unfolding homeomorphic_maps_def
+    by (metis topology_finer_continuous_id topology_eq)
+next
+  assume ?rhs
+  then show ?lhs
+    unfolding homeomorphic_maps_def by auto
+qed
+
+lemma homeomorphic_map_id [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
+       (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then have eq: "topspace X = topspace Y"
+    by (auto simp: homeomorphic_map_def continuous_map_def quotient_map_def)
+  then have "\<And>S. openin X S \<longrightarrow> openin Y S"
+    by (meson L homeomorphic_map_def injective_quotient_map topology_finer_open_id)
+  then show ?rhs
+    using L unfolding homeomorphic_map_def
+    by (metis eq quotient_imp_continuous_map topology_eq topology_finer_continuous_id)
+next
+  assume ?rhs
+  then show ?lhs
+    unfolding homeomorphic_map_def
+    by (simp add: closed_map_id continuous_closed_imp_quotient_map)
+qed
+
+lemma homeomorphic_maps_i [simp]:"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
+  by (metis (full_types) eq_id_iff homeomorphic_maps_id)
+
+lemma homeomorphic_map_i [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
+  by (metis (no_types) eq_id_iff homeomorphic_map_id)
+
+lemma homeomorphic_map_compose:
+  assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g"
+  shows "homeomorphic_map X X'' (g \<circ> f)"
+proof -
+  have "inj_on g (f ` topspace X)"
+    by (metis (no_types) assms homeomorphic_map_def quotient_imp_surjective_map)
+  then show ?thesis
+    using assms by (meson comp_inj_on homeomorphic_map_def quotient_map_compose_eq)
+qed
+
+lemma homeomorphic_maps_compose:
+   "homeomorphic_maps X Y f h \<and>
+        homeomorphic_maps Y X'' g k
+        \<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
+  unfolding homeomorphic_maps_def
+  by (auto simp: continuous_map_compose; simp add: continuous_map_def)
+
+lemma homeomorphic_eq_everything_map:
+   "homeomorphic_map X Y f \<longleftrightarrow>
+        continuous_map X Y f \<and> open_map X Y f \<and> closed_map X Y f \<and>
+        f ` (topspace X) = topspace Y \<and> inj_on f (topspace X)"
+  unfolding homeomorphic_map_def
+  by (force simp: injective_quotient_map intro: injective_quotient_map)
+
+lemma homeomorphic_imp_continuous_map:
+     "homeomorphic_map X Y f \<Longrightarrow> continuous_map X Y f"
+  by (simp add: homeomorphic_eq_everything_map)
+
+lemma homeomorphic_imp_open_map:
+   "homeomorphic_map X Y f \<Longrightarrow> open_map X Y f"
+  by (simp add: homeomorphic_eq_everything_map)
+
+lemma homeomorphic_imp_closed_map:
+   "homeomorphic_map X Y f \<Longrightarrow> closed_map X Y f"
+  by (simp add: homeomorphic_eq_everything_map)
+
+lemma homeomorphic_imp_surjective_map:
+   "homeomorphic_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
+  by (simp add: homeomorphic_eq_everything_map)
+
+lemma homeomorphic_imp_injective_map:
+    "homeomorphic_map X Y f \<Longrightarrow> inj_on f (topspace X)"
+  by (simp add: homeomorphic_eq_everything_map)
+
+lemma bijective_open_imp_homeomorphic_map:
+   "\<lbrakk>continuous_map X Y f; open_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
+        \<Longrightarrow> homeomorphic_map X Y f"
+  by (simp add: homeomorphic_map_def continuous_open_imp_quotient_map)
+
+lemma bijective_closed_imp_homeomorphic_map:
+   "\<lbrakk>continuous_map X Y f; closed_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
+        \<Longrightarrow> homeomorphic_map X Y f"
+  by (simp add: continuous_closed_quotient_map homeomorphic_map_def)
+
+lemma open_eq_continuous_inverse_map:
+  assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
+    and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
+  shows "open_map X Y f \<longleftrightarrow> continuous_map Y X g"
+proof -
+  have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "openin X U" for U
+    using openin_subset [OF that] by (force simp: X Y image_iff)
+  show ?thesis
+    by (auto simp: Y open_map_def continuous_map_def eq)
+qed
+
+lemma closed_eq_continuous_inverse_map:
+  assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
+    and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
+  shows "closed_map X Y f \<longleftrightarrow> continuous_map Y X g"
+proof -
+  have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "closedin X U" for U
+    using closedin_subset [OF that] by (force simp: X Y image_iff)
+  show ?thesis
+    by (auto simp: Y closed_map_def continuous_map_closedin eq)
+qed
+
+lemma homeomorphic_maps_map:
+  "homeomorphic_maps X Y f g \<longleftrightarrow>
+        homeomorphic_map X Y f \<and> homeomorphic_map Y X g \<and>
+        (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have L: "continuous_map X Y f" "continuous_map Y X g" "\<forall>x\<in>topspace X. g (f x) = x" "\<forall>x'\<in>topspace Y. f (g x') = x'"
+    by (auto simp: homeomorphic_maps_def)
+  show ?rhs
+  proof (intro conjI bijective_open_imp_homeomorphic_map L)
+    show "open_map X Y f"
+      using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
+    show "open_map Y X g"
+      using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
+    show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
+      using L by (force simp: continuous_map_closedin)+
+    show "inj_on f (topspace X)" "inj_on g (topspace Y)"
+      using L unfolding inj_on_def by metis+
+  qed
+next
+  assume ?rhs
+  then show ?lhs
+    by (auto simp: homeomorphic_maps_def homeomorphic_imp_continuous_map)
+qed
+
+lemma homeomorphic_maps_imp_map:
+    "homeomorphic_maps X Y f g \<Longrightarrow> homeomorphic_map X Y f"
+  using homeomorphic_maps_map by blast
+
+lemma homeomorphic_map_maps:
+     "homeomorphic_map X Y f \<longleftrightarrow> (\<exists>g. homeomorphic_maps X Y f g)"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have L: "continuous_map X Y f" "open_map X Y f" "closed_map X Y f"
+    "f ` (topspace X) = topspace Y" "inj_on f (topspace X)"
+    by (auto simp: homeomorphic_eq_everything_map)
+  have X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> inv_into (topspace X) f (f x) = x"
+    using L by auto
+  have Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> inv_into (topspace X) f y \<in> topspace X \<and> f (inv_into (topspace X) f y) = y"
+    by (simp add: L f_inv_into_f inv_into_into)
+  have "homeomorphic_maps X Y f (inv_into (topspace X) f)"
+    unfolding homeomorphic_maps_def
+  proof (intro conjI L)
+    show "continuous_map Y X (inv_into (topspace X) f)"
+      by (simp add: L X Y flip: open_eq_continuous_inverse_map [where f=f])
+  next
+    show "\<forall>x\<in>topspace X. inv_into (topspace X) f (f x) = x"
+         "\<forall>y\<in>topspace Y. f (inv_into (topspace X) f y) = y"
+      using X Y by auto
+  qed
+  then show ?rhs
+    by metis
+next
+  assume ?rhs
+  then show ?lhs
+    using homeomorphic_maps_map by blast
+qed
+
+lemma homeomorphic_maps_involution:
+   "\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_maps X X f f"
+  by (auto simp: homeomorphic_maps_def)
+
+lemma homeomorphic_map_involution:
+   "\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_map X X f"
+  using homeomorphic_maps_involution homeomorphic_maps_map by blast
+
+lemma homeomorphic_map_openness:
+  assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
+  shows "openin Y (f ` U) \<longleftrightarrow> openin X U"
+proof -
+  obtain g where "homeomorphic_maps X Y f g"
+    using assms by (auto simp: homeomorphic_map_maps)
+  then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
+    by (auto simp: homeomorphic_maps_map)
+  then have "openin X U \<Longrightarrow> openin Y (f ` U)"
+    using hom homeomorphic_imp_open_map open_map_def by blast
+  show "openin Y (f ` U) = openin X U"
+  proof
+    assume L: "openin Y (f ` U)"
+    have "U = g ` (f ` U)"
+      using U gf by force
+    then show "openin X U"
+      by (metis L homeomorphic_imp_open_map open_map_def g)
+  next
+    assume "openin X U"
+    then show "openin Y (f ` U)"
+      using hom homeomorphic_imp_open_map open_map_def by blast
+  qed
+qed
+
+
+lemma homeomorphic_map_closedness:
+  assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
+  shows "closedin Y (f ` U) \<longleftrightarrow> closedin X U"
+proof -
+  obtain g where "homeomorphic_maps X Y f g"
+    using assms by (auto simp: homeomorphic_map_maps)
+  then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
+    by (auto simp: homeomorphic_maps_map)
+  then have "closedin X U \<Longrightarrow> closedin Y (f ` U)"
+    using hom homeomorphic_imp_closed_map closed_map_def by blast
+  show "closedin Y (f ` U) = closedin X U"
+  proof
+    assume L: "closedin Y (f ` U)"
+    have "U = g ` (f ` U)"
+      using U gf by force
+    then show "closedin X U"
+      by (metis L homeomorphic_imp_closed_map closed_map_def g)
+  next
+    assume "closedin X U"
+    then show "closedin Y (f ` U)"
+      using hom homeomorphic_imp_closed_map closed_map_def by blast
+  qed
+qed
+
+lemma homeomorphic_map_openness_eq:
+     "homeomorphic_map X Y f \<Longrightarrow> openin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> openin Y (f ` U)"
+  by (meson homeomorphic_map_openness openin_closedin_eq)
+
+lemma homeomorphic_map_closedness_eq:
+    "homeomorphic_map X Y f \<Longrightarrow> closedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> closedin Y (f ` U)"
+  by (meson closedin_subset homeomorphic_map_closedness)
+
+lemma all_openin_homeomorphic_image:
+  assumes "homeomorphic_map X Y f"
+  shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (meson assms homeomorphic_map_openness_eq)
+next
+  assume ?rhs
+  then show ?lhs
+    by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff)
+qed
+
+lemma all_closedin_homeomorphic_image:
+  assumes "homeomorphic_map X Y f"
+  shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (meson assms homeomorphic_map_closedness_eq)
+next
+  assume ?rhs
+  then show ?lhs
+    by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff)
+qed
+
+
+lemma homeomorphic_map_derived_set_of:
+  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
+  shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
+proof -
+  have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
+    using hom by (auto simp: homeomorphic_eq_everything_map)
+  have iff: "(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) =
+            (\<forall>T. T \<subseteq> topspace Y \<longrightarrow> f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))"
+    if "x \<in> topspace X" for x
+  proof -
+    have 1: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
+      by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
+    have 2: "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)" (is "?lhs = ?rhs")
+      if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
+    proof
+      show "?lhs \<Longrightarrow> ?rhs"
+        by (meson "1" imageI inj inj_on_eq_iff inj_on_subset that)
+      show "?rhs \<Longrightarrow> ?lhs"
+        using S inj inj_onD that by fastforce
+    qed
+    show ?thesis
+      apply (simp flip: fim add: all_subset_image)
+      apply (simp flip: imp_conjL)
+      by (intro all_cong1 imp_cong 1 2)
+  qed
+  have *: "\<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x \<longleftrightarrow> Q(f x)\<rbrakk> \<Longrightarrow> {y. y \<in> T \<and> Q y} = f ` {x \<in> S. P x}" for T S P Q
+    by auto
+  show ?thesis
+    unfolding derived_set_of_def
+    apply (rule *)
+    using fim apply blast
+    using iff openin_subset by force
+qed
+
+
+lemma homeomorphic_map_closure_of:
+  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
+  shows "Y closure_of (f ` S) = f ` (X closure_of S)"
+  unfolding closure_of
+  using homeomorphic_imp_surjective_map [OF hom] S
+  by (auto simp: in_derived_set_of homeomorphic_map_derived_set_of [OF assms])
+
+lemma homeomorphic_map_interior_of:
+  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
+  shows "Y interior_of (f ` S) = f ` (X interior_of S)"
+proof -
+  { fix y
+    assume "y \<in> topspace Y" and "y \<notin> Y closure_of (topspace Y - f ` S)"
+    then have "y \<in> f ` (topspace X - X closure_of (topspace X - S))"
+      using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom]
+      by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) }
+  moreover
+  { fix x
+    assume "x \<in> topspace X"
+    then have "f x \<in> topspace Y"
+      using hom homeomorphic_imp_surjective_map by blast }
+  moreover
+  { fix x
+    assume "x \<in> topspace X" and "x \<notin> X closure_of (topspace X - S)" and "f x \<in> Y closure_of (topspace Y - f ` S)"
+    then have "False"
+      using homeomorphic_map_closure_of [OF hom] hom
+      unfolding homeomorphic_eq_everything_map
+      by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
+  ultimately  show ?thesis
+    by (auto simp: interior_of_closure_of)
+qed
+
+lemma homeomorphic_map_frontier_of:
+  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
+  shows "Y frontier_of (f ` S) = f ` (X frontier_of S)"
+  unfolding frontier_of_def
+proof (intro equalityI subsetI DiffI)
+  fix y
+  assume "y \<in> Y closure_of f ` S - Y interior_of f ` S"
+  then show "y \<in> f ` (X closure_of S - X interior_of S)"
+    using S hom homeomorphic_map_closure_of homeomorphic_map_interior_of by fastforce
+next
+  fix y
+  assume "y \<in> f ` (X closure_of S - X interior_of S)"
+  then show "y \<in> Y closure_of f ` S"
+    using S hom homeomorphic_map_closure_of by fastforce
+next
+  fix x
+  assume "x \<in> f ` (X closure_of S - X interior_of S)"
+  then obtain y where y: "x = f y" "y \<in> X closure_of S" "y \<notin> X interior_of S"
+    by blast
+  then have "y \<in> topspace X"
+    by (simp add: in_closure_of)
+  then have "f y \<notin> f ` (X interior_of S)"
+    by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
+  then show "x \<notin> Y interior_of f ` S"
+    using S hom homeomorphic_map_interior_of y(1) by blast
+qed
+
+lemma homeomorphic_maps_subtopologies:
+   "\<lbrakk>homeomorphic_maps X Y f g;  f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
+        \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
+  unfolding homeomorphic_maps_def
+  by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
+
+lemma homeomorphic_maps_subtopologies_alt:
+     "\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
+      \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
+  unfolding homeomorphic_maps_def
+  by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
+
+lemma homeomorphic_map_subtopologies:
+   "\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
+        \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
+  by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies)
+
+lemma homeomorphic_map_subtopologies_alt:
+   "\<lbrakk>homeomorphic_map X Y f;
+     \<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S\<rbrakk>
+    \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
+  unfolding homeomorphic_map_maps
+  apply (erule ex_forward)
+  apply (rule homeomorphic_maps_subtopologies)
+  apply (auto simp: homeomorphic_maps_def continuous_map_def)
+  by (metis IntI image_iff)
+
+
+subsection\<open>Relation of homeomorphism between topological spaces\<close>
+
+definition homeomorphic_space (infixr "homeomorphic'_space" 50)
+  where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
+
+lemma homeomorphic_space_refl: "X homeomorphic_space X"
+  by (meson homeomorphic_maps_id homeomorphic_space_def)
+
+lemma homeomorphic_space_sym:
+   "X homeomorphic_space Y \<longleftrightarrow> Y homeomorphic_space X"
+  unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym)
+
+lemma homeomorphic_space_trans:
+     "\<lbrakk>X1 homeomorphic_space X2; X2 homeomorphic_space X3\<rbrakk> \<Longrightarrow> X1 homeomorphic_space X3"
+  unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose)
+
+lemma homeomorphic_space:
+     "X homeomorphic_space Y \<longleftrightarrow> (\<exists>f. homeomorphic_map X Y f)"
+  by (simp add: homeomorphic_map_maps homeomorphic_space_def)
+
+lemma homeomorphic_maps_imp_homeomorphic_space:
+     "homeomorphic_maps X Y f g \<Longrightarrow> X homeomorphic_space Y"
+  unfolding homeomorphic_space_def by metis
+
+lemma homeomorphic_map_imp_homeomorphic_space:
+     "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_imp_surjective_map homeomorphic_space image_is_empty)
+
+lemma homeomorphic_empty_space_eq:
+  assumes "topspace X = {}"
+    shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
+proof -
+  have "\<forall>f t. continuous_map X (t::'b topology) f"
+    using assms continuous_map_on_empty by blast
+  then show ?thesis
+    by (metis (no_types) assms continuous_map_on_empty empty_iff homeomorphic_empty_space homeomorphic_maps_def homeomorphic_space_def)
+qed
+
+subsection\<open>Connected topological spaces\<close>
+
+definition connected_space :: "'a topology \<Rightarrow> bool" where
+  "connected_space X \<equiv>
+        ~(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
+                  topspace X \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
+
+definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
+
+lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
+  by (simp add: connectedin_def)
+
+lemma connectedin_topspace:
+     "connectedin X (topspace X) \<longleftrightarrow> connected_space X"
+  by (simp add: connectedin_def)
+
+lemma connected_space_subtopology:
+     "connectedin X S \<Longrightarrow> connected_space (subtopology X S)"
+  by (simp add: connectedin_def)
+
+lemma connectedin_subtopology:
+     "connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> S"
+  by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2)
+
+lemma connected_space_eq:
+     "connected_space X \<longleftrightarrow>
+      (\<nexists>E1 E2. openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
+  unfolding connected_space_def
+  by (metis openin_Un openin_subset subset_antisym)
+
+lemma connected_space_closedin:
+     "connected_space X \<longleftrightarrow>
+      (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and> topspace X \<subseteq> E1 \<union> E2 \<and>
+               E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have L: "\<And>E1 E2. \<lbrakk>openin X E1; E1 \<inter> E2 = {}; topspace X \<subseteq> E1 \<union> E2; openin X E2\<rbrakk> \<Longrightarrow> E1 = {} \<or> E2 = {}"
+    by (simp add: connected_space_def)
+  show ?rhs
+    unfolding connected_space_def
+  proof clarify
+    fix E1 E2
+    assume "closedin X E1" and "closedin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
+      and "E1 \<noteq> {}" and "E2 \<noteq> {}"
+    have "E1 \<union> E2 = topspace X"
+      by (meson Un_subset_iff \<open>closedin X E1\<close> \<open>closedin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> closedin_def subset_antisym)
+    then have "topspace X - E2 = E1"
+      using \<open>E1 \<inter> E2 = {}\<close> by fastforce
+    then have "topspace X = E1"
+      using \<open>E1 \<noteq> {}\<close> L \<open>closedin X E1\<close> \<open>closedin X E2\<close> by blast
+    then show "False"
+      using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
+  qed
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding connected_space_def
+  proof clarify
+    fix E1 E2
+    assume "openin X E1" and "openin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
+      and "E1 \<noteq> {}" and "E2 \<noteq> {}"
+    have "E1 \<union> E2 = topspace X"
+      by (meson Un_subset_iff \<open>openin X E1\<close> \<open>openin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> openin_closedin_eq subset_antisym)
+    then have "topspace X - E2 = E1"
+      using \<open>E1 \<inter> E2 = {}\<close> by fastforce
+    then have "topspace X = E1"
+      using \<open>E1 \<noteq> {}\<close> R \<open>openin X E1\<close> \<open>openin X E2\<close> by blast
+    then show "False"
+      using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
+  qed
+qed
+
+lemma connected_space_closedin_eq:
+     "connected_space X \<longleftrightarrow>
+       (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
+                E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
+  apply (simp add: connected_space_closedin)
+  apply (intro all_cong)
+  using closedin_subset apply blast
+  done
+
+lemma connected_space_clopen_in:
+     "connected_space X \<longleftrightarrow>
+        (\<forall>T. openin X T \<and> closedin X T \<longrightarrow> T = {} \<or> T = topspace X)"
+proof -
+  have eq: "openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> P
+        \<longleftrightarrow> E2 = topspace X - E1 \<and> openin X E1 \<and> openin X E2 \<and> P" for E1 E2 P
+    using openin_subset by blast
+  show ?thesis
+    unfolding connected_space_eq eq closedin_def
+    by (auto simp: openin_closedin_eq)
+qed
+
+lemma connectedin:
+     "connectedin X S \<longleftrightarrow>
+        S \<subseteq> topspace X \<and>
+         (\<nexists>E1 E2.
+             openin X E1 \<and> openin X E2 \<and>
+             S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
+proof -
+  have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
+             R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
+    by auto
+  show ?thesis
+    unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology Not_eq_iff *
+    apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
+    apply (blast elim: dest!: openin_subset)+
+    done
+qed
+
+lemma connectedin_iff_connected_real [simp]:
+     "connectedin euclideanreal S \<longleftrightarrow> connected S"
+    by (simp add: connected_def connectedin)
+
+lemma connectedin_closedin:
+   "connectedin X S \<longleftrightarrow>
+        S \<subseteq> topspace X \<and>
+        ~(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
+                  S \<subseteq> (E1 \<union> E2) \<and>
+                  (E1 \<inter> E2 \<inter> S = {}) \<and>
+                  ~(E1 \<inter> S = {}) \<and> ~(E2 \<inter> S = {}))"
+proof -
+  have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
+             R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
+    by auto
+  show ?thesis
+    unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology Not_eq_iff *
+    apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
+    apply (blast elim: dest!: openin_subset)+
+    done
+qed
+
+lemma connectedin_empty [simp]: "connectedin X {}"
+  by (simp add: connectedin)
+
+lemma connected_space_topspace_empty:
+     "topspace X = {} \<Longrightarrow> connected_space X"
+  using connectedin_topspace by fastforce
+
+lemma connectedin_sing [simp]: "connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
+  by (simp add: connectedin)
+
+lemma connectedin_absolute [simp]:
+  "connectedin (subtopology X S) S \<longleftrightarrow> connectedin X S"
+  apply (simp only: connectedin_def topspace_subtopology subtopology_subtopology)
+  apply (intro conj_cong imp_cong arg_cong [where f=Not] all_cong1 ex_cong1 refl)
+  by auto
+
+lemma connectedin_Union:
+  assumes \<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> connectedin X S" and ne: "\<Inter>\<U> \<noteq> {}"
+  shows "connectedin X (\<Union>\<U>)"
+proof -
+  have "\<Union>\<U> \<subseteq> topspace X"
+    using \<U> by (simp add: Union_least connectedin_def)
+  moreover have False
+    if "openin X E1" "openin X E2" and cover: "\<Union>\<U> \<subseteq> E1 \<union> E2" and disj: "E1 \<inter> E2 \<inter> \<Union>\<U> = {}"
+       and overlap1: "E1 \<inter> \<Union>\<U> \<noteq> {}" and overlap2: "E2 \<inter> \<Union>\<U> \<noteq> {}"
+      for E1 E2
+  proof -
+    have disjS: "E1 \<inter> E2 \<inter> S = {}" if "S \<in> \<U>" for S
+      using Diff_triv that disj by auto
+    have coverS: "S \<subseteq> E1 \<union> E2" if "S \<in> \<U>" for S
+      using that cover by blast
+    have "\<U> \<noteq> {}"
+      using overlap1 by blast
+    obtain a where a: "\<And>U. U \<in> \<U> \<Longrightarrow> a \<in> U"
+      using ne by force
+    with \<open>\<U> \<noteq> {}\<close> have "a \<in> \<Union>\<U>"
+      by blast
+    then consider "a \<in> E1" | "a \<in> E2"
+      using \<open>\<Union>\<U> \<subseteq> E1 \<union> E2\<close> by auto
+    then show False
+    proof cases
+      case 1
+      then obtain b S where "b \<in> E2" "b \<in> S" "S \<in> \<U>"
+        using overlap2 by blast
+      then show ?thesis
+        using "1" \<open>openin X E1\<close> \<open>openin X E2\<close> disjS coverS a [OF \<open>S \<in> \<U>\<close>]  \<U>[OF \<open>S \<in> \<U>\<close>]
+        unfolding connectedin
+        by (meson disjoint_iff_not_equal)
+    next
+      case 2
+      then obtain b S where "b \<in> E1" "b \<in> S" "S \<in> \<U>"
+        using overlap1 by blast
+      then show ?thesis
+        using "2" \<open>openin X E1\<close> \<open>openin X E2\<close> disjS coverS a [OF \<open>S \<in> \<U>\<close>]  \<U>[OF \<open>S \<in> \<U>\<close>]
+        unfolding connectedin
+        by (meson disjoint_iff_not_equal)
+    qed
+  qed
+  ultimately show ?thesis
+    unfolding connectedin by blast
+qed
+
+lemma connectedin_Un:
+     "\<lbrakk>connectedin X S; connectedin X T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
+  using connectedin_Union [of "{S,T}"] by auto
+
+lemma connected_space_subconnected:
+  "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. connectedin X S \<and> x \<in> S \<and> y \<in> S)" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    using connectedin_topspace by blast
+next
+  assume R [rule_format]: ?rhs
+  have False if "openin X U" "openin X V" and disj: "U \<inter> V = {}" and cover: "topspace X \<subseteq> U \<union> V"
+    and "U \<noteq> {}" "V \<noteq> {}" for U V
+  proof -
+    obtain u v where "u \<in> U" "v \<in> V"
+      using \<open>U \<noteq> {}\<close> \<open>V \<noteq> {}\<close> by auto
+    then obtain T where "u \<in> T" "v \<in> T" and T: "connectedin X T"
+      using R [of u v] that
+      by (meson \<open>openin X U\<close> \<open>openin X V\<close> subsetD openin_subset)
+    then show False
+      using that unfolding connectedin
+      by (metis IntI \<open>u \<in> U\<close> \<open>v \<in> V\<close> empty_iff inf_bot_left subset_trans)
+  qed
+  then show ?lhs
+    by (auto simp: connected_space_def)
+qed
+
+lemma connectedin_intermediate_closure_of:
+  assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
+  shows "connectedin X T"
+proof -
+  have S: "S \<subseteq> topspace X"and T: "T \<subseteq> topspace X"
+    using assms by (meson closure_of_subset_topspace dual_order.trans)+
+  show ?thesis
+  using assms
+  apply (simp add: connectedin closure_of_subset_topspace S T)
+  apply (elim all_forward imp_forward2 asm_rl)
+  apply (blast dest: openin_Int_closure_of_eq_empty [of X _ S])+
+  done
+qed
+
+lemma connectedin_closure_of:
+     "connectedin X S \<Longrightarrow> connectedin X (X closure_of S)"
+  by (meson closure_of_subset connectedin_def connectedin_intermediate_closure_of subset_refl)
+
+lemma connectedin_separation:
+  "connectedin X S \<longleftrightarrow>
+        S \<subseteq> topspace X \<and>
+        (\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> C1 \<inter> X closure_of C2 = {} \<and> C2 \<inter> X closure_of C1 = {})" (is "?lhs = ?rhs")
+  unfolding connectedin_def connected_space_closedin_eq closedin_Int_closure_of topspace_subtopology
+  apply (intro conj_cong refl arg_cong [where f=Not])
+  apply (intro ex_cong1 iffI, blast)
+  using closure_of_subset_Int by force
+
+lemma connectedin_eq_not_separated:
+   "connectedin X S \<longleftrightarrow>
+         S \<subseteq> topspace X \<and>
+         (\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
+  apply (simp add: separatedin_def connectedin_separation)
+  apply (intro conj_cong all_cong1 refl, blast)
+  done
+
+lemma connectedin_eq_not_separated_subset:
+  "connectedin X S \<longleftrightarrow>
+      S \<subseteq> topspace X \<and> (\<nexists>C1 C2. S \<subseteq> C1 \<union> C2 \<and> S \<inter> C1 \<noteq> {} \<and> S \<inter> C2 \<noteq> {} \<and> separatedin X C1 C2)"
+proof -
+  have *: "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
+    if "\<And>C1 C2. C1 \<union> C2 = S \<longrightarrow> C1 = {} \<or> C2 = {} \<or> \<not> separatedin X C1 C2"
+  proof (intro allI)
+    fix C1 C2
+    show "S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
+      using that [of "S \<inter> C1" "S \<inter> C2"]
+      by (auto simp: separatedin_mono)
+  qed
+  show ?thesis
+    apply (simp add: connectedin_eq_not_separated)
+    apply (intro conj_cong refl iffI *)
+    apply (blast elim!: all_forward)+
+    done
+qed
+
+lemma connected_space_eq_not_separated:
+     "connected_space X \<longleftrightarrow>
+      (\<nexists>C1 C2. C1 \<union> C2 = topspace X \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
+  by (simp add: connectedin_eq_not_separated flip: connectedin_topspace)
+
+lemma connected_space_eq_not_separated_subset:
+  "connected_space X \<longleftrightarrow>
+    (\<nexists>C1 C2. topspace X \<subseteq> C1 \<union> C2 \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
+  apply (simp add: connected_space_eq_not_separated)
+  apply (intro all_cong1)
+  by (metis Un_absorb dual_order.antisym separatedin_def subset_refl sup_mono)
+
+lemma connectedin_subset_separated_union:
+     "\<lbrakk>connectedin X C; separatedin X S T; C \<subseteq> S \<union> T\<rbrakk> \<Longrightarrow> C \<subseteq> S \<or> C \<subseteq> T"
+  unfolding connectedin_eq_not_separated_subset  by blast
+
+lemma connectedin_nonseparated_union:
+   "\<lbrakk>connectedin X S; connectedin X T; ~separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
+  apply (simp add: connectedin_eq_not_separated_subset, auto)
+    apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
+  apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
+  by (meson disjoint_iff_not_equal)
+
+lemma connected_space_closures:
+     "connected_space X \<longleftrightarrow>
+        (\<nexists>e1 e2. e1 \<union> e2 = topspace X \<and> X closure_of e1 \<inter> X closure_of e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
+     (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    unfolding connected_space_closedin_eq
+    by (metis Un_upper1 Un_upper2 closedin_closure_of closure_of_Un closure_of_eq_empty closure_of_topspace)
+next
+  assume ?rhs
+  then show ?lhs
+    unfolding connected_space_closedin_eq
+    by (metis closure_of_eq)
+qed
+
+lemma connectedin_inter_frontier_of:
+  assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
+  shows "S \<inter> X frontier_of T \<noteq> {}"
+proof -
+  have "S \<subseteq> topspace X" and *:
+    "\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
+    using \<open>connectedin X S\<close> by (auto simp: connectedin)
+  have "S - (topspace X \<inter> T) \<noteq> {}"
+    using assms(3) by blast
+  moreover
+  have "S \<inter> topspace X \<inter> T \<noteq> {}"
+    using assms(1) assms(2) connectedin by fastforce
+  moreover
+  have False if "S \<inter> T \<noteq> {}" "S - T \<noteq> {}" "T \<subseteq> topspace X" "S \<inter> X frontier_of T = {}" for T
+  proof -
+    have null: "S \<inter> (X closure_of T - X interior_of T) = {}"
+      using that unfolding frontier_of_def by blast
+    have 1: "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
+      by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty)
+    have 2: "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
+      using that \<open>S \<subseteq> topspace X\<close> null by auto
+    have 3: "S \<inter> X interior_of T \<noteq> {}"
+      using closure_of_subset that(1) that(3) null by fastforce
+    show ?thesis
+      using null \<open>S \<subseteq> topspace X\<close> that * [of "X interior_of T" "topspace X - X closure_of T"]
+      apply (clarsimp simp add: openin_diff 1 2)
+      apply (simp add: Int_commute Diff_Int_distrib 3)
+      by (metis Int_absorb2 contra_subsetD interior_of_subset)
+  qed
+  ultimately show ?thesis
+    by (metis Int_lower1 frontier_of_restrict inf_assoc)
+qed
+
+lemma connectedin_continuous_map_image:
+  assumes f: "continuous_map X Y f" and "connectedin X S"
+  shows "connectedin Y (f ` S)"
+proof -
+  have "S \<subseteq> topspace X" and *:
+    "\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
+    using \<open>connectedin X S\<close> by (auto simp: connectedin)
+  show ?thesis
+    unfolding connectedin connected_space_def
+  proof (intro conjI notI; clarify)
+    show "f x \<in> topspace Y" if  "x \<in> S" for x
+      using \<open>S \<subseteq> topspace X\<close> continuous_map_image_subset_topspace f that by blast
+  next
+    fix U V
+    let ?U = "{x \<in> topspace X. f x \<in> U}"
+    let ?V = "{x \<in> topspace X. f x \<in> V}"
+    assume UV: "openin Y U" "openin Y V" "f ` S \<subseteq> U \<union> V" "U \<inter> V \<inter> f ` S = {}" "U \<inter> f ` S \<noteq> {}" "V \<inter> f ` S \<noteq> {}"
+    then have 1: "?U \<inter> ?V \<inter> S = {}"
+      by auto
+    have 2: "openin X ?U" "openin X ?V"
+      using \<open>openin Y U\<close> \<open>openin Y V\<close> continuous_map f by fastforce+
+    show "False"
+      using  * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
+      by (auto simp: 1 2)
+  qed
+qed
+
+lemma homeomorphic_connected_space:
+     "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
+  unfolding homeomorphic_space_def homeomorphic_maps_def
+  apply safe
+  apply (metis connectedin_continuous_map_image connected_space_subconnected continuous_map_image_subset_topspace image_eqI image_subset_iff)
+  by (metis (no_types, hide_lams) connectedin_continuous_map_image connectedin_topspace continuous_map_def continuous_map_image_subset_topspace imageI set_eq_subset subsetI)
+
+lemma homeomorphic_map_connectedness:
+  assumes f: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
+  shows "connectedin Y (f ` U) \<longleftrightarrow> connectedin X U"
+proof -
+  have 1: "f ` U \<subseteq> topspace Y \<longleftrightarrow> U \<subseteq> topspace X"
+    using U f homeomorphic_imp_surjective_map by blast
+  moreover have "connected_space (subtopology Y (f ` U)) \<longleftrightarrow> connected_space (subtopology X U)"
+  proof (rule homeomorphic_connected_space)
+    have "f ` U \<subseteq> topspace Y"
+      by (simp add: U 1)
+    then have "topspace Y \<inter> f ` U = f ` U"
+      by (simp add: subset_antisym)
+    then show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
+      by (metis (no_types) Int_subset_iff U f homeomorphic_map_imp_homeomorphic_space homeomorphic_map_subtopologies homeomorphic_space_sym subset_antisym subset_refl)
+  qed
+  ultimately show ?thesis
+    by (auto simp: connectedin_def)
+qed
+
+lemma homeomorphic_map_connectedness_eq:
+   "homeomorphic_map X Y f
+        \<Longrightarrow> connectedin X U \<longleftrightarrow>
+             U \<subseteq> topspace X \<and> connectedin Y (f ` U)"
+  using homeomorphic_map_connectedness connectedin_subset_topspace by metis
+
+lemma connectedin_discrete_topology:
+   "connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
+proof (cases "S \<subseteq> U")
+  case True
+  show ?thesis
+  proof (cases "S = {}")
+    case False
+    moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
+      apply safe
+      using False connectedin_inter_frontier_of insert_Diff apply fastforce
+      using True by auto
+    ultimately show ?thesis
+      by auto
+  qed simp
+next
+  case False
+  then show ?thesis
+    by (simp add: connectedin_def)
+qed
+
+lemma connected_space_discrete_topology:
+     "connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
+  by (metis connectedin_discrete_topology connectedin_topspace order_refl topspace_discrete_topology)
+
+
+subsection\<open>Compact sets\<close>
+
+definition compactin where
+ "compactin X S \<longleftrightarrow>
+     S \<subseteq> topspace X \<and>
+     (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
+          \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>))"
+
+definition compact_space where
+   "compact_space X \<equiv> compactin X (topspace X)"
+
+lemma compact_space_alt:
+   "compact_space X \<longleftrightarrow>
+        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
+            \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>))"
+  by (simp add: compact_space_def compactin_def)
+
+lemma compact_space:
+   "compact_space X \<longleftrightarrow>
+        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
+            \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> \<Union>\<F> = topspace X))"
+  unfolding compact_space_alt
+  using openin_subset by fastforce
+
+lemma compactin_euclideanreal_iff [simp]: "compactin euclideanreal S \<longleftrightarrow> compact S"
+  by (simp add: compact_eq_heine_borel compactin_def) meson
+
+lemma compactin_absolute [simp]:
+   "compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
+proof -
+  have eq: "(\<forall>U \<in> \<U>. \<exists>Y. openin X Y \<and> U = Y \<inter> S) \<longleftrightarrow> \<U> \<subseteq> (\<lambda>Y. Y \<inter> S) ` {y. openin X y}" for \<U>
+    by auto
+  show ?thesis
+    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
+qed
+
+lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
+  unfolding compact_space_def topspace_subtopology
+  by (metis compactin_absolute compactin_def inf.absorb2)
+
+lemma compact_space_subtopology: "compactin X S \<Longrightarrow> compact_space (subtopology X S)"
+  by (simp add: compactin_subspace)
+
+lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
+apply (simp add: compactin_subspace topspace_subtopology)
+  by (metis inf.orderE inf_commute subtopology_subtopology)
+
+
+lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
+  by (simp add: compactin_subspace)
+
+lemma compactin_contractive:
+   "\<lbrakk>compactin X' S; topspace X' = topspace X;
+     \<And>U. openin X U \<Longrightarrow> openin X' U\<rbrakk> \<Longrightarrow> compactin X S"
+  by (simp add: compactin_def)
+
+lemma finite_imp_compactin:
+   "\<lbrakk>S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> compactin X S"
+  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"
+  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
+
+lemma compactin_sing [simp]: "compactin X {a} \<longleftrightarrow> a \<in> topspace X"
+  by (simp add: finite_imp_compactin_eq)
+
+lemma closed_compactin:
+  assumes XK: "compactin X K" and "C \<subseteq> K" and XC: "closedin X C"
+  shows "compactin X C"
+  unfolding compactin_def
+proof (intro conjI allI impI)
+  show "C \<subseteq> topspace X"
+    by (simp add: XC closedin_subset)
+next
+  fix \<U> :: "'a set set"
+  assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
+  have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
+    using XC \<U> by blast
+  moreover have "K \<subseteq> \<Union>insert (topspace X - C) \<U>"
+    using \<U> XK compactin_subset_topspace by fastforce
+  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
+    using assms unfolding compactin_def by metis
+  moreover have "openin X (topspace X - C)"
+    using XC by auto
+  ultimately show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> C \<subseteq> \<Union>\<F>"
+    using \<open>C \<subseteq> K\<close>
+    by (rule_tac x="\<F> - {topspace X - C}" in exI) auto
+qed
+
+lemma closedin_compact_space:
+   "\<lbrakk>compact_space X; closedin X S\<rbrakk> \<Longrightarrow> compactin X S"
+  by (simp add: closed_compactin closedin_subset compact_space_def)
+
+lemma compact_Int_closedin:
+  assumes "compactin X S" "closedin X T" shows "compactin X (S \<inter> T)"
+proof -
+  have "compactin (subtopology X S) (S \<inter> T)"
+    by (metis assms closedin_compact_space closedin_subtopology compactin_subspace inf_commute)
+  then show ?thesis
+    by (simp add: compactin_subtopology)
+qed
+
+lemma closed_Int_compactin: "\<lbrakk>closedin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
+  by (metis compact_Int_closedin inf_commute)
+
+lemma compactin_Un:
+  assumes S: "compactin X S" and T: "compactin X T" shows "compactin X (S \<union> T)"
+  unfolding compactin_def
+proof (intro conjI allI impI)
+  show "S \<union> T \<subseteq> topspace X"
+    using assms by (auto simp: compactin_def)
+next
+  fix \<U> :: "'a set set"
+  assume \<U>: "Ball \<U> (openin X) \<and> S \<union> T \<subseteq> \<Union>\<U>"
+  with S obtain \<F> where \<V>: "finite \<F>" "\<F> \<subseteq> \<U>" "S \<subseteq> \<Union>\<F>"
+    unfolding compactin_def by (meson sup.bounded_iff)
+  obtain \<W> where "finite \<W>" "\<W> \<subseteq> \<U>" "T \<subseteq> \<Union>\<W>"
+    using \<U> T
+    unfolding compactin_def by (meson sup.bounded_iff)
+  with \<V> show "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> S \<union> T \<subseteq> \<Union>\<V>"
+    by (rule_tac x="\<F> \<union> \<W>" in exI) auto
+qed
+
+lemma compactin_Union:
+   "\<lbrakk>finite \<F>; \<And>S. S \<in> \<F> \<Longrightarrow> compactin X S\<rbrakk> \<Longrightarrow> compactin X (\<Union>\<F>)"
+by (induction rule: finite_induct) (simp_all add: compactin_Un)
+
+lemma compactin_subtopology_imp_compact:
+  assumes "compactin (subtopology X S) K" shows "compactin X K"
+  using assms
+proof (clarsimp simp add: compactin_def topspace_subtopology)
+  fix \<U>
+  define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
+  assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
+  then have "\<forall>V \<in> \<V>. openin (subtopology X S) V" "K \<subseteq> \<Union>\<V>"
+    unfolding \<V>_def by (auto simp: openin_subtopology)
+  moreover
+  assume "\<forall>\<U>. (\<forall>x\<in>\<U>. openin (subtopology X S) x) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
+  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
+    by meson
+  then have \<F>: "\<exists>U. U \<in> \<U> \<and> V = U \<inter> S" if "V \<in> \<F>" for V
+    unfolding \<V>_def using that by blast
+  let ?\<F> = "(\<lambda>F. @U. U \<in> \<U> \<and> F = U \<inter> S) ` \<F>"
+  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
+  proof (intro exI conjI)
+    show "finite ?\<F>"
+      using \<open>finite \<F>\<close> by blast
+    show "?\<F> \<subseteq> \<U>"
+      using someI_ex [OF \<F>] by blast
+    show "K \<subseteq> \<Union>?\<F>"
+    proof clarsimp
+      fix x
+      assume "x \<in> K"
+      then show "\<exists>V \<in> \<F>. x \<in> (SOME U. U \<in> \<U> \<and> V = U \<inter> S)"
+        using \<open>K \<subseteq> \<Union>\<F>\<close> someI_ex [OF \<F>]
+        by (metis (no_types, lifting) IntD1 Union_iff subsetCE)
+    qed
+  qed
+qed
+
+lemma compact_imp_compactin_subtopology:
+  assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
+  using assms
+proof (clarsimp simp add: compactin_def topspace_subtopology)
+  fix \<U> :: "'a set set"
+  define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
+  assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
+  then have "\<forall>V \<in> \<V>. openin X V" "K \<subseteq> \<Union>\<V>"
+    unfolding \<V>_def by (fastforce simp: subset_eq openin_subtopology)+
+  moreover
+  assume "\<forall>\<U>. (\<forall>U\<in>\<U>. openin X U) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
+  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
+    by meson
+  let ?\<F> = "(\<lambda>F. F \<inter> S) ` \<F>"
+  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
+  proof (intro exI conjI)
+    show "finite ?\<F>"
+      using \<open>finite \<F>\<close> by blast
+    show "?\<F> \<subseteq> \<U>"
+      using \<V>_def \<open>\<F> \<subseteq> \<V>\<close> by blast
+    show "K \<subseteq> \<Union>?\<F>"
+      using \<open>K \<subseteq> \<Union>\<F>\<close> assms(2) by auto
+  qed
+qed
+
+
+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 = {}")
+  case True
+  then show ?thesis
+    apply (clarsimp simp add: compact_space_def closedin_topspace_empty)
+    by (metis finite.emptyI finite_insert infinite_super insertI1 subsetI)
+next
+  case False
+  show ?thesis
+  proof safe
+    fix \<U> :: "'a set set"
+    assume * [rule_format]: "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
+    define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
+    assume clo: "\<forall>C\<in>\<U>. closedin X C" and [simp]: "\<Inter>\<U> = {}"
+    then have "\<forall>V \<in> \<V>. openin X V" "topspace X \<subseteq> \<Union>\<V>"
+      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: exists_finite_subset_image \<V>_def)
+    moreover have "\<F> \<noteq> {}"
+      using \<F> \<open>topspace X \<noteq> {}\<close> by blast
+    ultimately show "False"
+      using * [of \<F>]
+      by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
+  next
+    assume R [rule_format]: ?rhs
+    show "compact_space X"
+      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> {}"
+        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> {}"
+          by (simp add: \<V>_def all_finite_subset_image)
+        with \<open>topspace X \<subseteq> \<Union>\<U>\<close> show False
+          using R [of \<V>] * by (simp add: \<V>_def)
+      qed
+    qed
+  qed
+qed
+
+corollary compactin_fip:
+  "compactin X S \<longleftrightarrow>
+    S \<subseteq> topspace X \<and>
+    (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
+proof (cases "S = {}")
+  case False
+  show ?thesis
+  proof (cases "S \<subseteq> topspace X")
+    case True
+    then have "compactin X S \<longleftrightarrow>
+          (\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
+           (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
+      by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
+    also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {})"
+      by (simp add: all_subset_image)
+    also have "\<dots> = (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
+    proof -
+      have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> INTER \<F> ((\<inter>) S) \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {}) =
+                ((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"  for \<U>
+        by simp (use \<open>S \<noteq> {}\<close> in blast)
+      show ?thesis
+        apply (simp only: imp_conjL [symmetric] all_finite_subset_image eq)
+        apply (simp add: subset_eq)
+        done
+    qed
+    finally show ?thesis
+      using True by simp
+  qed (simp add: compactin_subspace)
+qed force
+
+corollary compact_space_imp_nest:
+  fixes C :: "nat \<Rightarrow> 'a set"
+  assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
+    and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
+  shows "(\<Inter>n. C n) \<noteq> {}"
+proof -
+  let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
+  have "closedin X A" if "A \<in> ?\<U>" for A
+    using that clo by auto
+  moreover have "(\<Inter>n\<in>K. \<Inter>m \<le> n. C m) \<noteq> {}" if "finite K" for K
+  proof -
+    obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
+      using Max.coboundedI \<open>finite K\<close> by blast
+    with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
+    by blast
+  with ne [of n] show ?thesis
+    by blast
+  qed
+  ultimately show ?thesis
+    using \<open>compact_space X\<close> [unfolded compact_space_fip, rule_format, of ?\<U>]
+    by (simp add: all_finite_subset_image INT_extend_simps UN_atMost_UNIV del: INT_simps)
+qed
+
+lemma compactin_discrete_topology:
+   "compactin (discrete_topology X) S \<longleftrightarrow> S \<subseteq> X \<and> finite S" (is "?lhs = ?rhs")
+proof (intro iffI conjI)
+  assume L: ?lhs
+  then show "S \<subseteq> X"
+    by (auto simp: compactin_def)
+  have *: "\<And>\<U>. Ball \<U> (openin (discrete_topology X)) \<and> S \<subseteq> \<Union>\<U> \<Longrightarrow>
+        (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>)"
+    using L by (auto simp: compactin_def)
+  show "finite S"
+    using * [of "(\<lambda>x. {x}) ` X"] \<open>S \<subseteq> X\<close>
+    by clarsimp (metis UN_singleton finite_subset_image infinite_super)
+next
+  assume ?rhs
+  then show ?lhs
+    by (simp add: finite_imp_compactin)
+qed
+
+lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
+  by (simp add: compactin_discrete_topology compact_space_def)
+
+lemma compact_space_imp_bolzano_weierstrass:
+  assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
+  shows "X derived_set_of S \<noteq> {}"
+proof
+  assume X: "X derived_set_of S = {}"
+  then have "closedin X S"
+    by (simp add: closedin_contains_derived_set assms)
+  then have "compactin X S"
+    by (rule closedin_compact_space [OF \<open>compact_space X\<close>])
+  with X show False
+    by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
+qed
+
+lemma compactin_imp_bolzano_weierstrass:
+   "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
+  using compact_space_imp_bolzano_weierstrass [of "subtopology X S"]
+  by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
+
+lemma compact_closure_of_imp_bolzano_weierstrass:
+   "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
+  using closure_of_mono closure_of_subset compactin_imp_bolzano_weierstrass by fastforce
+
+lemma discrete_compactin_eq_finite:
+   "S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
+  apply (rule iffI)
+  using compactin_imp_bolzano_weierstrass compactin_subset_topspace apply blast
+  by (simp add: finite_imp_compactin_eq)
+
+lemma discrete_compact_space_eq_finite:
+   "X derived_set_of (topspace X) = {} \<Longrightarrow> (compact_space X \<longleftrightarrow> finite(topspace X))"
+  by (metis compact_space_discrete_topology discrete_topology_unique_derived_set)
+
+lemma image_compactin:
+  assumes cpt: "compactin X S" and cont: "continuous_map X Y f"
+  shows "compactin Y (f ` S)"
+  unfolding compactin_def
+proof (intro conjI allI impI)
+  show "f ` S \<subseteq> topspace Y"
+    using compactin_subset_topspace cont continuous_map_image_subset_topspace cpt by blast
+next
+  fix \<U> :: "'b set set"
+  assume \<U>: "Ball \<U> (openin Y) \<and> f ` S \<subseteq> \<Union>\<U>"
+  define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
+  have "S \<subseteq> topspace X"
+    and *: "\<And>\<U>. \<lbrakk>\<forall>U\<in>\<U>. openin X U; S \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow> \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
+    using cpt by (auto simp: compactin_def)
+  obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<V>" "S \<subseteq> \<Union>\<F>"
+  proof -
+    have 1: "\<forall>U\<in>\<V>. openin X U"
+      unfolding \<V>_def using \<U> cont continuous_map by blast
+    have 2: "S \<subseteq> \<Union>\<V>"
+      unfolding \<V>_def using compactin_subset_topspace cpt \<U> by fastforce
+    show thesis
+      using * [OF 1 2] that by metis
+  qed
+  have "\<forall>v \<in> \<V>. \<exists>U. U \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U}"
+    using \<V>_def by blast
+  then obtain U where U: "\<forall>v \<in> \<V>. U v \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U v}"
+    by metis
+  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> f ` S \<subseteq> \<Union>\<F>"
+  proof (intro conjI exI)
+    show "finite (U ` \<F>)"
+      by (simp add: \<open>finite \<F>\<close>)
+  next
+    show "U ` \<F> \<subseteq> \<U>"
+      using \<open>\<F> \<subseteq> \<V>\<close> U by auto
+  next
+    show "f ` S \<subseteq> UNION \<F> U"
+      using \<F>(2-3) U UnionE subset_eq U by fastforce
+  qed
+qed
+
+
+lemma homeomorphic_compact_space:
+  assumes "X homeomorphic_space Y"
+  shows "compact_space X \<longleftrightarrow> compact_space Y"
+    using homeomorphic_space_sym
+    by (metis assms compact_space_def homeomorphic_eq_everything_map homeomorphic_space image_compactin)
+
+lemma homeomorphic_map_compactness:
+  assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
+  shows "compactin Y (f ` U) \<longleftrightarrow> compactin X U"
+proof -
+  have "f ` U \<subseteq> topspace Y"
+    using hom U homeomorphic_imp_surjective_map by blast
+  moreover have "homeomorphic_map (subtopology X U) (subtopology Y (f ` U)) f"
+    using U hom homeomorphic_imp_surjective_map by (blast intro: homeomorphic_map_subtopologies)
+  then have "compact_space (subtopology Y (f ` U)) = compact_space (subtopology X U)"
+    using homeomorphic_compact_space homeomorphic_map_imp_homeomorphic_space by blast
+  ultimately show ?thesis
+    by (simp add: compactin_subspace U)
+qed
+
+lemma homeomorphic_map_compactness_eq:
+   "homeomorphic_map X Y f
+        \<Longrightarrow> compactin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> compactin Y (f ` U)"
+  by (meson compactin_subset_topspace homeomorphic_map_compactness)
+
+
+subsection\<open>Embedding maps\<close>
+
+definition embedding_map
+  where "embedding_map X Y f \<equiv> homeomorphic_map X (subtopology Y (f ` (topspace X))) f"
+
+lemma embedding_map_eq:
+   "\<lbrakk>embedding_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> embedding_map X Y g"
+  unfolding embedding_map_def
+  by (metis homeomorphic_map_eq image_cong)
+
+lemma embedding_map_compose:
+  assumes "embedding_map X X' f" "embedding_map X' X'' g"
+  shows "embedding_map X X'' (g \<circ> f)"
+proof -
+  have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g"
+    using assms by (auto simp: embedding_map_def)
+  then obtain C where "g ` topspace X' \<inter> C = (g \<circ> f) ` topspace X"
+    by (metis (no_types) Int_absorb1 continuous_map_image_subset_topspace continuous_map_in_subtopology homeomorphic_eq_everything_map image_comp image_mono)
+  then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \<circ> f) ` topspace X)) g"
+    by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
+  then show ?thesis
+  unfolding embedding_map_def
+  using hm(1) homeomorphic_map_compose by blast
+qed
+
+lemma surjective_embedding_map:
+   "embedding_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
+  by (force simp: embedding_map_def homeomorphic_eq_everything_map)
+
+lemma embedding_map_in_subtopology:
+   "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
+  apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
+    apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
+  apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
+  done
+
+lemma injective_open_imp_embedding_map:
+   "\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
+  unfolding embedding_map_def
+  apply (rule bijective_open_imp_homeomorphic_map)
+  using continuous_map_in_subtopology apply blast
+    apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
+  done
+
+lemma injective_closed_imp_embedding_map:
+  "\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
+  unfolding embedding_map_def
+  apply (rule bijective_closed_imp_homeomorphic_map)
+     apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
+  apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
+  done
+
+lemma embedding_map_imp_homeomorphic_space:
+   "embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
+  unfolding embedding_map_def
+  using homeomorphic_space by blast
+
+end
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Analysis/Analysis.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -10,6 +10,7 @@
   Cross3
   Homeomorphism
   Bounded_Continuous_Function
+  Abstract_Topology
   Function_Topology
   Infinite_Products
   Infinite_Set_Sum
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -2853,8 +2853,6 @@
     by (simp cong: measurable_cong)
 qed
 
-lemma%unimportant Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
-
 lemma%unimportant (in sigma_finite_measure) measurable_measure[measurable (raw)]:
   "(\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M) \<Longrightarrow>
     {x \<in> space (N \<Otimes>\<^sub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^sub>M M) \<Longrightarrow>
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -1263,6 +1263,10 @@
     using assms by auto
 qed
 
+lemma linepath_le_1:
+  fixes a::"'a::linordered_idom" shows "\<lbrakk>a \<le> 1; b \<le> 1; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> (1 - u) * a + u * b \<le> 1"
+  using mult_left_le [of a "1-u"] mult_left_le [of b u] by auto
+
 
 subsection%unimportant\<open>Segments via convex hulls\<close>
 
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -635,8 +635,8 @@
   then show "T1 = T2" unfolding openin_inverse .
 qed
 
-text\<open>Infer the "universe" from union of all sets in the topology.\<close>
-
+
+text\<open>The "universe": the union of all sets in the topology.\<close>
 definition "topspace T = \<Union>{S. openin T S}"
 
 subsubsection \<open>Main properties of open sets\<close>
@@ -778,7 +778,52 @@
 qed
 
 
-subsubsection \<open>Subspace topology\<close>
+subsection\<open>The discrete topology\<close>
+
+definition discrete_topology where "discrete_topology U \<equiv> topology (\<lambda>S. S \<subseteq> U)"
+
+lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
+proof -
+  have "istopology (\<lambda>S. S \<subseteq> U)"
+    by (auto simp: istopology_def)
+  then show ?thesis
+    by (simp add: discrete_topology_def topology_inverse')
+qed
+
+lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U"
+  by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)
+
+lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
+  by (simp add: Diff_subset closedin_def)
+
+lemma discrete_topology_unique:
+   "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
+proof
+  assume R: ?rhs
+  then have "openin X S" if "S \<subseteq> U" for S
+    using openin_subopen subsetD that by fastforce
+  moreover have "x \<in> topspace X" if "openin X S" and "x \<in> S" for x S
+    using openin_subset that by blast
+  ultimately
+  show ?lhs
+    using R by (auto simp: topology_eq)
+qed auto
+
+lemma discrete_topology_unique_alt:
+  "discrete_topology U = X \<longleftrightarrow> topspace X \<subseteq> U \<and> (\<forall>x \<in> U. openin X {x})"
+  using openin_subset
+  by (auto simp: discrete_topology_unique)
+
+lemma subtopology_eq_discrete_topology_empty:
+   "X = discrete_topology {} \<longleftrightarrow> topspace X = {}"
+  using discrete_topology_unique [of "{}" X] by auto
+
+lemma subtopology_eq_discrete_topology_sing:
+   "X = discrete_topology {a} \<longleftrightarrow> topspace X = {a}"
+  by (metis discrete_topology_unique openin_topspace singletonD)
+
+
+subsection \<open>Subspace topology\<close>
 
 definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
 
@@ -818,6 +863,19 @@
   unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
   by auto
 
+lemma openin_subtopology_Int:
+   "openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
+  using openin_subtopology by auto
+
+lemma openin_subtopology_Int2:
+   "openin X T \<Longrightarrow> openin (subtopology X S) (S \<inter> T)"
+  using openin_subtopology by auto
+
+lemma openin_subtopology_diff_closed:
+   "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> openin (subtopology X S) (S - T)"
+  unfolding closedin_def openin_subtopology
+  by (rule_tac x="topspace X - T" in exI) auto
+
 lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
   by (force simp: relative_to_def openin_subtopology)
 
@@ -927,7 +985,7 @@
 by (simp add: closedin_subtopology) blast
 
 
-subsubsection \<open>The standard Euclidean topology\<close>
+subsection \<open>The standard Euclidean topology\<close>
 
 definition%important euclidean :: "'a::topological_space topology"
   where "euclidean = topology open"
@@ -958,7 +1016,25 @@
 lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
   by (metis openin_topspace topspace_euclidean_subtopology)
 
-text \<open>Basic "localization" results are handy for connectedness.\<close>
+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 real_openin [simp]: "openin euclideanreal S = open S"
+  by (simp add: euclidean_def open_openin)
+
+lemma topspace_euclideanreal [simp]: "topspace euclideanreal = UNIV"
+  using openin_subset open_UNIV real_openin by blast
+
+lemma topspace_euclideanreal_subtopology [simp]:
+   "topspace (subtopology euclideanreal S) = S"
+  by (simp add: topspace_subtopology)
+
+lemma real_closedin [simp]: "closedin euclideanreal S = closed S"
+  by (simp add: closed_closedin euclidean_def)
+
+subsection \<open>Basic "localization" results are handy for connectedness.\<close>
 
 lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
   by (auto simp: openin_subtopology)
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -974,6 +974,12 @@
   then show ?thesis by simp
 qed
 
+lemma sum_bounded_above_divide:
+  fixes K :: "'a::linordered_field"
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> K / of_nat (card A)" and fin: "finite A" "A \<noteq> {}"
+  shows "sum f A \<le> K"
+  using sum_bounded_above [of A f "K / of_nat (card A)", OF le] fin by simp
+
 lemma sum_bounded_above_strict:
   fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}"
   assumes "\<And>i. i\<in>A \<Longrightarrow> f i < K" "card A > 0"
@@ -994,6 +1000,27 @@
   then show ?thesis by simp
 qed
 
+lemma convex_sum_bound_le:
+  fixes x :: "'a \<Rightarrow> 'b::linordered_idom"
+  assumes 0: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> x i" and 1: "sum x I = 1"
+      and \<delta>: "\<And>i. i \<in> I \<Longrightarrow> \<bar>a i - b\<bar> \<le> \<delta>"
+    shows "\<bar>(\<Sum>i\<in>I. a i * x i) - b\<bar> \<le> \<delta>"
+proof -
+  have [simp]: "(\<Sum>i\<in>I. c * x i) = c" for c
+    by (simp flip: sum_distrib_left 1)
+  then have "\<bar>(\<Sum>i\<in>I. a i * x i) - b\<bar> = \<bar>\<Sum>i\<in>I. (a i - b) * x i\<bar>"
+    by (simp add: sum_subtractf left_diff_distrib)
+  also have "\<dots> \<le> (\<Sum>i\<in>I. \<bar>(a i - b) * x i\<bar>)"
+    using abs_abs abs_of_nonneg by blast
+  also have "\<dots> \<le> (\<Sum>i\<in>I. \<bar>(a i - b)\<bar> * x i)"
+    by (simp add: abs_mult 0)
+  also have "\<dots> \<le> (\<Sum>i\<in>I. \<delta> * x i)"
+    by (rule sum_mono) (use \<delta> "0" mult_right_mono in blast)
+  also have "\<dots> = \<delta>"
+    by simp
+  finally show ?thesis .
+qed
+
 lemma card_UN_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -570,6 +570,40 @@
   done
 
 
+subsubsection \<open>Misc properties of functions, composition and restriction from HOL Light\<close>
+
+lemma function_factors_left_gen:
+  "(\<forall>x y. P x \<and> P y \<and> g x = g y \<longrightarrow> f x = f y) \<longleftrightarrow> (\<exists>h. \<forall>x. P x \<longrightarrow> f x = h(g x))"
+  (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then show ?rhs
+    apply (rule_tac x="f \<circ> inv_into (Collect P) g" in exI)
+    unfolding o_def
+    by (metis (mono_tags, hide_lams) f_inv_into_f imageI inv_into_into mem_Collect_eq)
+qed auto
+
+lemma function_factors_left:
+  "(\<forall>x y. (g x = g y) \<longrightarrow> (f x = f y)) \<longleftrightarrow> (\<exists>h. f = h \<circ> g)"
+  using function_factors_left_gen [of "\<lambda>x. True" g f] unfolding o_def by blast
+
+lemma function_factors_right_gen:
+  "(\<forall>x. P x \<longrightarrow> (\<exists>y. g y = f x)) \<longleftrightarrow> (\<exists>h. \<forall>x. P x \<longrightarrow> f x = g(h x))"
+  by metis
+
+lemma function_factors_right:
+  "(\<forall>x. \<exists>y. g y = f x) \<longleftrightarrow> (\<exists>h. f = g \<circ> h)"
+  unfolding o_def by metis
+
+lemma restrict_compose_right:
+   "restrict (g \<circ> restrict f S) S = restrict (g \<circ> f) S"
+  by auto
+
+lemma restrict_compose_left:
+   "f ` S \<subseteq> T \<Longrightarrow> restrict (restrict g T \<circ> f) S = restrict (g \<circ> f) S"
+  by fastforce
+
+
 subsubsection \<open>Cardinality\<close>
 
 lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (\<Pi>\<^sub>E i \<in> S. T i)"
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Meson.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -106,6 +106,9 @@
 lemma imp_forward: "\<lbrakk>P' \<longrightarrow> Q';  P \<Longrightarrow> P';  Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P \<longrightarrow> Q"
 by blast
 
+lemma imp_forward2: "\<lbrakk>P' \<longrightarrow> Q';  P \<Longrightarrow> P';  P' \<Longrightarrow> Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P \<longrightarrow> Q"
+  by blast
+
 (*Version of @{text disj_forward} for removal of duplicate literals*)
 lemma disj_forward2: "\<lbrakk> P'\<or>Q';  P' \<Longrightarrow> P;  \<lbrakk>Q'; P\<Longrightarrow>False\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> P\<or>Q"
 apply blast 
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -436,7 +436,7 @@
 subsection \<open>fixed points\<close>
 
 lemma fix_subset: "fix f A \<subseteq> A"
-by (simp add: fix_def, fast)
+by (auto simp add: fix_def)
 
 lemma fix_imp_eq: "x \<in> fix f A ==> f x = x"
 by (simp add: fix_def)
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -1100,6 +1100,9 @@
 lemma Times_empty [simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   by auto
 
+lemma times_subset_iff: "A \<times> C \<subseteq> B \<times> D \<longleftrightarrow> A={} \<or> C={} \<or> A \<subseteq> B \<and> C \<subseteq> D"
+  by blast
+
 lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
   by auto
 
diff -r 5acb1eece41b -r f13b82281715 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Set.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -1140,6 +1140,8 @@
 lemma not_psubset_empty [iff]: "\<not> (A < {})"
   by (fact not_less_bot) (* FIXME: already simp *)
 
+lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
+
 lemma Collect_empty_eq [simp]: "Collect P = {} \<longleftrightarrow> (\<forall>x. \<not> P x)"
   by blast
 
diff -r 5acb1eece41b -r f13b82281715 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Wed Oct 17 14:19:07 2018 +0100
@@ -62,10 +62,7 @@
 text\<open>The next three results state that @{term "cl L r"} is the minimal
  element of @{term L} that includes @{term r}.\<close>
 lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
-apply (simp add: lattice_def cl_def)
-apply (erule conjE)  
-apply (drule spec, erule mp, blast) 
-done
+  by (simp add: lattice_def cl_def)
 
 lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
 by (force simp add: cl_def)