src/HOL/Analysis/Abstract_Topology.thy
 author haftmann Sun Nov 18 18:07:51 2018 +0000 (8 months ago) changeset 69313 b021008c5397 parent 69286 e4d5a07fecb6 child 69325 4b6ddc5989fc permissions -rw-r--r--
removed legacy input syntax
```     1 (*  Author:     L C Paulson, University of Cambridge [ported from HOL Light]
```
```     2 *)
```
```     3
```
```     4 section \<open>Operators involving abstract topology\<close>
```
```     5
```
```     6 theory Abstract_Topology
```
```     7   imports Topology_Euclidean_Space Path_Connected
```
```     8 begin
```
```     9
```
```    10
```
```    11 subsection\<open>Derived set (set of limit points)\<close>
```
```    12
```
```    13 definition derived_set_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "derived'_set'_of" 80)
```
```    14   where "X derived_set_of S \<equiv>
```
```    15          {x \<in> topspace X.
```
```    16                 (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
```
```    17
```
```    18 lemma derived_set_of_restrict:
```
```    19    "X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
```
```    20   by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
```
```    21
```
```    22 lemma in_derived_set_of:
```
```    23    "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))"
```
```    24   by (simp add: derived_set_of_def)
```
```    25
```
```    26 lemma derived_set_of_subset_topspace:
```
```    27    "X derived_set_of S \<subseteq> topspace X"
```
```    28   by (auto simp add: derived_set_of_def)
```
```    29
```
```    30 lemma derived_set_of_subtopology:
```
```    31    "(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
```
```    32   by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast
```
```    33
```
```    34 lemma derived_set_of_subset_subtopology:
```
```    35    "(subtopology X S) derived_set_of T \<subseteq> S"
```
```    36   by (simp add: derived_set_of_subtopology)
```
```    37
```
```    38 lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}"
```
```    39   by (auto simp: derived_set_of_def)
```
```    40
```
```    41 lemma derived_set_of_mono:
```
```    42    "S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
```
```    43   unfolding derived_set_of_def by blast
```
```    44
```
```    45 lemma derived_set_of_union:
```
```    46    "X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
```
```    47 proof
```
```    48   show "?lhs \<subseteq> ?rhs"
```
```    49     apply (clarsimp simp: in_derived_set_of)
```
```    50     by (metis IntE IntI openin_Int)
```
```    51   show "?rhs \<subseteq> ?lhs"
```
```    52     by (simp add: derived_set_of_mono)
```
```    53 qed
```
```    54
```
```    55 lemma derived_set_of_unions:
```
```    56    "finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
```
```    57 proof (induction \<F> rule: finite_induct)
```
```    58   case (insert S \<F>)
```
```    59   then show ?case
```
```    60     by (simp add: derived_set_of_union)
```
```    61 qed auto
```
```    62
```
```    63 lemma derived_set_of_topspace:
```
```    64   "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
```
```    65   apply (auto simp: in_derived_set_of)
```
```    66   by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)
```
```    67
```
```    68 lemma discrete_topology_unique_derived_set:
```
```    69      "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
```
```    70   by (auto simp: discrete_topology_unique derived_set_of_topspace)
```
```    71
```
```    72 lemma subtopology_eq_discrete_topology_eq:
```
```    73    "subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
```
```    74   using discrete_topology_unique_derived_set [of U "subtopology X U"]
```
```    75   by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)
```
```    76
```
```    77 lemma subtopology_eq_discrete_topology:
```
```    78    "S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
```
```    79         \<Longrightarrow> subtopology X S = discrete_topology S"
```
```    80   by (simp add: subtopology_eq_discrete_topology_eq)
```
```    81
```
```    82 lemma subtopology_eq_discrete_topology_gen:
```
```    83    "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
```
```    84   by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
```
```    85
```
```    86 lemma openin_Int_derived_set_of_subset:
```
```    87    "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
```
```    88   by (auto simp: derived_set_of_def)
```
```    89
```
```    90 lemma openin_Int_derived_set_of_eq:
```
```    91   "openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
```
```    92   apply auto
```
```    93    apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
```
```    94   by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)
```
```    95
```
```    96
```
```    97 subsection\<open> Closure with respect to a topological space\<close>
```
```    98
```
```    99 definition closure_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "closure'_of" 80)
```
```   100   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)}"
```
```   101
```
```   102 lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
```
```   103   unfolding closure_of_def
```
```   104   apply safe
```
```   105   apply (meson IntI openin_subset subset_iff)
```
```   106   by auto
```
```   107
```
```   108 lemma in_closure_of:
```
```   109    "x \<in> X closure_of S \<longleftrightarrow>
```
```   110     x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
```
```   111   by (auto simp: closure_of_def)
```
```   112
```
```   113 lemma closure_of: "X closure_of S = topspace X \<inter> (S \<union> X derived_set_of S)"
```
```   114   by (fastforce simp: in_closure_of in_derived_set_of)
```
```   115
```
```   116 lemma closure_of_alt: "X closure_of S = topspace X \<inter> S \<union> X derived_set_of S"
```
```   117   using derived_set_of_subset_topspace [of X S]
```
```   118   unfolding closure_of_def in_derived_set_of
```
```   119   by safe (auto simp: in_derived_set_of)
```
```   120
```
```   121 lemma derived_set_of_subset_closure_of:
```
```   122    "X derived_set_of S \<subseteq> X closure_of S"
```
```   123   by (fastforce simp: closure_of_def in_derived_set_of)
```
```   124
```
```   125 lemma closure_of_subtopology:
```
```   126   "(subtopology X U) closure_of S = U \<inter> (X closure_of (U \<inter> S))"
```
```   127   unfolding closure_of_def topspace_subtopology openin_subtopology
```
```   128   by safe (metis (full_types) IntI Int_iff inf.commute)+
```
```   129
```
```   130 lemma closure_of_empty [simp]: "X closure_of {} = {}"
```
```   131   by (simp add: closure_of_alt)
```
```   132
```
```   133 lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"
```
```   134   by (simp add: closure_of)
```
```   135
```
```   136 lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"
```
```   137   by (simp add: closure_of)
```
```   138
```
```   139 lemma closure_of_subset_topspace: "X closure_of S \<subseteq> topspace X"
```
```   140   by (simp add: closure_of)
```
```   141
```
```   142 lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T \<subseteq> S"
```
```   143   by (simp add: closure_of_subtopology)
```
```   144
```
```   145 lemma closure_of_mono: "S \<subseteq> T \<Longrightarrow> X closure_of S \<subseteq> X closure_of T"
```
```   146   by (fastforce simp add: closure_of_def)
```
```   147
```
```   148 lemma closure_of_subtopology_subset:
```
```   149    "(subtopology X U) closure_of S \<subseteq> (X closure_of S)"
```
```   150   unfolding closure_of_subtopology
```
```   151   by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2)
```
```   152
```
```   153 lemma closure_of_subtopology_mono:
```
```   154    "T \<subseteq> U \<Longrightarrow> (subtopology X T) closure_of S \<subseteq> (subtopology X U) closure_of S"
```
```   155   unfolding closure_of_subtopology
```
```   156   by auto (meson closure_of_mono inf_mono subset_iff)
```
```   157
```
```   158 lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
```
```   159   by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_union inf_sup_distrib1)
```
```   160
```
```   161 lemma closure_of_Union:
```
```   162    "finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
```
```   163 by (induction \<F> rule: finite_induct) auto
```
```   164
```
```   165 lemma closure_of_subset: "S \<subseteq> topspace X \<Longrightarrow> S \<subseteq> X closure_of S"
```
```   166   by (auto simp: closure_of_def)
```
```   167
```
```   168 lemma closure_of_subset_Int: "topspace X \<inter> S \<subseteq> X closure_of S"
```
```   169   by (auto simp: closure_of_def)
```
```   170
```
```   171 lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
```
```   172 proof (cases "S \<subseteq> topspace X")
```
```   173   case True
```
```   174   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
```
```   175              \<Longrightarrow> openin X (topspace X - S)"
```
```   176     apply (subst openin_subopen, safe)
```
```   177     by (metis DiffI subset_eq openin_subset [of X])
```
```   178   then show ?thesis
```
```   179     by (auto simp: closedin_def closure_of_def)
```
```   180 next
```
```   181   case False
```
```   182   then show ?thesis
```
```   183     by (simp add: closedin_def)
```
```   184 qed
```
```   185
```
```   186 lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
```
```   187 proof (cases "S \<subseteq> topspace X")
```
```   188   case True
```
```   189   then show ?thesis
```
```   190     by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
```
```   191 next
```
```   192   case False
```
```   193   then show ?thesis
```
```   194     using closure_of closure_of_subset_eq by fastforce
```
```   195 qed
```
```   196
```
```   197 lemma closedin_contains_derived_set:
```
```   198    "closedin X S \<longleftrightarrow> X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X"
```
```   199 proof (intro iffI conjI)
```
```   200   show "closedin X S \<Longrightarrow> X derived_set_of S \<subseteq> S"
```
```   201     using closure_of_eq derived_set_of_subset_closure_of by fastforce
```
```   202   show "closedin X S \<Longrightarrow> S \<subseteq> topspace X"
```
```   203     using closedin_subset by blast
```
```   204   show "X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X \<Longrightarrow> closedin X S"
```
```   205     by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
```
```   206 qed
```
```   207
```
```   208 lemma derived_set_subset_gen:
```
```   209    "X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X (topspace X \<inter> S)"
```
```   210   by (simp add: closedin_contains_derived_set derived_set_of_restrict derived_set_of_subset_topspace)
```
```   211
```
```   212 lemma derived_set_subset: "S \<subseteq> topspace X \<Longrightarrow> (X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X S)"
```
```   213   by (simp add: closedin_contains_derived_set)
```
```   214
```
```   215 lemma closedin_derived_set:
```
```   216      "closedin (subtopology X T) S \<longleftrightarrow>
```
```   217       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)"
```
```   218   by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)
```
```   219
```
```   220 lemma closedin_Int_closure_of:
```
```   221      "closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
```
```   222   by (metis Int_left_absorb closure_of_eq closure_of_subtopology)
```
```   223
```
```   224 lemma closure_of_closedin: "closedin X S \<Longrightarrow> X closure_of S = S"
```
```   225   by (simp add: closure_of_eq)
```
```   226
```
```   227 lemma closure_of_eq_diff: "X closure_of S = topspace X - \<Union>{T. openin X T \<and> disjnt S T}"
```
```   228   by (auto simp: closure_of_def disjnt_iff)
```
```   229
```
```   230 lemma closedin_closure_of [simp]: "closedin X (X closure_of S)"
```
```   231   unfolding closure_of_eq_diff by blast
```
```   232
```
```   233 lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S"
```
```   234   by (simp add: closure_of_eq)
```
```   235
```
```   236 lemma closure_of_hull:
```
```   237   assumes "S \<subseteq> topspace X" shows "X closure_of S = (closedin X) hull S"
```
```   238 proof (rule hull_unique [THEN sym])
```
```   239   show "S \<subseteq> X closure_of S"
```
```   240     by (simp add: closure_of_subset assms)
```
```   241 next
```
```   242   show "closedin X (X closure_of S)"
```
```   243     by simp
```
```   244   show "\<And>T. \<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> X closure_of S \<subseteq> T"
```
```   245     by (metis closure_of_eq closure_of_mono)
```
```   246 qed
```
```   247
```
```   248 lemma closure_of_minimal:
```
```   249    "\<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T"
```
```   250   by (metis closure_of_eq closure_of_mono)
```
```   251
```
```   252 lemma closure_of_minimal_eq:
```
```   253    "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T \<longleftrightarrow> S \<subseteq> T"
```
```   254   by (meson closure_of_minimal closure_of_subset subset_trans)
```
```   255
```
```   256 lemma closure_of_unique:
```
```   257    "\<lbrakk>S \<subseteq> T; closedin X T;
```
```   258      \<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
```
```   259     \<Longrightarrow> X closure_of S = T"
```
```   260   by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)
```
```   261
```
```   262 lemma closure_of_eq_empty_gen: "X closure_of S = {} \<longleftrightarrow> disjnt (topspace X) S"
```
```   263   unfolding disjnt_def closure_of_restrict [where S=S]
```
```   264   using closure_of by fastforce
```
```   265
```
```   266 lemma closure_of_eq_empty: "S \<subseteq> topspace X \<Longrightarrow> X closure_of S = {} \<longleftrightarrow> S = {}"
```
```   267   using closure_of_subset by fastforce
```
```   268
```
```   269 lemma openin_Int_closure_of_subset:
```
```   270   assumes "openin X S"
```
```   271   shows "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
```
```   272 proof -
```
```   273   have "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
```
```   274     by (meson assms openin_Int_derived_set_of_eq)
```
```   275   moreover have "S \<inter> (S \<inter> T) = S \<inter> T"
```
```   276     by fastforce
```
```   277   ultimately show ?thesis
```
```   278     by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1)
```
```   279 qed
```
```   280
```
```   281 lemma closure_of_openin_Int_closure_of:
```
```   282   assumes "openin X S"
```
```   283   shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)"
```
```   284 proof
```
```   285   show "X closure_of (S \<inter> X closure_of T) \<subseteq> X closure_of (S \<inter> T)"
```
```   286     by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
```
```   287 next
```
```   288   show "X closure_of (S \<inter> T) \<subseteq> X closure_of (S \<inter> X closure_of T)"
```
```   289     by (metis Int_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
```
```   290 qed
```
```   291
```
```   292 lemma openin_Int_closure_of_eq:
```
```   293   "openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
```
```   294   apply (rule equalityI)
```
```   295    apply (simp add: openin_Int_closure_of_subset)
```
```   296   by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)
```
```   297
```
```   298 lemma openin_Int_closure_of_eq_empty:
```
```   299    "openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
```
```   300   apply (subst openin_Int_closure_of_eq, auto)
```
```   301   by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)
```
```   302
```
```   303 lemma closure_of_openin_Int_superset:
```
```   304    "openin X S \<and> S \<subseteq> X closure_of T
```
```   305         \<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
```
```   306   by (metis closure_of_openin_Int_closure_of inf.orderE)
```
```   307
```
```   308 lemma closure_of_openin_subtopology_Int_closure_of:
```
```   309   assumes S: "openin (subtopology X U) S" and "T \<subseteq> U"
```
```   310   shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
```
```   311 proof
```
```   312   obtain S0 where S0: "openin X S0" "S = S0 \<inter> U"
```
```   313     using assms by (auto simp: openin_subtopology)
```
```   314   show "?lhs \<subseteq> ?rhs"
```
```   315   proof -
```
```   316     have "S0 \<inter> X closure_of T = S0 \<inter> X closure_of (S0 \<inter> T)"
```
```   317       by (meson S0(1) openin_Int_closure_of_eq)
```
```   318     moreover have "S0 \<inter> T = S0 \<inter> U \<inter> T"
```
```   319       using \<open>T \<subseteq> U\<close> by fastforce
```
```   320     ultimately have "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
```
```   321       using S0(2) by auto
```
```   322     then show ?thesis
```
```   323       by (meson closedin_closure_of closure_of_minimal)
```
```   324   qed
```
```   325 next
```
```   326   show "?rhs \<subseteq> ?lhs"
```
```   327   proof -
```
```   328     have "T \<inter> S \<subseteq> T \<union> X derived_set_of T"
```
```   329       by force
```
```   330     then show ?thesis
```
```   331       by (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
```
```   332   qed
```
```   333 qed
```
```   334
```
```   335 lemma closure_of_subtopology_open:
```
```   336      "openin X U \<or> S \<subseteq> U \<Longrightarrow> (subtopology X U) closure_of S = U \<inter> X closure_of S"
```
```   337   by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq)
```
```   338
```
```   339 lemma discrete_topology_closure_of:
```
```   340      "(discrete_topology U) closure_of S = U \<inter> S"
```
```   341   by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)
```
```   342
```
```   343
```
```   344 text\<open> Interior with respect to a topological space.                             \<close>
```
```   345
```
```   346 definition interior_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "interior'_of" 80)
```
```   347   where "X interior_of S \<equiv> {x. \<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> S}"
```
```   348
```
```   349 lemma interior_of_restrict:
```
```   350    "X interior_of S = X interior_of (topspace X \<inter> S)"
```
```   351   using openin_subset by (auto simp: interior_of_def)
```
```   352
```
```   353 lemma interior_of_eq: "(X interior_of S = S) \<longleftrightarrow> openin X S"
```
```   354   unfolding interior_of_def  using openin_subopen by blast
```
```   355
```
```   356 lemma interior_of_openin: "openin X S \<Longrightarrow> X interior_of S = S"
```
```   357   by (simp add: interior_of_eq)
```
```   358
```
```   359 lemma interior_of_empty [simp]: "X interior_of {} = {}"
```
```   360   by (simp add: interior_of_eq)
```
```   361
```
```   362 lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X"
```
```   363   by (simp add: interior_of_eq)
```
```   364
```
```   365 lemma openin_interior_of [simp]: "openin X (X interior_of S)"
```
```   366   unfolding interior_of_def
```
```   367   using openin_subopen by fastforce
```
```   368
```
```   369 lemma interior_of_interior_of [simp]:
```
```   370    "X interior_of X interior_of S = X interior_of S"
```
```   371   by (simp add: interior_of_eq)
```
```   372
```
```   373 lemma interior_of_subset: "X interior_of S \<subseteq> S"
```
```   374   by (auto simp: interior_of_def)
```
```   375
```
```   376 lemma interior_of_subset_closure_of: "X interior_of S \<subseteq> X closure_of S"
```
```   377   by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset)
```
```   378
```
```   379 lemma subset_interior_of_eq: "S \<subseteq> X interior_of S \<longleftrightarrow> openin X S"
```
```   380   by (metis interior_of_eq interior_of_subset subset_antisym)
```
```   381
```
```   382 lemma interior_of_mono: "S \<subseteq> T \<Longrightarrow> X interior_of S \<subseteq> X interior_of T"
```
```   383   by (auto simp: interior_of_def)
```
```   384
```
```   385 lemma interior_of_maximal: "\<lbrakk>T \<subseteq> S; openin X T\<rbrakk> \<Longrightarrow> T \<subseteq> X interior_of S"
```
```   386   by (auto simp: interior_of_def)
```
```   387
```
```   388 lemma interior_of_maximal_eq: "openin X T \<Longrightarrow> T \<subseteq> X interior_of S \<longleftrightarrow> T \<subseteq> S"
```
```   389   by (meson interior_of_maximal interior_of_subset order_trans)
```
```   390
```
```   391 lemma interior_of_unique:
```
```   392    "\<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"
```
```   393   by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym)
```
```   394
```
```   395 lemma interior_of_subset_topspace: "X interior_of S \<subseteq> topspace X"
```
```   396   by (simp add: openin_subset)
```
```   397
```
```   398 lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
```
```   399   by (meson openin_imp_subset openin_interior_of)
```
```   400
```
```   401 lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
```
```   402   apply (rule equalityI)
```
```   403    apply (simp add: interior_of_mono)
```
```   404   apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
```
```   405   done
```
```   406
```
```   407 lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
```
```   408   by (simp add: INT_greatest Inf_lower interior_of_mono)
```
```   409
```
```   410 lemma union_interior_of_subset:
```
```   411    "X interior_of S \<union> X interior_of T \<subseteq> X interior_of (S \<union> T)"
```
```   412   by (simp add: interior_of_mono)
```
```   413
```
```   414 lemma interior_of_eq_empty:
```
```   415    "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<subseteq> S \<longrightarrow> T = {})"
```
```   416   by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of)
```
```   417
```
```   418 lemma interior_of_eq_empty_alt:
```
```   419    "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> T - S \<noteq> {})"
```
```   420   by (auto simp: interior_of_eq_empty)
```
```   421
```
```   422 lemma interior_of_Union_openin_subsets:
```
```   423    "\<Union>{T. openin X T \<and> T \<subseteq> S} = X interior_of S"
```
```   424   by (rule interior_of_unique [symmetric]) auto
```
```   425
```
```   426 lemma interior_of_complement:
```
```   427    "X interior_of (topspace X - S) = topspace X - X closure_of S"
```
```   428   by (auto simp: interior_of_def closure_of_def)
```
```   429
```
```   430 lemma interior_of_closure_of:
```
```   431    "X interior_of S = topspace X - X closure_of (topspace X - S)"
```
```   432   unfolding interior_of_complement [symmetric]
```
```   433   by (metis Diff_Diff_Int interior_of_restrict)
```
```   434
```
```   435 lemma closure_of_interior_of:
```
```   436    "X closure_of S = topspace X - X interior_of (topspace X - S)"
```
```   437   by (simp add: interior_of_complement Diff_Diff_Int closure_of)
```
```   438
```
```   439 lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S"
```
```   440   unfolding interior_of_def closure_of_def
```
```   441   by (blast dest: openin_subset)
```
```   442
```
```   443 lemma interior_of_eq_empty_complement:
```
```   444   "X interior_of S = {} \<longleftrightarrow> X closure_of (topspace X - S) = topspace X"
```
```   445   using interior_of_subset_topspace [of X S] closure_of_complement by fastforce
```
```   446
```
```   447 lemma closure_of_eq_topspace:
```
```   448    "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
```
```   449   using closure_of_subset_topspace [of X S] interior_of_complement by fastforce
```
```   450
```
```   451 lemma interior_of_subtopology_subset:
```
```   452      "U \<inter> X interior_of S \<subseteq> (subtopology X U) interior_of S"
```
```   453   by (auto simp: interior_of_def openin_subtopology)
```
```   454
```
```   455 lemma interior_of_subtopology_subsets:
```
```   456    "T \<subseteq> U \<Longrightarrow> T \<inter> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
```
```   457   by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)
```
```   458
```
```   459 lemma interior_of_subtopology_mono:
```
```   460    "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
```
```   461   by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets)
```
```   462
```
```   463 lemma interior_of_subtopology_open:
```
```   464   assumes "openin X U"
```
```   465   shows "(subtopology X U) interior_of S = U \<inter> X interior_of S"
```
```   466 proof -
```
```   467   have "\<forall>A. U \<inter> X closure_of (U \<inter> A) = U \<inter> X closure_of A"
```
```   468     using assms openin_Int_closure_of_eq by blast
```
```   469   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))"
```
```   470     by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
```
```   471   then show ?thesis
```
```   472     unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
```
```   473     using openin_Int_closure_of_eq [OF assms]
```
```   474     by (metis assms closure_of_subtopology_open)
```
```   475 qed
```
```   476
```
```   477 lemma dense_intersects_open:
```
```   478    "X closure_of S = topspace X \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
```
```   479 proof -
```
```   480   have "X closure_of S = topspace X \<longleftrightarrow> (topspace X - X interior_of (topspace X - S) = topspace X)"
```
```   481     by (simp add: closure_of_interior_of)
```
```   482   also have "\<dots> \<longleftrightarrow> X interior_of (topspace X - S) = {}"
```
```   483     by (simp add: closure_of_complement interior_of_eq_empty_complement)
```
```   484   also have "\<dots> \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
```
```   485     unfolding interior_of_eq_empty_alt
```
```   486     using openin_subset by fastforce
```
```   487   finally show ?thesis .
```
```   488 qed
```
```   489
```
```   490 lemma interior_of_closedin_union_empty_interior_of:
```
```   491   assumes "closedin X S" and disj: "X interior_of T = {}"
```
```   492   shows "X interior_of (S \<union> T) = X interior_of S"
```
```   493 proof -
```
```   494   have "X closure_of (topspace X - T) = topspace X"
```
```   495     by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of)
```
```   496   then show ?thesis
```
```   497     unfolding interior_of_closure_of
```
```   498     by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset)
```
```   499 qed
```
```   500
```
```   501 lemma interior_of_union_eq_empty:
```
```   502    "closedin X S
```
```   503         \<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
```
```   504              X interior_of S = {} \<and> X interior_of T = {})"
```
```   505   by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)
```
```   506
```
```   507 lemma discrete_topology_interior_of [simp]:
```
```   508     "(discrete_topology U) interior_of S = U \<inter> S"
```
```   509   by (simp add: interior_of_restrict [of _ S] interior_of_eq)
```
```   510
```
```   511
```
```   512 subsection \<open>Frontier with respect to topological space \<close>
```
```   513
```
```   514 definition frontier_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "frontier'_of" 80)
```
```   515   where "X frontier_of S \<equiv> X closure_of S - X interior_of S"
```
```   516
```
```   517 lemma frontier_of_closures:
```
```   518      "X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
```
```   519   by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)
```
```   520
```
```   521
```
```   522 lemma interior_of_union_frontier_of [simp]:
```
```   523      "X interior_of S \<union> X frontier_of S = X closure_of S"
```
```   524   by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)
```
```   525
```
```   526 lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X \<inter> S)"
```
```   527   by (metis closure_of_restrict frontier_of_def interior_of_restrict)
```
```   528
```
```   529 lemma closedin_frontier_of: "closedin X (X frontier_of S)"
```
```   530   by (simp add: closedin_Int frontier_of_closures)
```
```   531
```
```   532 lemma frontier_of_subset_topspace: "X frontier_of S \<subseteq> topspace X"
```
```   533   by (simp add: closedin_frontier_of closedin_subset)
```
```   534
```
```   535 lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T \<subseteq> S"
```
```   536   by (metis (no_types) closedin_derived_set closedin_frontier_of)
```
```   537
```
```   538 lemma frontier_of_subtopology_subset:
```
```   539   "U \<inter> (subtopology X U) frontier_of S \<subseteq> (X frontier_of S)"
```
```   540 proof -
```
```   541   have "U \<inter> X interior_of S - subtopology X U interior_of S = {}"
```
```   542     by (simp add: interior_of_subtopology_subset)
```
```   543   moreover have "X closure_of S \<inter> subtopology X U closure_of S = subtopology X U closure_of S"
```
```   544     by (meson closure_of_subtopology_subset inf.absorb_iff2)
```
```   545   ultimately show ?thesis
```
```   546     unfolding frontier_of_def
```
```   547     by blast
```
```   548 qed
```
```   549
```
```   550 lemma frontier_of_subtopology_mono:
```
```   551    "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X T) frontier_of S \<subseteq> (subtopology X U) frontier_of S"
```
```   552     by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono)
```
```   553
```
```   554 lemma clopenin_eq_frontier_of:
```
```   555    "closedin X S \<and> openin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> X frontier_of S = {}"
```
```   556 proof (cases "S \<subseteq> topspace X")
```
```   557   case True
```
```   558   then show ?thesis
```
```   559     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)
```
```   560 next
```
```   561   case False
```
```   562   then show ?thesis
```
```   563     by (simp add: frontier_of_closures openin_closedin_eq)
```
```   564 qed
```
```   565
```
```   566 lemma frontier_of_eq_empty:
```
```   567      "S \<subseteq> topspace X \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> closedin X S \<and> openin X S)"
```
```   568   by (simp add: clopenin_eq_frontier_of)
```
```   569
```
```   570 lemma frontier_of_openin:
```
```   571      "openin X S \<Longrightarrow> X frontier_of S = X closure_of S - S"
```
```   572   by (metis (no_types) frontier_of_def interior_of_eq)
```
```   573
```
```   574 lemma frontier_of_openin_straddle_Int:
```
```   575   assumes "openin X U" "U \<inter> X frontier_of S \<noteq> {}"
```
```   576   shows "U \<inter> S \<noteq> {}" "U - S \<noteq> {}"
```
```   577 proof -
```
```   578   have "U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}"
```
```   579     using assms by (simp add: frontier_of_closures)
```
```   580   then show "U \<inter> S \<noteq> {}"
```
```   581     using assms openin_Int_closure_of_eq_empty by fastforce
```
```   582   show "U - S \<noteq> {}"
```
```   583   proof -
```
```   584     have "\<exists>A. X closure_of (A - S) \<inter> U \<noteq> {}"
```
```   585       using \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> by blast
```
```   586     then have "\<not> U \<subseteq> S"
```
```   587       by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty)
```
```   588     then show ?thesis
```
```   589       by blast
```
```   590   qed
```
```   591 qed
```
```   592
```
```   593 lemma frontier_of_subset_closedin: "closedin X S \<Longrightarrow> (X frontier_of S) \<subseteq> S"
```
```   594   using closure_of_eq frontier_of_def by fastforce
```
```   595
```
```   596 lemma frontier_of_empty [simp]: "X frontier_of {} = {}"
```
```   597   by (simp add: frontier_of_def)
```
```   598
```
```   599 lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"
```
```   600   by (simp add: frontier_of_def)
```
```   601
```
```   602 lemma frontier_of_subset_eq:
```
```   603   assumes "S \<subseteq> topspace X"
```
```   604   shows "(X frontier_of S) \<subseteq> S \<longleftrightarrow> closedin X S"
```
```   605 proof
```
```   606   show "X frontier_of S \<subseteq> S \<Longrightarrow> closedin X S"
```
```   607     by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff)
```
```   608   show "closedin X S \<Longrightarrow> X frontier_of S \<subseteq> S"
```
```   609     by (simp add: frontier_of_subset_closedin)
```
```   610 qed
```
```   611
```
```   612 lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S"
```
```   613   by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute)
```
```   614
```
```   615 lemma frontier_of_disjoint_eq:
```
```   616   assumes "S \<subseteq> topspace X"
```
```   617   shows "((X frontier_of S) \<inter> S = {} \<longleftrightarrow> openin X S)"
```
```   618 proof
```
```   619   assume "X frontier_of S \<inter> S = {}"
```
```   620   then have "closedin X (topspace X - S)"
```
```   621     using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce
```
```   622   then show "openin X S"
```
```   623     using assms by (simp add: openin_closedin)
```
```   624 next
```
```   625   show "openin X S \<Longrightarrow> X frontier_of S \<inter> S = {}"
```
```   626     by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute)
```
```   627 qed
```
```   628
```
```   629 lemma frontier_of_disjoint_eq_alt:
```
```   630   "S \<subseteq> (topspace X - X frontier_of S) \<longleftrightarrow> openin X S"
```
```   631 proof (cases "S \<subseteq> topspace X")
```
```   632   case True
```
```   633   show ?thesis
```
```   634     using True frontier_of_disjoint_eq by auto
```
```   635 next
```
```   636   case False
```
```   637   then show ?thesis
```
```   638     by (meson Diff_subset openin_subset subset_trans)
```
```   639 qed
```
```   640
```
```   641 lemma frontier_of_Int:
```
```   642      "X frontier_of (S \<inter> T) =
```
```   643       X closure_of (S \<inter> T) \<inter> (X frontier_of S \<union> X frontier_of T)"
```
```   644 proof -
```
```   645   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"
```
```   646     by blast
```
```   647   show ?thesis
```
```   648     by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un)
```
```   649 qed
```
```   650
```
```   651 lemma frontier_of_Int_subset: "X frontier_of (S \<inter> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
```
```   652   by (simp add: frontier_of_Int)
```
```   653
```
```   654 lemma frontier_of_Int_closedin:
```
```   655   "\<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"
```
```   656   apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
```
```   657   using frontier_of_subset_closedin by blast
```
```   658
```
```   659 lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
```
```   660   by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)
```
```   661
```
```   662 lemma frontier_of_Union_subset:
```
```   663    "finite \<F> \<Longrightarrow> X frontier_of (\<Union>\<F>) \<subseteq> (\<Union>T \<in> \<F>. X frontier_of T)"
```
```   664 proof (induction \<F> rule: finite_induct)
```
```   665   case (insert A \<F>)
```
```   666   then show ?case
```
```   667     using frontier_of_Un_subset by fastforce
```
```   668 qed simp
```
```   669
```
```   670 lemma frontier_of_frontier_of_subset:
```
```   671      "X frontier_of (X frontier_of S) \<subseteq> X frontier_of S"
```
```   672   by (simp add: closedin_frontier_of frontier_of_subset_closedin)
```
```   673
```
```   674 lemma frontier_of_subtopology_open:
```
```   675      "openin X U \<Longrightarrow> (subtopology X U) frontier_of S = U \<inter> X frontier_of S"
```
```   676   by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open)
```
```   677
```
```   678 lemma discrete_topology_frontier_of [simp]:
```
```   679      "(discrete_topology U) frontier_of S = {}"
```
```   680   by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
```
```   681
```
```   682
```
```   683 subsection\<open>Continuous maps\<close>
```
```   684
```
```   685 definition continuous_map where
```
```   686   "continuous_map X Y f \<equiv>
```
```   687      (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
```
```   688      (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
```
```   689
```
```   690 lemma continuous_map:
```
```   691    "continuous_map X Y f \<longleftrightarrow>
```
```   692         f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
```
```   693   by (auto simp: continuous_map_def)
```
```   694
```
```   695 lemma continuous_map_image_subset_topspace:
```
```   696    "continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
```
```   697   by (auto simp: continuous_map_def)
```
```   698
```
```   699 lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
```
```   700   by (auto simp: continuous_map_def)
```
```   701
```
```   702 lemma continuous_map_closedin:
```
```   703    "continuous_map X Y f \<longleftrightarrow>
```
```   704          (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
```
```   705          (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
```
```   706 proof -
```
```   707   have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
```
```   708         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
```
```   709     if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
```
```   710   proof -
```
```   711     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
```
```   712       using that by blast
```
```   713     show ?thesis
```
```   714     proof (intro iffI allI impI)
```
```   715       fix C
```
```   716       assume "\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}" and "closedin Y C"
```
```   717       then have "openin X {x \<in> topspace X. f x \<in> topspace Y - C}" by blast
```
```   718       then show "closedin X {x \<in> topspace X. f x \<in> C}"
```
```   719         by (auto simp add: closedin_def eq)
```
```   720     next
```
```   721       fix U
```
```   722       assume "\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}" and "openin Y U"
```
```   723       then have "closedin X {x \<in> topspace X. f x \<in> topspace Y - U}" by blast
```
```   724       then show "openin X {x \<in> topspace X. f x \<in> U}"
```
```   725         by (auto simp add: openin_closedin_eq eq)
```
```   726     qed
```
```   727   qed
```
```   728   then show ?thesis
```
```   729     by (auto simp: continuous_map_def)
```
```   730 qed
```
```   731
```
```   732 lemma openin_continuous_map_preimage:
```
```   733    "\<lbrakk>continuous_map X Y f; openin Y U\<rbrakk> \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
```
```   734   by (simp add: continuous_map_def)
```
```   735
```
```   736 lemma closedin_continuous_map_preimage:
```
```   737    "\<lbrakk>continuous_map X Y f; closedin Y C\<rbrakk> \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}"
```
```   738   by (simp add: continuous_map_closedin)
```
```   739
```
```   740 lemma openin_continuous_map_preimage_gen:
```
```   741   assumes "continuous_map X Y f" "openin X U" "openin Y V"
```
```   742   shows "openin X {x \<in> U. f x \<in> V}"
```
```   743 proof -
```
```   744   have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
```
```   745     using assms(2) openin_closedin_eq by fastforce
```
```   746   show ?thesis
```
```   747     unfolding eq
```
```   748     using assms openin_continuous_map_preimage by fastforce
```
```   749 qed
```
```   750
```
```   751 lemma closedin_continuous_map_preimage_gen:
```
```   752   assumes "continuous_map X Y f" "closedin X U" "closedin Y V"
```
```   753   shows "closedin X {x \<in> U. f x \<in> V}"
```
```   754 proof -
```
```   755   have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
```
```   756     using assms(2) closedin_def by fastforce
```
```   757   show ?thesis
```
```   758     unfolding eq
```
```   759     using assms closedin_continuous_map_preimage by fastforce
```
```   760 qed
```
```   761
```
```   762 lemma continuous_map_image_closure_subset:
```
```   763   assumes "continuous_map X Y f"
```
```   764   shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
```
```   765 proof -
```
```   766   have *: "f ` (topspace X) \<subseteq> topspace Y"
```
```   767     by (meson assms continuous_map)
```
```   768   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
```
```   769   proof (rule closure_of_minimal)
```
```   770     show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
```
```   771       using closure_of_subset * that  by (fastforce simp: in_closure_of)
```
```   772   next
```
```   773     show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
```
```   774       using assms closedin_continuous_map_preimage_gen by fastforce
```
```   775   qed
```
```   776   then have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (f ` (topspace X \<inter> S))"
```
```   777     by blast
```
```   778   also have "\<dots> \<subseteq> Y closure_of (topspace Y \<inter> f ` S)"
```
```   779     using * by (blast intro!: closure_of_mono)
```
```   780   finally have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (topspace Y \<inter> f ` S)" .
```
```   781   then show ?thesis
```
```   782     by (metis closure_of_restrict)
```
```   783 qed
```
```   784
```
```   785 lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
```
```   786        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
```
```   787   using continuous_map_image_closure_subset by blast
```
```   788
```
```   789 lemma continuous_map_subset_aux2:
```
```   790   assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
```
```   791   shows "continuous_map X Y f"
```
```   792   unfolding continuous_map_closedin
```
```   793 proof (intro conjI ballI allI impI)
```
```   794   fix x
```
```   795   assume "x \<in> topspace X"
```
```   796   then show "f x \<in> topspace Y"
```
```   797     using assms closure_of_subset_topspace by fastforce
```
```   798 next
```
```   799   fix C
```
```   800   assume "closedin Y C"
```
```   801   then show "closedin X {x \<in> topspace X. f x \<in> C}"
```
```   802   proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
```
```   803     fix x
```
```   804     assume x: "x \<in> X closure_of {x \<in> topspace X. f x \<in> C}"
```
```   805       and "C \<subseteq> topspace Y" and "Y closure_of C \<subseteq> C"
```
```   806     show "x \<in> topspace X"
```
```   807       by (meson x in_closure_of)
```
```   808     have "{a \<in> topspace X. f a \<in> C} \<subseteq> topspace X"
```
```   809       by simp
```
```   810     moreover have "Y closure_of f ` {a \<in> topspace X. f a \<in> C} \<subseteq> C"
```
```   811       by (simp add: \<open>closedin Y C\<close> closure_of_minimal image_subset_iff)
```
```   812     ultimately have "f ` (X closure_of {a \<in> topspace X. f a \<in> C}) \<subseteq> C"
```
```   813       using assms by blast
```
```   814     then show "f x \<in> C"
```
```   815       using x by auto
```
```   816   qed
```
```   817 qed
```
```   818
```
```   819 lemma continuous_map_eq_image_closure_subset:
```
```   820      "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
```
```   821   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
```
```   822
```
```   823 lemma continuous_map_eq_image_closure_subset_alt:
```
```   824      "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
```
```   825   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
```
```   826
```
```   827 lemma continuous_map_eq_image_closure_subset_gen:
```
```   828      "continuous_map X Y f \<longleftrightarrow>
```
```   829         f ` (topspace X) \<subseteq> topspace Y \<and>
```
```   830         (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
```
```   831   using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
```
```   832
```
```   833 lemma continuous_map_closure_preimage_subset:
```
```   834    "continuous_map X Y f
```
```   835         \<Longrightarrow> X closure_of {x \<in> topspace X. f x \<in> T}
```
```   836             \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
```
```   837   unfolding continuous_map_closedin
```
```   838   by (rule closure_of_minimal) (use in_closure_of in \<open>fastforce+\<close>)
```
```   839
```
```   840
```
```   841 lemma continuous_map_frontier_frontier_preimage_subset:
```
```   842   assumes "continuous_map X Y f"
```
```   843   shows "X frontier_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y frontier_of T}"
```
```   844 proof -
```
```   845   have eq: "topspace X - {x \<in> topspace X. f x \<in> T} = {x \<in> topspace X. f x \<in> topspace Y - T}"
```
```   846     using assms unfolding continuous_map_def by blast
```
```   847   have "X closure_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
```
```   848     by (simp add: assms continuous_map_closure_preimage_subset)
```
```   849   moreover
```
```   850   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)}"
```
```   851     using continuous_map_closure_preimage_subset [OF assms] eq by presburger
```
```   852   ultimately show ?thesis
```
```   853     by (auto simp: frontier_of_closures)
```
```   854 qed
```
```   855
```
```   856 lemma continuous_map_id [simp]: "continuous_map X X id"
```
```   857   unfolding continuous_map_def  using openin_subopen topspace_def by fastforce
```
```   858
```
```   859 lemma topology_finer_continuous_id:
```
```   860   "topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
```
```   861   unfolding continuous_map_def
```
```   862   apply auto
```
```   863   using openin_subopen openin_subset apply fastforce
```
```   864   using openin_subopen topspace_def by fastforce
```
```   865
```
```   866 lemma continuous_map_const [simp]:
```
```   867    "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
```
```   868 proof (cases "topspace X = {}")
```
```   869   case False
```
```   870   show ?thesis
```
```   871   proof (cases "C \<in> topspace Y")
```
```   872     case True
```
```   873     with openin_subopen show ?thesis
```
```   874       by (auto simp: continuous_map_def)
```
```   875   next
```
```   876     case False
```
```   877     then show ?thesis
```
```   878       unfolding continuous_map_def by fastforce
```
```   879   qed
```
```   880 qed (auto simp: continuous_map_on_empty)
```
```   881
```
```   882 lemma continuous_map_compose:
```
```   883   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
```
```   884   shows "continuous_map X X'' (g \<circ> f)"
```
```   885   unfolding continuous_map_def
```
```   886 proof (intro conjI ballI allI impI)
```
```   887   fix x
```
```   888   assume "x \<in> topspace X"
```
```   889   then show "(g \<circ> f) x \<in> topspace X''"
```
```   890     using assms unfolding continuous_map_def by force
```
```   891 next
```
```   892   fix U
```
```   893   assume "openin X'' U"
```
```   894   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}}"
```
```   895     by auto (meson f continuous_map_def)
```
```   896   show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
```
```   897     unfolding eq
```
```   898     using assms unfolding continuous_map_def
```
```   899     using \<open>openin X'' U\<close> by blast
```
```   900 qed
```
```   901
```
```   902 lemma continuous_map_eq:
```
```   903   assumes "continuous_map X X' f" and "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x" shows "continuous_map X X' g"
```
```   904 proof -
```
```   905   have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
```
```   906     using assms by auto
```
```   907   show ?thesis
```
```   908     using assms by (simp add: continuous_map_def eq)
```
```   909 qed
```
```   910
```
```   911 lemma restrict_continuous_map [simp]:
```
```   912      "topspace X \<subseteq> S \<Longrightarrow> continuous_map X X' (restrict f S) \<longleftrightarrow> continuous_map X X' f"
```
```   913   by (auto simp: elim!: continuous_map_eq)
```
```   914
```
```   915 lemma continuous_map_in_subtopology:
```
```   916   "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
```
```   917   (is "?lhs = ?rhs")
```
```   918 proof
```
```   919   assume L: ?lhs
```
```   920   show ?rhs
```
```   921   proof -
```
```   922     have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
```
```   923       by (meson L continuous_map_image_closure_subset)
```
```   924     then show ?thesis
```
```   925       by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset dual_order.trans)
```
```   926   qed
```
```   927 next
```
```   928   assume R: ?rhs
```
```   929   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
```
```   930     by auto
```
```   931   show ?lhs
```
```   932     using R
```
```   933     unfolding continuous_map
```
```   934     by (auto simp: topspace_subtopology openin_subtopology eq)
```
```   935 qed
```
```   936
```
```   937
```
```   938 lemma continuous_map_from_subtopology:
```
```   939      "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
```
```   940   by (auto simp: continuous_map topspace_subtopology openin_subtopology)
```
```   941
```
```   942 lemma continuous_map_into_fulltopology:
```
```   943    "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
```
```   944   by (auto simp: continuous_map_in_subtopology)
```
```   945
```
```   946 lemma continuous_map_into_subtopology:
```
```   947    "\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
```
```   948   by (auto simp: continuous_map_in_subtopology)
```
```   949
```
```   950 lemma continuous_map_from_subtopology_mono:
```
```   951      "\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
```
```   952       \<Longrightarrow> continuous_map (subtopology X S) X' f"
```
```   953   by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)
```
```   954
```
```   955 lemma continuous_map_from_discrete_topology [simp]:
```
```   956   "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
```
```   957   by (auto simp: continuous_map_def)
```
```   958
```
```   959 lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g"
```
```   960   by (force simp: continuous_map openin_subtopology continuous_on_open_invariant)
```
```   961
```
```   962
```
```   963 subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
```
```   964
```
```   965 definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```   966   where "open_map X1 X2 f \<equiv> \<forall>U. openin X1 U \<longrightarrow> openin X2 (f ` U)"
```
```   967
```
```   968 definition closed_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```   969   where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"
```
```   970
```
```   971 lemma open_map_imp_subset_topspace:
```
```   972      "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
```
```   973   unfolding open_map_def by (simp add: openin_subset)
```
```   974
```
```   975 lemma open_map_imp_subset:
```
```   976     "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
```
```   977   by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
```
```   978
```
```   979 lemma topology_finer_open_id:
```
```   980      "(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
```
```   981   unfolding open_map_def by auto
```
```   982
```
```   983 lemma open_map_id: "open_map X X id"
```
```   984   unfolding open_map_def by auto
```
```   985
```
```   986 lemma open_map_eq:
```
```   987      "\<lbrakk>open_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> open_map X X' g"
```
```   988   unfolding open_map_def
```
```   989   by (metis image_cong openin_subset subset_iff)
```
```   990
```
```   991 lemma open_map_inclusion_eq:
```
```   992   "open_map (subtopology X S) X id \<longleftrightarrow> openin X (topspace X \<inter> S)"
```
```   993 proof -
```
```   994   have *: "openin X (T \<inter> S)" if "openin X (S \<inter> topspace X)" "openin X T" for T
```
```   995   proof -
```
```   996     have "T \<subseteq> topspace X"
```
```   997       using that by (simp add: openin_subset)
```
```   998     with that show "openin X (T \<inter> S)"
```
```   999       by (metis inf.absorb1 inf.left_commute inf_commute openin_Int)
```
```  1000   qed
```
```  1001   show ?thesis
```
```  1002     by (fastforce simp add: open_map_def Int_commute openin_subtopology_alt intro: *)
```
```  1003 qed
```
```  1004
```
```  1005 lemma open_map_inclusion:
```
```  1006      "openin X S \<Longrightarrow> open_map (subtopology X S) X id"
```
```  1007   by (simp add: open_map_inclusion_eq openin_Int)
```
```  1008
```
```  1009 lemma open_map_compose:
```
```  1010      "\<lbrakk>open_map X X' f; open_map X' X'' g\<rbrakk> \<Longrightarrow> open_map X X'' (g \<circ> f)"
```
```  1011   by (metis (no_types, lifting) image_comp open_map_def)
```
```  1012
```
```  1013 lemma closed_map_imp_subset_topspace:
```
```  1014      "closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
```
```  1015   by (simp add: closed_map_def closedin_subset)
```
```  1016
```
```  1017 lemma closed_map_imp_subset:
```
```  1018      "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
```
```  1019   using closed_map_imp_subset_topspace by blast
```
```  1020
```
```  1021 lemma topology_finer_closed_id:
```
```  1022     "(\<forall>S. closedin X S \<longrightarrow> closedin X' S) \<longleftrightarrow> closed_map X X' id"
```
```  1023   by (simp add: closed_map_def)
```
```  1024
```
```  1025 lemma closed_map_id: "closed_map X X id"
```
```  1026   by (simp add: closed_map_def)
```
```  1027
```
```  1028 lemma closed_map_eq:
```
```  1029    "\<lbrakk>closed_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> closed_map X X' g"
```
```  1030   unfolding closed_map_def
```
```  1031   by (metis image_cong closedin_subset subset_iff)
```
```  1032
```
```  1033 lemma closed_map_compose:
```
```  1034     "\<lbrakk>closed_map X X' f; closed_map X' X'' g\<rbrakk> \<Longrightarrow> closed_map X X'' (g \<circ> f)"
```
```  1035   by (metis (no_types, lifting) closed_map_def image_comp)
```
```  1036
```
```  1037 lemma closed_map_inclusion_eq:
```
```  1038    "closed_map (subtopology X S) X id \<longleftrightarrow>
```
```  1039         closedin X (topspace X \<inter> S)"
```
```  1040 proof -
```
```  1041   have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
```
```  1042   proof -
```
```  1043     have "T \<subseteq> topspace X"
```
```  1044       using that by (simp add: closedin_subset)
```
```  1045     with that show "closedin X (T \<inter> S)"
```
```  1046       by (metis inf.absorb1 inf.left_commute inf_commute closedin_Int)
```
```  1047   qed
```
```  1048   show ?thesis
```
```  1049     by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *)
```
```  1050 qed
```
```  1051
```
```  1052 lemma closed_map_inclusion: "closedin X S \<Longrightarrow> closed_map (subtopology X S) X id"
```
```  1053   by (simp add: closed_map_inclusion_eq closedin_Int)
```
```  1054
```
```  1055 lemma open_map_into_subtopology:
```
```  1056     "\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
```
```  1057   unfolding open_map_def openin_subtopology
```
```  1058   using openin_subset by fastforce
```
```  1059
```
```  1060 lemma closed_map_into_subtopology:
```
```  1061     "\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
```
```  1062   unfolding closed_map_def closedin_subtopology
```
```  1063   using closedin_subset by fastforce
```
```  1064
```
```  1065 lemma open_map_into_discrete_topology:
```
```  1066     "open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
```
```  1067   unfolding open_map_def openin_discrete_topology using openin_subset by blast
```
```  1068
```
```  1069 lemma closed_map_into_discrete_topology:
```
```  1070     "closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
```
```  1071   unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast
```
```  1072
```
```  1073 lemma bijective_open_imp_closed_map:
```
```  1074      "\<lbrakk>open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> closed_map X X' f"
```
```  1075   unfolding open_map_def closed_map_def closedin_def
```
```  1076   by auto (metis Diff_subset inj_on_image_set_diff)
```
```  1077
```
```  1078 lemma bijective_closed_imp_open_map:
```
```  1079      "\<lbrakk>closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> open_map X X' f"
```
```  1080   unfolding closed_map_def open_map_def openin_closedin_eq
```
```  1081   by auto (metis Diff_subset inj_on_image_set_diff)
```
```  1082
```
```  1083 lemma open_map_from_subtopology:
```
```  1084      "\<lbrakk>open_map X X' f; openin X U\<rbrakk> \<Longrightarrow> open_map (subtopology X U) X' f"
```
```  1085   unfolding open_map_def openin_subtopology_alt by blast
```
```  1086
```
```  1087 lemma closed_map_from_subtopology:
```
```  1088      "\<lbrakk>closed_map X X' f; closedin X U\<rbrakk> \<Longrightarrow> closed_map (subtopology X U) X' f"
```
```  1089   unfolding closed_map_def closedin_subtopology_alt by blast
```
```  1090
```
```  1091 lemma open_map_restriction:
```
```  1092      "\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
```
```  1093       \<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
```
```  1094   unfolding open_map_def openin_subtopology_alt
```
```  1095   apply clarify
```
```  1096   apply (rename_tac T)
```
```  1097   apply (rule_tac x="f ` T" in image_eqI)
```
```  1098   using openin_closedin_eq by force+
```
```  1099
```
```  1100 lemma closed_map_restriction:
```
```  1101      "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
```
```  1102       \<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
```
```  1103   unfolding closed_map_def closedin_subtopology_alt
```
```  1104   apply clarify
```
```  1105   apply (rename_tac T)
```
```  1106   apply (rule_tac x="f ` T" in image_eqI)
```
```  1107   using closedin_def by force+
```
```  1108
```
```  1109 subsection\<open>Quotient maps\<close>
```
```  1110
```
```  1111 definition quotient_map where
```
```  1112  "quotient_map X X' f \<longleftrightarrow>
```
```  1113         f ` (topspace X) = topspace X' \<and>
```
```  1114         (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (openin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> openin X' U))"
```
```  1115
```
```  1116 lemma quotient_map_eq:
```
```  1117   assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
```
```  1118   shows "quotient_map X X' g"
```
```  1119 proof -
```
```  1120   have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
```
```  1121     using assms by auto
```
```  1122   show ?thesis
```
```  1123   using assms
```
```  1124   unfolding quotient_map_def
```
```  1125   by (metis (mono_tags, lifting) eq image_cong)
```
```  1126 qed
```
```  1127
```
```  1128 lemma quotient_map_compose:
```
```  1129   assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
```
```  1130   shows "quotient_map X X'' (g \<circ> f)"
```
```  1131   unfolding quotient_map_def
```
```  1132 proof (intro conjI allI impI)
```
```  1133   show "(g \<circ> f) ` topspace X = topspace X''"
```
```  1134     using assms image_comp unfolding quotient_map_def by force
```
```  1135 next
```
```  1136   fix U''
```
```  1137   assume "U'' \<subseteq> topspace X''"
```
```  1138   define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}"
```
```  1139   have "U' \<subseteq> topspace X'"
```
```  1140     by (auto simp add: U'_def)
```
```  1141   then have U': "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
```
```  1142     using assms unfolding quotient_map_def by simp
```
```  1143   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''}"
```
```  1144     using f quotient_map_def by fastforce
```
```  1145   have "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X {x \<in> topspace X. f x \<in> U'}"
```
```  1146     using assms  by (simp add: quotient_map_def U'_def eq)
```
```  1147   also have "\<dots> = openin X'' U''"
```
```  1148     using U'_def \<open>U'' \<subseteq> topspace X''\<close> U' g quotient_map_def by fastforce
```
```  1149   finally show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X'' U''" .
```
```  1150 qed
```
```  1151
```
```  1152 lemma quotient_map_from_composition:
```
```  1153   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \<circ> f)"
```
```  1154   shows  "quotient_map X' X'' g"
```
```  1155   unfolding quotient_map_def
```
```  1156 proof (intro conjI allI impI)
```
```  1157   show "g ` topspace X' = topspace X''"
```
```  1158     using assms unfolding continuous_map_def quotient_map_def by fastforce
```
```  1159 next
```
```  1160   fix U'' :: "'c set"
```
```  1161   assume U'': "U'' \<subseteq> topspace X''"
```
```  1162   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''}}"
```
```  1163     using continuous_map_def f by fastforce
```
```  1164   show "openin X' {x \<in> topspace X'. g x \<in> U''} = openin X'' U''"
```
```  1165     using assms unfolding continuous_map_def quotient_map_def
```
```  1166     by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq)
```
```  1167 qed
```
```  1168
```
```  1169 lemma quotient_imp_continuous_map:
```
```  1170     "quotient_map X X' f \<Longrightarrow> continuous_map X X' f"
```
```  1171   by (simp add: continuous_map openin_subset quotient_map_def)
```
```  1172
```
```  1173 lemma quotient_imp_surjective_map:
```
```  1174     "quotient_map X X' f \<Longrightarrow> f ` (topspace X) = topspace X'"
```
```  1175   by (simp add: quotient_map_def)
```
```  1176
```
```  1177 lemma quotient_map_closedin:
```
```  1178   "quotient_map X X' f \<longleftrightarrow>
```
```  1179         f ` (topspace X) = topspace X' \<and>
```
```  1180         (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (closedin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> closedin X' U))"
```
```  1181 proof -
```
```  1182   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'}"
```
```  1183     if "f ` topspace X = topspace X'" "U' \<subseteq> topspace X'" for U'
```
```  1184       using that by auto
```
```  1185   have "(\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U) =
```
```  1186           (\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U)"
```
```  1187     if "f ` topspace X = topspace X'"
```
```  1188   proof (rule iffI; intro allI impI subsetI)
```
```  1189     fix U'
```
```  1190     assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
```
```  1191       and U': "U' \<subseteq> topspace X'"
```
```  1192     show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
```
```  1193       using U'  by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
```
```  1194   next
```
```  1195     fix U' :: "'b set"
```
```  1196     assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
```
```  1197       and U': "U' \<subseteq> topspace X'"
```
```  1198     show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
```
```  1199       using U'  by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
```
```  1200   qed
```
```  1201   then show ?thesis
```
```  1202     unfolding quotient_map_def by force
```
```  1203 qed
```
```  1204
```
```  1205 lemma continuous_open_imp_quotient_map:
```
```  1206   assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
```
```  1207   shows "quotient_map X X' f"
```
```  1208 proof -
```
```  1209   { fix U
```
```  1210     assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
```
```  1211     then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
```
```  1212       using om unfolding open_map_def by blast
```
```  1213     then have "openin X' U"
```
```  1214       using U feq by (subst openin_subopen) force
```
```  1215   }
```
```  1216   moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
```
```  1217     using that assms unfolding continuous_map_def by blast
```
```  1218   ultimately show ?thesis
```
```  1219     unfolding quotient_map_def using assms by blast
```
```  1220 qed
```
```  1221
```
```  1222 lemma continuous_closed_imp_quotient_map:
```
```  1223   assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'"
```
```  1224   shows "quotient_map X X' f"
```
```  1225 proof -
```
```  1226   have "f ` {x \<in> topspace X. f x \<in> U} = U" if "U \<subseteq> topspace X'" for U
```
```  1227     using that feq by auto
```
```  1228   with assms show ?thesis
```
```  1229     unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto
```
```  1230 qed
```
```  1231
```
```  1232 lemma continuous_open_quotient_map:
```
```  1233    "\<lbrakk>continuous_map X X' f; open_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
```
```  1234   by (meson continuous_open_imp_quotient_map quotient_map_def)
```
```  1235
```
```  1236 lemma continuous_closed_quotient_map:
```
```  1237      "\<lbrakk>continuous_map X X' f; closed_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
```
```  1238   by (meson continuous_closed_imp_quotient_map quotient_map_def)
```
```  1239
```
```  1240 lemma injective_quotient_map:
```
```  1241   assumes "inj_on f (topspace X)"
```
```  1242   shows "quotient_map X X' f \<longleftrightarrow>
```
```  1243          continuous_map X X' f \<and> open_map X X' f \<and> closed_map X X' f \<and> f ` (topspace X) = topspace X'"
```
```  1244          (is "?lhs = ?rhs")
```
```  1245 proof
```
```  1246   assume L: ?lhs
```
```  1247   have "open_map X X' f"
```
```  1248   proof (clarsimp simp add: open_map_def)
```
```  1249     fix U
```
```  1250     assume "openin X U"
```
```  1251     then have "U \<subseteq> topspace X"
```
```  1252       by (simp add: openin_subset)
```
```  1253     moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
```
```  1254       using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
```
```  1255     ultimately show "openin X' (f ` U)"
```
```  1256       using L unfolding quotient_map_def
```
```  1257       by (metis (no_types, lifting) Collect_cong \<open>openin X U\<close> image_mono)
```
```  1258   qed
```
```  1259   moreover have "closed_map X X' f"
```
```  1260   proof (clarsimp simp add: closed_map_def)
```
```  1261     fix U
```
```  1262     assume "closedin X U"
```
```  1263     then have "U \<subseteq> topspace X"
```
```  1264       by (simp add: closedin_subset)
```
```  1265     moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
```
```  1266       using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
```
```  1267     ultimately show "closedin X' (f ` U)"
```
```  1268       using L unfolding quotient_map_closedin
```
```  1269       by (metis (no_types, lifting) Collect_cong \<open>closedin X U\<close> image_mono)
```
```  1270   qed
```
```  1271   ultimately show ?rhs
```
```  1272     using L by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
```
```  1273 next
```
```  1274   assume ?rhs
```
```  1275   then show ?lhs
```
```  1276     by (simp add: continuous_closed_imp_quotient_map)
```
```  1277 qed
```
```  1278
```
```  1279 lemma continuous_compose_quotient_map:
```
```  1280   assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
```
```  1281   shows "continuous_map X' X'' g"
```
```  1282   unfolding quotient_map_def continuous_map_def
```
```  1283 proof (intro conjI ballI allI impI)
```
```  1284   show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
```
```  1285     using assms unfolding quotient_map_def
```
```  1286     by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
```
```  1287 next
```
```  1288   fix U'' :: "'c set"
```
```  1289   assume U'': "openin X'' U''"
```
```  1290   have "f ` topspace X = topspace X'"
```
```  1291     by (simp add: f quotient_imp_surjective_map)
```
```  1292   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
```
```  1293     by auto
```
```  1294   have "openin X {x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''}"
```
```  1295     unfolding eq using U'' g openin_continuous_map_preimage by fastforce
```
```  1296   then have *: "openin X {x \<in> topspace X. f x \<in> {x \<in> topspace X'. g x \<in> U''}}"
```
```  1297     by auto
```
```  1298   show "openin X' {x \<in> topspace X'. g x \<in> U''}"
```
```  1299     using f unfolding quotient_map_def
```
```  1300     by (metis (no_types) Collect_subset *)
```
```  1301 qed
```
```  1302
```
```  1303 lemma continuous_compose_quotient_map_eq:
```
```  1304    "quotient_map X X' f \<Longrightarrow> continuous_map X X'' (g \<circ> f) \<longleftrightarrow> continuous_map X' X'' g"
```
```  1305   using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast
```
```  1306
```
```  1307 lemma quotient_map_compose_eq:
```
```  1308    "quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
```
```  1309   apply safe
```
```  1310   apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
```
```  1311   by (simp add: quotient_map_compose)
```
```  1312
```
```  1313 lemma quotient_map_restriction:
```
```  1314   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"
```
```  1315  shows "quotient_map (subtopology X U) (subtopology Y V) f"
```
```  1316   using disj
```
```  1317 proof
```
```  1318   assume V: "openin Y V"
```
```  1319   with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
```
```  1320     by (auto simp: openin_subset)
```
```  1321   have fim: "f ` topspace X = topspace Y"
```
```  1322      and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
```
```  1323     using quo unfolding quotient_map_def by auto
```
```  1324   have "openin X U"
```
```  1325     using U V Y sub(2) by blast
```
```  1326   show ?thesis
```
```  1327     unfolding quotient_map_def
```
```  1328   proof (intro conjI allI impI)
```
```  1329     show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
```
```  1330       using sub U fim by (auto simp: topspace_subtopology)
```
```  1331   next
```
```  1332     fix Y' :: "'b set"
```
```  1333     assume "Y' \<subseteq> topspace (subtopology Y V)"
```
```  1334     then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
```
```  1335       by (simp_all add: topspace_subtopology)
```
```  1336     then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
```
```  1337       using U by blast
```
```  1338     then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
```
```  1339       using U V Y \<open>openin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
```
```  1340       by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
```
```  1341   qed
```
```  1342 next
```
```  1343   assume V: "closedin Y V"
```
```  1344   with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
```
```  1345     by (auto simp: closedin_subset)
```
```  1346   have fim: "f ` topspace X = topspace Y"
```
```  1347      and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U} = closedin Y U"
```
```  1348     using quo unfolding quotient_map_closedin by auto
```
```  1349   have "closedin X U"
```
```  1350     using U V Y sub(2) by blast
```
```  1351   show ?thesis
```
```  1352     unfolding quotient_map_closedin
```
```  1353   proof (intro conjI allI impI)
```
```  1354     show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
```
```  1355       using sub U fim by (auto simp: topspace_subtopology)
```
```  1356   next
```
```  1357     fix Y' :: "'b set"
```
```  1358     assume "Y' \<subseteq> topspace (subtopology Y V)"
```
```  1359     then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
```
```  1360       by (simp_all add: topspace_subtopology)
```
```  1361     then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
```
```  1362       using U by blast
```
```  1363     then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
```
```  1364       using U V Y \<open>closedin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
```
```  1365       by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
```
```  1366   qed
```
```  1367 qed
```
```  1368
```
```  1369 lemma quotient_map_saturated_open:
```
```  1370      "quotient_map X Y f \<longleftrightarrow>
```
```  1371         continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
```
```  1372         (\<forall>U. openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> openin Y (f ` U))"
```
```  1373      (is "?lhs = ?rhs")
```
```  1374 proof
```
```  1375   assume L: ?lhs
```
```  1376   then have fim: "f ` topspace X = topspace Y"
```
```  1377     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin Y U = openin X {x \<in> topspace X. f x \<in> U}"
```
```  1378     unfolding quotient_map_def by auto
```
```  1379   show ?rhs
```
```  1380   proof (intro conjI allI impI)
```
```  1381     show "continuous_map X Y f"
```
```  1382       by (simp add: L quotient_imp_continuous_map)
```
```  1383     show "f ` topspace X = topspace Y"
```
```  1384       by (simp add: fim)
```
```  1385   next
```
```  1386     fix U :: "'a set"
```
```  1387     assume U: "openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
```
```  1388     then have sub:  "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
```
```  1389       using fim openin_subset by fastforce+
```
```  1390     show "openin Y (f ` U)"
```
```  1391       by (simp add: sub Y eq U)
```
```  1392   qed
```
```  1393 next
```
```  1394   assume ?rhs
```
```  1395   then have YX: "\<And>U. openin Y U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
```
```  1396        and fim: "f ` topspace X = topspace Y"
```
```  1397        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)"
```
```  1398     by (auto simp: quotient_map_def continuous_map_def)
```
```  1399   show ?lhs
```
```  1400   proof (simp add: quotient_map_def fim, intro allI impI iffI)
```
```  1401     fix U :: "'b set"
```
```  1402     assume "U \<subseteq> topspace Y" and X: "openin X {x \<in> topspace X. f x \<in> U}"
```
```  1403     have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
```
```  1404       using \<open>U \<subseteq> topspace Y\<close> fim by auto
```
```  1405     show "openin Y U"
```
```  1406       using XY [OF X] by (simp add: feq)
```
```  1407   next
```
```  1408     fix U :: "'b set"
```
```  1409     assume "U \<subseteq> topspace Y" and Y: "openin Y U"
```
```  1410     show "openin X {x \<in> topspace X. f x \<in> U}"
```
```  1411       by (metis YX [OF Y])
```
```  1412   qed
```
```  1413 qed
```
```  1414
```
```  1415 subsection\<open> Separated Sets\<close>
```
```  1416
```
```  1417 definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
```
```  1418   where "separatedin X S T \<equiv>
```
```  1419            S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
```
```  1420            S \<inter> X closure_of T = {} \<and> T \<inter> X closure_of S = {}"
```
```  1421
```
```  1422 lemma separatedin_empty [simp]:
```
```  1423      "separatedin X S {} \<longleftrightarrow> S \<subseteq> topspace X"
```
```  1424      "separatedin X {} S \<longleftrightarrow> S \<subseteq> topspace X"
```
```  1425   by (simp_all add: separatedin_def)
```
```  1426
```
```  1427 lemma separatedin_refl [simp]:
```
```  1428      "separatedin X S S \<longleftrightarrow> S = {}"
```
```  1429 proof -
```
```  1430   have "\<And>x. \<lbrakk>separatedin X S S; x \<in> S\<rbrakk> \<Longrightarrow> False"
```
```  1431     by (metis all_not_in_conv closure_of_subset inf.orderE separatedin_def)
```
```  1432   then show ?thesis
```
```  1433     by auto
```
```  1434 qed
```
```  1435
```
```  1436 lemma separatedin_sym:
```
```  1437      "separatedin X S T \<longleftrightarrow> separatedin X T S"
```
```  1438   by (auto simp: separatedin_def)
```
```  1439
```
```  1440 lemma separatedin_imp_disjoint:
```
```  1441      "separatedin X S T \<Longrightarrow> disjnt S T"
```
```  1442   by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def)
```
```  1443
```
```  1444 lemma separatedin_mono:
```
```  1445    "\<lbrakk>separatedin X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separatedin X S' T'"
```
```  1446   unfolding separatedin_def
```
```  1447   using closure_of_mono by blast
```
```  1448
```
```  1449 lemma separatedin_open_sets:
```
```  1450      "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
```
```  1451   unfolding disjnt_def separatedin_def
```
```  1452   by (auto simp: openin_Int_closure_of_eq_empty openin_subset)
```
```  1453
```
```  1454 lemma separatedin_closed_sets:
```
```  1455      "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
```
```  1456   by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)
```
```  1457
```
```  1458 lemma separatedin_subtopology:
```
```  1459      "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
```
```  1460   apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
```
```  1461   apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
```
```  1462   done
```
```  1463
```
```  1464 lemma separatedin_discrete_topology:
```
```  1465      "separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
```
```  1466   by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology)
```
```  1467
```
```  1468 lemma separated_eq_distinguishable:
```
```  1469    "separatedin X {x} {y} \<longleftrightarrow>
```
```  1470         x \<in> topspace X \<and> y \<in> topspace X \<and>
```
```  1471         (\<exists>U. openin X U \<and> x \<in> U \<and> (y \<notin> U)) \<and>
```
```  1472         (\<exists>v. openin X v \<and> y \<in> v \<and> (x \<notin> v))"
```
```  1473   by (force simp: separatedin_def closure_of_def)
```
```  1474
```
```  1475 lemma separatedin_Un [simp]:
```
```  1476    "separatedin X S (T \<union> U) \<longleftrightarrow> separatedin X S T \<and> separatedin X S U"
```
```  1477    "separatedin X (S \<union> T) U \<longleftrightarrow> separatedin X S U \<and> separatedin X T U"
```
```  1478   by (auto simp: separatedin_def)
```
```  1479
```
```  1480 lemma separatedin_Union:
```
```  1481   "finite \<F> \<Longrightarrow> separatedin X S (\<Union>\<F>) \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<forall>T \<in> \<F>. separatedin X S T)"
```
```  1482   "finite \<F> \<Longrightarrow> separatedin X (\<Union>\<F>) S \<longleftrightarrow> (\<forall>T \<in> \<F>. separatedin X S T) \<and> S \<subseteq> topspace X"
```
```  1483   by (auto simp: separatedin_def closure_of_Union)
```
```  1484
```
```  1485 lemma separatedin_openin_diff:
```
```  1486    "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
```
```  1487   unfolding separatedin_def
```
```  1488   apply (intro conjI)
```
```  1489   apply (meson Diff_subset openin_subset subset_trans)+
```
```  1490   using openin_Int_closure_of_eq_empty by fastforce+
```
```  1491
```
```  1492 lemma separatedin_closedin_diff:
```
```  1493      "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
```
```  1494   apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
```
```  1495   apply (meson Diff_subset closedin_subset subset_trans)
```
```  1496   done
```
```  1497
```
```  1498 lemma separation_closedin_Un_gen:
```
```  1499      "separatedin X S T \<longleftrightarrow>
```
```  1500         S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
```
```  1501         closedin (subtopology X (S \<union> T)) S \<and>
```
```  1502         closedin (subtopology X (S \<union> T)) T"
```
```  1503   apply (simp add: separatedin_def closedin_Int_closure_of disjnt_iff)
```
```  1504   using closure_of_subset apply blast
```
```  1505   done
```
```  1506
```
```  1507 lemma separation_openin_Un_gen:
```
```  1508      "separatedin X S T \<longleftrightarrow>
```
```  1509         S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
```
```  1510         openin (subtopology X (S \<union> T)) S \<and>
```
```  1511         openin (subtopology X (S \<union> T)) T"
```
```  1512   unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
```
```  1513   by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)
```
```  1514
```
```  1515
```
```  1516 subsection\<open>Homeomorphisms\<close>
```
```  1517 text\<open>(1-way and 2-way versions may be useful in places)\<close>
```
```  1518
```
```  1519 definition homeomorphic_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```  1520   where
```
```  1521  "homeomorphic_map X Y f \<equiv> quotient_map X Y f \<and> inj_on f (topspace X)"
```
```  1522
```
```  1523 definition homeomorphic_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
```
```  1524   where
```
```  1525  "homeomorphic_maps X Y f g \<equiv>
```
```  1526     continuous_map X Y f \<and> continuous_map Y X g \<and>
```
```  1527      (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
```
```  1528
```
```  1529
```
```  1530 lemma homeomorphic_map_eq:
```
```  1531    "\<lbrakk>homeomorphic_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> homeomorphic_map X Y g"
```
```  1532   by (meson homeomorphic_map_def inj_on_cong quotient_map_eq)
```
```  1533
```
```  1534 lemma homeomorphic_maps_eq:
```
```  1535      "\<lbrakk>homeomorphic_maps X Y f g;
```
```  1536        \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
```
```  1537       \<Longrightarrow> homeomorphic_maps X Y f' g'"
```
```  1538   apply (simp add: homeomorphic_maps_def)
```
```  1539   by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
```
```  1540
```
```  1541 lemma homeomorphic_maps_sym:
```
```  1542      "homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
```
```  1543   by (auto simp: homeomorphic_maps_def)
```
```  1544
```
```  1545 lemma homeomorphic_maps_id:
```
```  1546      "homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
```
```  1547   (is "?lhs = ?rhs")
```
```  1548 proof
```
```  1549   assume L: ?lhs
```
```  1550   then have "topspace X = topspace Y"
```
```  1551     by (auto simp: homeomorphic_maps_def continuous_map_def)
```
```  1552   with L show ?rhs
```
```  1553     unfolding homeomorphic_maps_def
```
```  1554     by (metis topology_finer_continuous_id topology_eq)
```
```  1555 next
```
```  1556   assume ?rhs
```
```  1557   then show ?lhs
```
```  1558     unfolding homeomorphic_maps_def by auto
```
```  1559 qed
```
```  1560
```
```  1561 lemma homeomorphic_map_id [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
```
```  1562        (is "?lhs = ?rhs")
```
```  1563 proof
```
```  1564   assume L: ?lhs
```
```  1565   then have eq: "topspace X = topspace Y"
```
```  1566     by (auto simp: homeomorphic_map_def continuous_map_def quotient_map_def)
```
```  1567   then have "\<And>S. openin X S \<longrightarrow> openin Y S"
```
```  1568     by (meson L homeomorphic_map_def injective_quotient_map topology_finer_open_id)
```
```  1569   then show ?rhs
```
```  1570     using L unfolding homeomorphic_map_def
```
```  1571     by (metis eq quotient_imp_continuous_map topology_eq topology_finer_continuous_id)
```
```  1572 next
```
```  1573   assume ?rhs
```
```  1574   then show ?lhs
```
```  1575     unfolding homeomorphic_map_def
```
```  1576     by (simp add: closed_map_id continuous_closed_imp_quotient_map)
```
```  1577 qed
```
```  1578
```
```  1579 lemma homeomorphic_maps_i [simp]:"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
```
```  1580   by (metis (full_types) eq_id_iff homeomorphic_maps_id)
```
```  1581
```
```  1582 lemma homeomorphic_map_i [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
```
```  1583   by (metis (no_types) eq_id_iff homeomorphic_map_id)
```
```  1584
```
```  1585 lemma homeomorphic_map_compose:
```
```  1586   assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g"
```
```  1587   shows "homeomorphic_map X X'' (g \<circ> f)"
```
```  1588 proof -
```
```  1589   have "inj_on g (f ` topspace X)"
```
```  1590     by (metis (no_types) assms homeomorphic_map_def quotient_imp_surjective_map)
```
```  1591   then show ?thesis
```
```  1592     using assms by (meson comp_inj_on homeomorphic_map_def quotient_map_compose_eq)
```
```  1593 qed
```
```  1594
```
```  1595 lemma homeomorphic_maps_compose:
```
```  1596    "homeomorphic_maps X Y f h \<and>
```
```  1597         homeomorphic_maps Y X'' g k
```
```  1598         \<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
```
```  1599   unfolding homeomorphic_maps_def
```
```  1600   by (auto simp: continuous_map_compose; simp add: continuous_map_def)
```
```  1601
```
```  1602 lemma homeomorphic_eq_everything_map:
```
```  1603    "homeomorphic_map X Y f \<longleftrightarrow>
```
```  1604         continuous_map X Y f \<and> open_map X Y f \<and> closed_map X Y f \<and>
```
```  1605         f ` (topspace X) = topspace Y \<and> inj_on f (topspace X)"
```
```  1606   unfolding homeomorphic_map_def
```
```  1607   by (force simp: injective_quotient_map intro: injective_quotient_map)
```
```  1608
```
```  1609 lemma homeomorphic_imp_continuous_map:
```
```  1610      "homeomorphic_map X Y f \<Longrightarrow> continuous_map X Y f"
```
```  1611   by (simp add: homeomorphic_eq_everything_map)
```
```  1612
```
```  1613 lemma homeomorphic_imp_open_map:
```
```  1614    "homeomorphic_map X Y f \<Longrightarrow> open_map X Y f"
```
```  1615   by (simp add: homeomorphic_eq_everything_map)
```
```  1616
```
```  1617 lemma homeomorphic_imp_closed_map:
```
```  1618    "homeomorphic_map X Y f \<Longrightarrow> closed_map X Y f"
```
```  1619   by (simp add: homeomorphic_eq_everything_map)
```
```  1620
```
```  1621 lemma homeomorphic_imp_surjective_map:
```
```  1622    "homeomorphic_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
```
```  1623   by (simp add: homeomorphic_eq_everything_map)
```
```  1624
```
```  1625 lemma homeomorphic_imp_injective_map:
```
```  1626     "homeomorphic_map X Y f \<Longrightarrow> inj_on f (topspace X)"
```
```  1627   by (simp add: homeomorphic_eq_everything_map)
```
```  1628
```
```  1629 lemma bijective_open_imp_homeomorphic_map:
```
```  1630    "\<lbrakk>continuous_map X Y f; open_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
```
```  1631         \<Longrightarrow> homeomorphic_map X Y f"
```
```  1632   by (simp add: homeomorphic_map_def continuous_open_imp_quotient_map)
```
```  1633
```
```  1634 lemma bijective_closed_imp_homeomorphic_map:
```
```  1635    "\<lbrakk>continuous_map X Y f; closed_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
```
```  1636         \<Longrightarrow> homeomorphic_map X Y f"
```
```  1637   by (simp add: continuous_closed_quotient_map homeomorphic_map_def)
```
```  1638
```
```  1639 lemma open_eq_continuous_inverse_map:
```
```  1640   assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
```
```  1641     and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
```
```  1642   shows "open_map X Y f \<longleftrightarrow> continuous_map Y X g"
```
```  1643 proof -
```
```  1644   have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "openin X U" for U
```
```  1645     using openin_subset [OF that] by (force simp: X Y image_iff)
```
```  1646   show ?thesis
```
```  1647     by (auto simp: Y open_map_def continuous_map_def eq)
```
```  1648 qed
```
```  1649
```
```  1650 lemma closed_eq_continuous_inverse_map:
```
```  1651   assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
```
```  1652     and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
```
```  1653   shows "closed_map X Y f \<longleftrightarrow> continuous_map Y X g"
```
```  1654 proof -
```
```  1655   have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "closedin X U" for U
```
```  1656     using closedin_subset [OF that] by (force simp: X Y image_iff)
```
```  1657   show ?thesis
```
```  1658     by (auto simp: Y closed_map_def continuous_map_closedin eq)
```
```  1659 qed
```
```  1660
```
```  1661 lemma homeomorphic_maps_map:
```
```  1662   "homeomorphic_maps X Y f g \<longleftrightarrow>
```
```  1663         homeomorphic_map X Y f \<and> homeomorphic_map Y X g \<and>
```
```  1664         (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
```
```  1665   (is "?lhs = ?rhs")
```
```  1666 proof
```
```  1667   assume ?lhs
```
```  1668   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'"
```
```  1669     by (auto simp: homeomorphic_maps_def)
```
```  1670   show ?rhs
```
```  1671   proof (intro conjI bijective_open_imp_homeomorphic_map L)
```
```  1672     show "open_map X Y f"
```
```  1673       using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
```
```  1674     show "open_map Y X g"
```
```  1675       using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
```
```  1676     show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
```
```  1677       using L by (force simp: continuous_map_closedin)+
```
```  1678     show "inj_on f (topspace X)" "inj_on g (topspace Y)"
```
```  1679       using L unfolding inj_on_def by metis+
```
```  1680   qed
```
```  1681 next
```
```  1682   assume ?rhs
```
```  1683   then show ?lhs
```
```  1684     by (auto simp: homeomorphic_maps_def homeomorphic_imp_continuous_map)
```
```  1685 qed
```
```  1686
```
```  1687 lemma homeomorphic_maps_imp_map:
```
```  1688     "homeomorphic_maps X Y f g \<Longrightarrow> homeomorphic_map X Y f"
```
```  1689   using homeomorphic_maps_map by blast
```
```  1690
```
```  1691 lemma homeomorphic_map_maps:
```
```  1692      "homeomorphic_map X Y f \<longleftrightarrow> (\<exists>g. homeomorphic_maps X Y f g)"
```
```  1693   (is "?lhs = ?rhs")
```
```  1694 proof
```
```  1695   assume ?lhs
```
```  1696   then have L: "continuous_map X Y f" "open_map X Y f" "closed_map X Y f"
```
```  1697     "f ` (topspace X) = topspace Y" "inj_on f (topspace X)"
```
```  1698     by (auto simp: homeomorphic_eq_everything_map)
```
```  1699   have X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> inv_into (topspace X) f (f x) = x"
```
```  1700     using L by auto
```
```  1701   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"
```
```  1702     by (simp add: L f_inv_into_f inv_into_into)
```
```  1703   have "homeomorphic_maps X Y f (inv_into (topspace X) f)"
```
```  1704     unfolding homeomorphic_maps_def
```
```  1705   proof (intro conjI L)
```
```  1706     show "continuous_map Y X (inv_into (topspace X) f)"
```
```  1707       by (simp add: L X Y flip: open_eq_continuous_inverse_map [where f=f])
```
```  1708   next
```
```  1709     show "\<forall>x\<in>topspace X. inv_into (topspace X) f (f x) = x"
```
```  1710          "\<forall>y\<in>topspace Y. f (inv_into (topspace X) f y) = y"
```
```  1711       using X Y by auto
```
```  1712   qed
```
```  1713   then show ?rhs
```
```  1714     by metis
```
```  1715 next
```
```  1716   assume ?rhs
```
```  1717   then show ?lhs
```
```  1718     using homeomorphic_maps_map by blast
```
```  1719 qed
```
```  1720
```
```  1721 lemma homeomorphic_maps_involution:
```
```  1722    "\<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"
```
```  1723   by (auto simp: homeomorphic_maps_def)
```
```  1724
```
```  1725 lemma homeomorphic_map_involution:
```
```  1726    "\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_map X X f"
```
```  1727   using homeomorphic_maps_involution homeomorphic_maps_map by blast
```
```  1728
```
```  1729 lemma homeomorphic_map_openness:
```
```  1730   assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
```
```  1731   shows "openin Y (f ` U) \<longleftrightarrow> openin X U"
```
```  1732 proof -
```
```  1733   obtain g where "homeomorphic_maps X Y f g"
```
```  1734     using assms by (auto simp: homeomorphic_map_maps)
```
```  1735   then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
```
```  1736     by (auto simp: homeomorphic_maps_map)
```
```  1737   then have "openin X U \<Longrightarrow> openin Y (f ` U)"
```
```  1738     using hom homeomorphic_imp_open_map open_map_def by blast
```
```  1739   show "openin Y (f ` U) = openin X U"
```
```  1740   proof
```
```  1741     assume L: "openin Y (f ` U)"
```
```  1742     have "U = g ` (f ` U)"
```
```  1743       using U gf by force
```
```  1744     then show "openin X U"
```
```  1745       by (metis L homeomorphic_imp_open_map open_map_def g)
```
```  1746   next
```
```  1747     assume "openin X U"
```
```  1748     then show "openin Y (f ` U)"
```
```  1749       using hom homeomorphic_imp_open_map open_map_def by blast
```
```  1750   qed
```
```  1751 qed
```
```  1752
```
```  1753
```
```  1754 lemma homeomorphic_map_closedness:
```
```  1755   assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
```
```  1756   shows "closedin Y (f ` U) \<longleftrightarrow> closedin X U"
```
```  1757 proof -
```
```  1758   obtain g where "homeomorphic_maps X Y f g"
```
```  1759     using assms by (auto simp: homeomorphic_map_maps)
```
```  1760   then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
```
```  1761     by (auto simp: homeomorphic_maps_map)
```
```  1762   then have "closedin X U \<Longrightarrow> closedin Y (f ` U)"
```
```  1763     using hom homeomorphic_imp_closed_map closed_map_def by blast
```
```  1764   show "closedin Y (f ` U) = closedin X U"
```
```  1765   proof
```
```  1766     assume L: "closedin Y (f ` U)"
```
```  1767     have "U = g ` (f ` U)"
```
```  1768       using U gf by force
```
```  1769     then show "closedin X U"
```
```  1770       by (metis L homeomorphic_imp_closed_map closed_map_def g)
```
```  1771   next
```
```  1772     assume "closedin X U"
```
```  1773     then show "closedin Y (f ` U)"
```
```  1774       using hom homeomorphic_imp_closed_map closed_map_def by blast
```
```  1775   qed
```
```  1776 qed
```
```  1777
```
```  1778 lemma homeomorphic_map_openness_eq:
```
```  1779      "homeomorphic_map X Y f \<Longrightarrow> openin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> openin Y (f ` U)"
```
```  1780   by (meson homeomorphic_map_openness openin_closedin_eq)
```
```  1781
```
```  1782 lemma homeomorphic_map_closedness_eq:
```
```  1783     "homeomorphic_map X Y f \<Longrightarrow> closedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> closedin Y (f ` U)"
```
```  1784   by (meson closedin_subset homeomorphic_map_closedness)
```
```  1785
```
```  1786 lemma all_openin_homeomorphic_image:
```
```  1787   assumes "homeomorphic_map X Y f"
```
```  1788   shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
```
```  1789 proof
```
```  1790   assume ?lhs
```
```  1791   then show ?rhs
```
```  1792     by (meson assms homeomorphic_map_openness_eq)
```
```  1793 next
```
```  1794   assume ?rhs
```
```  1795   then show ?lhs
```
```  1796     by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff)
```
```  1797 qed
```
```  1798
```
```  1799 lemma all_closedin_homeomorphic_image:
```
```  1800   assumes "homeomorphic_map X Y f"
```
```  1801   shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
```
```  1802 proof
```
```  1803   assume ?lhs
```
```  1804   then show ?rhs
```
```  1805     by (meson assms homeomorphic_map_closedness_eq)
```
```  1806 next
```
```  1807   assume ?rhs
```
```  1808   then show ?lhs
```
```  1809     by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff)
```
```  1810 qed
```
```  1811
```
```  1812
```
```  1813 lemma homeomorphic_map_derived_set_of:
```
```  1814   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
```
```  1815   shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
```
```  1816 proof -
```
```  1817   have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
```
```  1818     using hom by (auto simp: homeomorphic_eq_everything_map)
```
```  1819   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)) =
```
```  1820             (\<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))"
```
```  1821     if "x \<in> topspace X" for x
```
```  1822   proof -
```
```  1823     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
```
```  1824       by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
```
```  1825     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")
```
```  1826       if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
```
```  1827     proof
```
```  1828       show "?lhs \<Longrightarrow> ?rhs"
```
```  1829         by (meson "1" imageI inj inj_on_eq_iff inj_on_subset that)
```
```  1830       show "?rhs \<Longrightarrow> ?lhs"
```
```  1831         using S inj inj_onD that by fastforce
```
```  1832     qed
```
```  1833     show ?thesis
```
```  1834       apply (simp flip: fim add: all_subset_image)
```
```  1835       apply (simp flip: imp_conjL)
```
```  1836       by (intro all_cong1 imp_cong 1 2)
```
```  1837   qed
```
```  1838   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
```
```  1839     by auto
```
```  1840   show ?thesis
```
```  1841     unfolding derived_set_of_def
```
```  1842     apply (rule *)
```
```  1843     using fim apply blast
```
```  1844     using iff openin_subset by force
```
```  1845 qed
```
```  1846
```
```  1847
```
```  1848 lemma homeomorphic_map_closure_of:
```
```  1849   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
```
```  1850   shows "Y closure_of (f ` S) = f ` (X closure_of S)"
```
```  1851   unfolding closure_of
```
```  1852   using homeomorphic_imp_surjective_map [OF hom] S
```
```  1853   by (auto simp: in_derived_set_of homeomorphic_map_derived_set_of [OF assms])
```
```  1854
```
```  1855 lemma homeomorphic_map_interior_of:
```
```  1856   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
```
```  1857   shows "Y interior_of (f ` S) = f ` (X interior_of S)"
```
```  1858 proof -
```
```  1859   { fix y
```
```  1860     assume "y \<in> topspace Y" and "y \<notin> Y closure_of (topspace Y - f ` S)"
```
```  1861     then have "y \<in> f ` (topspace X - X closure_of (topspace X - S))"
```
```  1862       using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom]
```
```  1863       by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) }
```
```  1864   moreover
```
```  1865   { fix x
```
```  1866     assume "x \<in> topspace X"
```
```  1867     then have "f x \<in> topspace Y"
```
```  1868       using hom homeomorphic_imp_surjective_map by blast }
```
```  1869   moreover
```
```  1870   { fix x
```
```  1871     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)"
```
```  1872     then have "False"
```
```  1873       using homeomorphic_map_closure_of [OF hom] hom
```
```  1874       unfolding homeomorphic_eq_everything_map
```
```  1875       by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
```
```  1876   ultimately  show ?thesis
```
```  1877     by (auto simp: interior_of_closure_of)
```
```  1878 qed
```
```  1879
```
```  1880 lemma homeomorphic_map_frontier_of:
```
```  1881   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
```
```  1882   shows "Y frontier_of (f ` S) = f ` (X frontier_of S)"
```
```  1883   unfolding frontier_of_def
```
```  1884 proof (intro equalityI subsetI DiffI)
```
```  1885   fix y
```
```  1886   assume "y \<in> Y closure_of f ` S - Y interior_of f ` S"
```
```  1887   then show "y \<in> f ` (X closure_of S - X interior_of S)"
```
```  1888     using S hom homeomorphic_map_closure_of homeomorphic_map_interior_of by fastforce
```
```  1889 next
```
```  1890   fix y
```
```  1891   assume "y \<in> f ` (X closure_of S - X interior_of S)"
```
```  1892   then show "y \<in> Y closure_of f ` S"
```
```  1893     using S hom homeomorphic_map_closure_of by fastforce
```
```  1894 next
```
```  1895   fix x
```
```  1896   assume "x \<in> f ` (X closure_of S - X interior_of S)"
```
```  1897   then obtain y where y: "x = f y" "y \<in> X closure_of S" "y \<notin> X interior_of S"
```
```  1898     by blast
```
```  1899   then have "y \<in> topspace X"
```
```  1900     by (simp add: in_closure_of)
```
```  1901   then have "f y \<notin> f ` (X interior_of S)"
```
```  1902     by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
```
```  1903   then show "x \<notin> Y interior_of f ` S"
```
```  1904     using S hom homeomorphic_map_interior_of y(1) by blast
```
```  1905 qed
```
```  1906
```
```  1907 lemma homeomorphic_maps_subtopologies:
```
```  1908    "\<lbrakk>homeomorphic_maps X Y f g;  f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
```
```  1909         \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
```
```  1910   unfolding homeomorphic_maps_def
```
```  1911   by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
```
```  1912
```
```  1913 lemma homeomorphic_maps_subtopologies_alt:
```
```  1914      "\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
```
```  1915       \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
```
```  1916   unfolding homeomorphic_maps_def
```
```  1917   by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
```
```  1918
```
```  1919 lemma homeomorphic_map_subtopologies:
```
```  1920    "\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
```
```  1921         \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
```
```  1922   by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies)
```
```  1923
```
```  1924 lemma homeomorphic_map_subtopologies_alt:
```
```  1925    "\<lbrakk>homeomorphic_map X Y f;
```
```  1926      \<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S\<rbrakk>
```
```  1927     \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
```
```  1928   unfolding homeomorphic_map_maps
```
```  1929   apply (erule ex_forward)
```
```  1930   apply (rule homeomorphic_maps_subtopologies)
```
```  1931   apply (auto simp: homeomorphic_maps_def continuous_map_def)
```
```  1932   by (metis IntI image_iff)
```
```  1933
```
```  1934
```
```  1935 subsection\<open>Relation of homeomorphism between topological spaces\<close>
```
```  1936
```
```  1937 definition homeomorphic_space (infixr "homeomorphic'_space" 50)
```
```  1938   where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
```
```  1939
```
```  1940 lemma homeomorphic_space_refl: "X homeomorphic_space X"
```
```  1941   by (meson homeomorphic_maps_id homeomorphic_space_def)
```
```  1942
```
```  1943 lemma homeomorphic_space_sym:
```
```  1944    "X homeomorphic_space Y \<longleftrightarrow> Y homeomorphic_space X"
```
```  1945   unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym)
```
```  1946
```
```  1947 lemma homeomorphic_space_trans:
```
```  1948      "\<lbrakk>X1 homeomorphic_space X2; X2 homeomorphic_space X3\<rbrakk> \<Longrightarrow> X1 homeomorphic_space X3"
```
```  1949   unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose)
```
```  1950
```
```  1951 lemma homeomorphic_space:
```
```  1952      "X homeomorphic_space Y \<longleftrightarrow> (\<exists>f. homeomorphic_map X Y f)"
```
```  1953   by (simp add: homeomorphic_map_maps homeomorphic_space_def)
```
```  1954
```
```  1955 lemma homeomorphic_maps_imp_homeomorphic_space:
```
```  1956      "homeomorphic_maps X Y f g \<Longrightarrow> X homeomorphic_space Y"
```
```  1957   unfolding homeomorphic_space_def by metis
```
```  1958
```
```  1959 lemma homeomorphic_map_imp_homeomorphic_space:
```
```  1960      "homeomorphic_map X Y f \<Longrightarrow> X homeomorphic_space Y"
```
```  1961   unfolding homeomorphic_map_maps
```
```  1962   using homeomorphic_space_def by blast
```
```  1963
```
```  1964 lemma homeomorphic_empty_space:
```
```  1965      "X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
```
```  1966   by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty)
```
```  1967
```
```  1968 lemma homeomorphic_empty_space_eq:
```
```  1969   assumes "topspace X = {}"
```
```  1970     shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
```
```  1971 proof -
```
```  1972   have "\<forall>f t. continuous_map X (t::'b topology) f"
```
```  1973     using assms continuous_map_on_empty by blast
```
```  1974   then show ?thesis
```
```  1975     by (metis (no_types) assms continuous_map_on_empty empty_iff homeomorphic_empty_space homeomorphic_maps_def homeomorphic_space_def)
```
```  1976 qed
```
```  1977
```
```  1978 subsection\<open>Connected topological spaces\<close>
```
```  1979
```
```  1980 definition connected_space :: "'a topology \<Rightarrow> bool" where
```
```  1981   "connected_space X \<equiv>
```
```  1982         ~(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
```
```  1983                   topspace X \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
```
```  1984
```
```  1985 definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
```
```  1986   "connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
```
```  1987
```
```  1988 lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
```
```  1989   by (simp add: connectedin_def)
```
```  1990
```
```  1991 lemma connectedin_topspace:
```
```  1992      "connectedin X (topspace X) \<longleftrightarrow> connected_space X"
```
```  1993   by (simp add: connectedin_def)
```
```  1994
```
```  1995 lemma connected_space_subtopology:
```
```  1996      "connectedin X S \<Longrightarrow> connected_space (subtopology X S)"
```
```  1997   by (simp add: connectedin_def)
```
```  1998
```
```  1999 lemma connectedin_subtopology:
```
```  2000      "connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> S"
```
```  2001   by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2)
```
```  2002
```
```  2003 lemma connected_space_eq:
```
```  2004      "connected_space X \<longleftrightarrow>
```
```  2005       (\<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> {})"
```
```  2006   unfolding connected_space_def
```
```  2007   by (metis openin_Un openin_subset subset_antisym)
```
```  2008
```
```  2009 lemma connected_space_closedin:
```
```  2010      "connected_space X \<longleftrightarrow>
```
```  2011       (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and> topspace X \<subseteq> E1 \<union> E2 \<and>
```
```  2012                E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" (is "?lhs = ?rhs")
```
```  2013 proof
```
```  2014   assume ?lhs
```
```  2015   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 = {}"
```
```  2016     by (simp add: connected_space_def)
```
```  2017   show ?rhs
```
```  2018     unfolding connected_space_def
```
```  2019   proof clarify
```
```  2020     fix E1 E2
```
```  2021     assume "closedin X E1" and "closedin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
```
```  2022       and "E1 \<noteq> {}" and "E2 \<noteq> {}"
```
```  2023     have "E1 \<union> E2 = topspace X"
```
```  2024       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)
```
```  2025     then have "topspace X - E2 = E1"
```
```  2026       using \<open>E1 \<inter> E2 = {}\<close> by fastforce
```
```  2027     then have "topspace X = E1"
```
```  2028       using \<open>E1 \<noteq> {}\<close> L \<open>closedin X E1\<close> \<open>closedin X E2\<close> by blast
```
```  2029     then show "False"
```
```  2030       using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
```
```  2031   qed
```
```  2032 next
```
```  2033   assume R: ?rhs
```
```  2034   show ?lhs
```
```  2035     unfolding connected_space_def
```
```  2036   proof clarify
```
```  2037     fix E1 E2
```
```  2038     assume "openin X E1" and "openin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
```
```  2039       and "E1 \<noteq> {}" and "E2 \<noteq> {}"
```
```  2040     have "E1 \<union> E2 = topspace X"
```
```  2041       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)
```
```  2042     then have "topspace X - E2 = E1"
```
```  2043       using \<open>E1 \<inter> E2 = {}\<close> by fastforce
```
```  2044     then have "topspace X = E1"
```
```  2045       using \<open>E1 \<noteq> {}\<close> R \<open>openin X E1\<close> \<open>openin X E2\<close> by blast
```
```  2046     then show "False"
```
```  2047       using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
```
```  2048   qed
```
```  2049 qed
```
```  2050
```
```  2051 lemma connected_space_closedin_eq:
```
```  2052      "connected_space X \<longleftrightarrow>
```
```  2053        (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
```
```  2054                 E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
```
```  2055   apply (simp add: connected_space_closedin)
```
```  2056   apply (intro all_cong)
```
```  2057   using closedin_subset apply blast
```
```  2058   done
```
```  2059
```
```  2060 lemma connected_space_clopen_in:
```
```  2061      "connected_space X \<longleftrightarrow>
```
```  2062         (\<forall>T. openin X T \<and> closedin X T \<longrightarrow> T = {} \<or> T = topspace X)"
```
```  2063 proof -
```
```  2064   have eq: "openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> P
```
```  2065         \<longleftrightarrow> E2 = topspace X - E1 \<and> openin X E1 \<and> openin X E2 \<and> P" for E1 E2 P
```
```  2066     using openin_subset by blast
```
```  2067   show ?thesis
```
```  2068     unfolding connected_space_eq eq closedin_def
```
```  2069     by (auto simp: openin_closedin_eq)
```
```  2070 qed
```
```  2071
```
```  2072 lemma connectedin:
```
```  2073      "connectedin X S \<longleftrightarrow>
```
```  2074         S \<subseteq> topspace X \<and>
```
```  2075          (\<nexists>E1 E2.
```
```  2076              openin X E1 \<and> openin X E2 \<and>
```
```  2077              S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
```
```  2078 proof -
```
```  2079   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>
```
```  2080              R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
```
```  2081     by auto
```
```  2082   show ?thesis
```
```  2083     unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology Not_eq_iff *
```
```  2084     apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
```
```  2085     apply (blast elim: dest!: openin_subset)+
```
```  2086     done
```
```  2087 qed
```
```  2088
```
```  2089 lemma connectedin_iff_connected_real [simp]:
```
```  2090      "connectedin euclideanreal S \<longleftrightarrow> connected S"
```
```  2091     by (simp add: connected_def connectedin)
```
```  2092
```
```  2093 lemma connectedin_closedin:
```
```  2094    "connectedin X S \<longleftrightarrow>
```
```  2095         S \<subseteq> topspace X \<and>
```
```  2096         ~(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
```
```  2097                   S \<subseteq> (E1 \<union> E2) \<and>
```
```  2098                   (E1 \<inter> E2 \<inter> S = {}) \<and>
```
```  2099                   ~(E1 \<inter> S = {}) \<and> ~(E2 \<inter> S = {}))"
```
```  2100 proof -
```
```  2101   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>
```
```  2102              R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
```
```  2103     by auto
```
```  2104   show ?thesis
```
```  2105     unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology Not_eq_iff *
```
```  2106     apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
```
```  2107     apply (blast elim: dest!: openin_subset)+
```
```  2108     done
```
```  2109 qed
```
```  2110
```
```  2111 lemma connectedin_empty [simp]: "connectedin X {}"
```
```  2112   by (simp add: connectedin)
```
```  2113
```
```  2114 lemma connected_space_topspace_empty:
```
```  2115      "topspace X = {} \<Longrightarrow> connected_space X"
```
```  2116   using connectedin_topspace by fastforce
```
```  2117
```
```  2118 lemma connectedin_sing [simp]: "connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
```
```  2119   by (simp add: connectedin)
```
```  2120
```
```  2121 lemma connectedin_absolute [simp]:
```
```  2122   "connectedin (subtopology X S) S \<longleftrightarrow> connectedin X S"
```
```  2123   apply (simp only: connectedin_def topspace_subtopology subtopology_subtopology)
```
```  2124   apply (intro conj_cong imp_cong arg_cong [where f=Not] all_cong1 ex_cong1 refl)
```
```  2125   by auto
```
```  2126
```
```  2127 lemma connectedin_Union:
```
```  2128   assumes \<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> connectedin X S" and ne: "\<Inter>\<U> \<noteq> {}"
```
```  2129   shows "connectedin X (\<Union>\<U>)"
```
```  2130 proof -
```
```  2131   have "\<Union>\<U> \<subseteq> topspace X"
```
```  2132     using \<U> by (simp add: Union_least connectedin_def)
```
```  2133   moreover have False
```
```  2134     if "openin X E1" "openin X E2" and cover: "\<Union>\<U> \<subseteq> E1 \<union> E2" and disj: "E1 \<inter> E2 \<inter> \<Union>\<U> = {}"
```
```  2135        and overlap1: "E1 \<inter> \<Union>\<U> \<noteq> {}" and overlap2: "E2 \<inter> \<Union>\<U> \<noteq> {}"
```
```  2136       for E1 E2
```
```  2137   proof -
```
```  2138     have disjS: "E1 \<inter> E2 \<inter> S = {}" if "S \<in> \<U>" for S
```
```  2139       using Diff_triv that disj by auto
```
```  2140     have coverS: "S \<subseteq> E1 \<union> E2" if "S \<in> \<U>" for S
```
```  2141       using that cover by blast
```
```  2142     have "\<U> \<noteq> {}"
```
```  2143       using overlap1 by blast
```
```  2144     obtain a where a: "\<And>U. U \<in> \<U> \<Longrightarrow> a \<in> U"
```
```  2145       using ne by force
```
```  2146     with \<open>\<U> \<noteq> {}\<close> have "a \<in> \<Union>\<U>"
```
```  2147       by blast
```
```  2148     then consider "a \<in> E1" | "a \<in> E2"
```
```  2149       using \<open>\<Union>\<U> \<subseteq> E1 \<union> E2\<close> by auto
```
```  2150     then show False
```
```  2151     proof cases
```
```  2152       case 1
```
```  2153       then obtain b S where "b \<in> E2" "b \<in> S" "S \<in> \<U>"
```
```  2154         using overlap2 by blast
```
```  2155       then show ?thesis
```
```  2156         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>]
```
```  2157         unfolding connectedin
```
```  2158         by (meson disjoint_iff_not_equal)
```
```  2159     next
```
```  2160       case 2
```
```  2161       then obtain b S where "b \<in> E1" "b \<in> S" "S \<in> \<U>"
```
```  2162         using overlap1 by blast
```
```  2163       then show ?thesis
```
```  2164         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>]
```
```  2165         unfolding connectedin
```
```  2166         by (meson disjoint_iff_not_equal)
```
```  2167     qed
```
```  2168   qed
```
```  2169   ultimately show ?thesis
```
```  2170     unfolding connectedin by blast
```
```  2171 qed
```
```  2172
```
```  2173 lemma connectedin_Un:
```
```  2174      "\<lbrakk>connectedin X S; connectedin X T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
```
```  2175   using connectedin_Union [of "{S,T}"] by auto
```
```  2176
```
```  2177 lemma connected_space_subconnected:
```
```  2178   "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")
```
```  2179 proof
```
```  2180   assume ?lhs
```
```  2181   then show ?rhs
```
```  2182     using connectedin_topspace by blast
```
```  2183 next
```
```  2184   assume R [rule_format]: ?rhs
```
```  2185   have False if "openin X U" "openin X V" and disj: "U \<inter> V = {}" and cover: "topspace X \<subseteq> U \<union> V"
```
```  2186     and "U \<noteq> {}" "V \<noteq> {}" for U V
```
```  2187   proof -
```
```  2188     obtain u v where "u \<in> U" "v \<in> V"
```
```  2189       using \<open>U \<noteq> {}\<close> \<open>V \<noteq> {}\<close> by auto
```
```  2190     then obtain T where "u \<in> T" "v \<in> T" and T: "connectedin X T"
```
```  2191       using R [of u v] that
```
```  2192       by (meson \<open>openin X U\<close> \<open>openin X V\<close> subsetD openin_subset)
```
```  2193     then show False
```
```  2194       using that unfolding connectedin
```
```  2195       by (metis IntI \<open>u \<in> U\<close> \<open>v \<in> V\<close> empty_iff inf_bot_left subset_trans)
```
```  2196   qed
```
```  2197   then show ?lhs
```
```  2198     by (auto simp: connected_space_def)
```
```  2199 qed
```
```  2200
```
```  2201 lemma connectedin_intermediate_closure_of:
```
```  2202   assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
```
```  2203   shows "connectedin X T"
```
```  2204 proof -
```
```  2205   have S: "S \<subseteq> topspace X"and T: "T \<subseteq> topspace X"
```
```  2206     using assms by (meson closure_of_subset_topspace dual_order.trans)+
```
```  2207   show ?thesis
```
```  2208   using assms
```
```  2209   apply (simp add: connectedin closure_of_subset_topspace S T)
```
```  2210   apply (elim all_forward imp_forward2 asm_rl)
```
```  2211   apply (blast dest: openin_Int_closure_of_eq_empty [of X _ S])+
```
```  2212   done
```
```  2213 qed
```
```  2214
```
```  2215 lemma connectedin_closure_of:
```
```  2216      "connectedin X S \<Longrightarrow> connectedin X (X closure_of S)"
```
```  2217   by (meson closure_of_subset connectedin_def connectedin_intermediate_closure_of subset_refl)
```
```  2218
```
```  2219 lemma connectedin_separation:
```
```  2220   "connectedin X S \<longleftrightarrow>
```
```  2221         S \<subseteq> topspace X \<and>
```
```  2222         (\<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")
```
```  2223   unfolding connectedin_def connected_space_closedin_eq closedin_Int_closure_of topspace_subtopology
```
```  2224   apply (intro conj_cong refl arg_cong [where f=Not])
```
```  2225   apply (intro ex_cong1 iffI, blast)
```
```  2226   using closure_of_subset_Int by force
```
```  2227
```
```  2228 lemma connectedin_eq_not_separated:
```
```  2229    "connectedin X S \<longleftrightarrow>
```
```  2230          S \<subseteq> topspace X \<and>
```
```  2231          (\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
```
```  2232   apply (simp add: separatedin_def connectedin_separation)
```
```  2233   apply (intro conj_cong all_cong1 refl, blast)
```
```  2234   done
```
```  2235
```
```  2236 lemma connectedin_eq_not_separated_subset:
```
```  2237   "connectedin X S \<longleftrightarrow>
```
```  2238       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)"
```
```  2239 proof -
```
```  2240   have *: "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
```
```  2241     if "\<And>C1 C2. C1 \<union> C2 = S \<longrightarrow> C1 = {} \<or> C2 = {} \<or> \<not> separatedin X C1 C2"
```
```  2242   proof (intro allI)
```
```  2243     fix C1 C2
```
```  2244     show "S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
```
```  2245       using that [of "S \<inter> C1" "S \<inter> C2"]
```
```  2246       by (auto simp: separatedin_mono)
```
```  2247   qed
```
```  2248   show ?thesis
```
```  2249     apply (simp add: connectedin_eq_not_separated)
```
```  2250     apply (intro conj_cong refl iffI *)
```
```  2251     apply (blast elim!: all_forward)+
```
```  2252     done
```
```  2253 qed
```
```  2254
```
```  2255 lemma connected_space_eq_not_separated:
```
```  2256      "connected_space X \<longleftrightarrow>
```
```  2257       (\<nexists>C1 C2. C1 \<union> C2 = topspace X \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
```
```  2258   by (simp add: connectedin_eq_not_separated flip: connectedin_topspace)
```
```  2259
```
```  2260 lemma connected_space_eq_not_separated_subset:
```
```  2261   "connected_space X \<longleftrightarrow>
```
```  2262     (\<nexists>C1 C2. topspace X \<subseteq> C1 \<union> C2 \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
```
```  2263   apply (simp add: connected_space_eq_not_separated)
```
```  2264   apply (intro all_cong1)
```
```  2265   by (metis Un_absorb dual_order.antisym separatedin_def subset_refl sup_mono)
```
```  2266
```
```  2267 lemma connectedin_subset_separated_union:
```
```  2268      "\<lbrakk>connectedin X C; separatedin X S T; C \<subseteq> S \<union> T\<rbrakk> \<Longrightarrow> C \<subseteq> S \<or> C \<subseteq> T"
```
```  2269   unfolding connectedin_eq_not_separated_subset  by blast
```
```  2270
```
```  2271 lemma connectedin_nonseparated_union:
```
```  2272    "\<lbrakk>connectedin X S; connectedin X T; ~separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
```
```  2273   apply (simp add: connectedin_eq_not_separated_subset, auto)
```
```  2274     apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
```
```  2275   apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
```
```  2276   by (meson disjoint_iff_not_equal)
```
```  2277
```
```  2278 lemma connected_space_closures:
```
```  2279      "connected_space X \<longleftrightarrow>
```
```  2280         (\<nexists>e1 e2. e1 \<union> e2 = topspace X \<and> X closure_of e1 \<inter> X closure_of e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
```
```  2281      (is "?lhs = ?rhs")
```
```  2282 proof
```
```  2283   assume ?lhs
```
```  2284   then show ?rhs
```
```  2285     unfolding connected_space_closedin_eq
```
```  2286     by (metis Un_upper1 Un_upper2 closedin_closure_of closure_of_Un closure_of_eq_empty closure_of_topspace)
```
```  2287 next
```
```  2288   assume ?rhs
```
```  2289   then show ?lhs
```
```  2290     unfolding connected_space_closedin_eq
```
```  2291     by (metis closure_of_eq)
```
```  2292 qed
```
```  2293
```
```  2294 lemma connectedin_inter_frontier_of:
```
```  2295   assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
```
```  2296   shows "S \<inter> X frontier_of T \<noteq> {}"
```
```  2297 proof -
```
```  2298   have "S \<subseteq> topspace X" and *:
```
```  2299     "\<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 = {}"
```
```  2300     using \<open>connectedin X S\<close> by (auto simp: connectedin)
```
```  2301   have "S - (topspace X \<inter> T) \<noteq> {}"
```
```  2302     using assms(3) by blast
```
```  2303   moreover
```
```  2304   have "S \<inter> topspace X \<inter> T \<noteq> {}"
```
```  2305     using assms(1) assms(2) connectedin by fastforce
```
```  2306   moreover
```
```  2307   have False if "S \<inter> T \<noteq> {}" "S - T \<noteq> {}" "T \<subseteq> topspace X" "S \<inter> X frontier_of T = {}" for T
```
```  2308   proof -
```
```  2309     have null: "S \<inter> (X closure_of T - X interior_of T) = {}"
```
```  2310       using that unfolding frontier_of_def by blast
```
```  2311     have 1: "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
```
```  2312       by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty)
```
```  2313     have 2: "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
```
```  2314       using that \<open>S \<subseteq> topspace X\<close> null by auto
```
```  2315     have 3: "S \<inter> X interior_of T \<noteq> {}"
```
```  2316       using closure_of_subset that(1) that(3) null by fastforce
```
```  2317     show ?thesis
```
```  2318       using null \<open>S \<subseteq> topspace X\<close> that * [of "X interior_of T" "topspace X - X closure_of T"]
```
```  2319       apply (clarsimp simp add: openin_diff 1 2)
```
```  2320       apply (simp add: Int_commute Diff_Int_distrib 3)
```
```  2321       by (metis Int_absorb2 contra_subsetD interior_of_subset)
```
```  2322   qed
```
```  2323   ultimately show ?thesis
```
```  2324     by (metis Int_lower1 frontier_of_restrict inf_assoc)
```
```  2325 qed
```
```  2326
```
```  2327 lemma connectedin_continuous_map_image:
```
```  2328   assumes f: "continuous_map X Y f" and "connectedin X S"
```
```  2329   shows "connectedin Y (f ` S)"
```
```  2330 proof -
```
```  2331   have "S \<subseteq> topspace X" and *:
```
```  2332     "\<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 = {}"
```
```  2333     using \<open>connectedin X S\<close> by (auto simp: connectedin)
```
```  2334   show ?thesis
```
```  2335     unfolding connectedin connected_space_def
```
```  2336   proof (intro conjI notI; clarify)
```
```  2337     show "f x \<in> topspace Y" if  "x \<in> S" for x
```
```  2338       using \<open>S \<subseteq> topspace X\<close> continuous_map_image_subset_topspace f that by blast
```
```  2339   next
```
```  2340     fix U V
```
```  2341     let ?U = "{x \<in> topspace X. f x \<in> U}"
```
```  2342     let ?V = "{x \<in> topspace X. f x \<in> V}"
```
```  2343     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> {}"
```
```  2344     then have 1: "?U \<inter> ?V \<inter> S = {}"
```
```  2345       by auto
```
```  2346     have 2: "openin X ?U" "openin X ?V"
```
```  2347       using \<open>openin Y U\<close> \<open>openin Y V\<close> continuous_map f by fastforce+
```
```  2348     show "False"
```
```  2349       using  * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
```
```  2350       by (auto simp: 1 2)
```
```  2351   qed
```
```  2352 qed
```
```  2353
```
```  2354 lemma homeomorphic_connected_space:
```
```  2355      "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
```
```  2356   unfolding homeomorphic_space_def homeomorphic_maps_def
```
```  2357   apply safe
```
```  2358   apply (metis connectedin_continuous_map_image connected_space_subconnected continuous_map_image_subset_topspace image_eqI image_subset_iff)
```
```  2359   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)
```
```  2360
```
```  2361 lemma homeomorphic_map_connectedness:
```
```  2362   assumes f: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
```
```  2363   shows "connectedin Y (f ` U) \<longleftrightarrow> connectedin X U"
```
```  2364 proof -
```
```  2365   have 1: "f ` U \<subseteq> topspace Y \<longleftrightarrow> U \<subseteq> topspace X"
```
```  2366     using U f homeomorphic_imp_surjective_map by blast
```
```  2367   moreover have "connected_space (subtopology Y (f ` U)) \<longleftrightarrow> connected_space (subtopology X U)"
```
```  2368   proof (rule homeomorphic_connected_space)
```
```  2369     have "f ` U \<subseteq> topspace Y"
```
```  2370       by (simp add: U 1)
```
```  2371     then have "topspace Y \<inter> f ` U = f ` U"
```
```  2372       by (simp add: subset_antisym)
```
```  2373     then show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
```
```  2374       by (metis (no_types) Int_subset_iff U f homeomorphic_map_imp_homeomorphic_space homeomorphic_map_subtopologies homeomorphic_space_sym subset_antisym subset_refl)
```
```  2375   qed
```
```  2376   ultimately show ?thesis
```
```  2377     by (auto simp: connectedin_def)
```
```  2378 qed
```
```  2379
```
```  2380 lemma homeomorphic_map_connectedness_eq:
```
```  2381    "homeomorphic_map X Y f
```
```  2382         \<Longrightarrow> connectedin X U \<longleftrightarrow>
```
```  2383              U \<subseteq> topspace X \<and> connectedin Y (f ` U)"
```
```  2384   using homeomorphic_map_connectedness connectedin_subset_topspace by metis
```
```  2385
```
```  2386 lemma connectedin_discrete_topology:
```
```  2387    "connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
```
```  2388 proof (cases "S \<subseteq> U")
```
```  2389   case True
```
```  2390   show ?thesis
```
```  2391   proof (cases "S = {}")
```
```  2392     case False
```
```  2393     moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
```
```  2394       apply safe
```
```  2395       using False connectedin_inter_frontier_of insert_Diff apply fastforce
```
```  2396       using True by auto
```
```  2397     ultimately show ?thesis
```
```  2398       by auto
```
```  2399   qed simp
```
```  2400 next
```
```  2401   case False
```
```  2402   then show ?thesis
```
```  2403     by (simp add: connectedin_def)
```
```  2404 qed
```
```  2405
```
```  2406 lemma connected_space_discrete_topology:
```
```  2407      "connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
```
```  2408   by (metis connectedin_discrete_topology connectedin_topspace order_refl topspace_discrete_topology)
```
```  2409
```
```  2410
```
```  2411 subsection\<open>Compact sets\<close>
```
```  2412
```
```  2413 definition compactin where
```
```  2414  "compactin X S \<longleftrightarrow>
```
```  2415      S \<subseteq> topspace X \<and>
```
```  2416      (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
```
```  2417           \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>))"
```
```  2418
```
```  2419 definition compact_space where
```
```  2420    "compact_space X \<equiv> compactin X (topspace X)"
```
```  2421
```
```  2422 lemma compact_space_alt:
```
```  2423    "compact_space X \<longleftrightarrow>
```
```  2424         (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
```
```  2425             \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>))"
```
```  2426   by (simp add: compact_space_def compactin_def)
```
```  2427
```
```  2428 lemma compact_space:
```
```  2429    "compact_space X \<longleftrightarrow>
```
```  2430         (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
```
```  2431             \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> \<Union>\<F> = topspace X))"
```
```  2432   unfolding compact_space_alt
```
```  2433   using openin_subset by fastforce
```
```  2434
```
```  2435 lemma compactin_euclideanreal_iff [simp]: "compactin euclideanreal S \<longleftrightarrow> compact S"
```
```  2436   by (simp add: compact_eq_heine_borel compactin_def) meson
```
```  2437
```
```  2438 lemma compactin_absolute [simp]:
```
```  2439    "compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
```
```  2440 proof -
```
```  2441   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>
```
```  2442     by auto
```
```  2443   show ?thesis
```
```  2444     by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
```
```  2445 qed
```
```  2446
```
```  2447 lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
```
```  2448   unfolding compact_space_def topspace_subtopology
```
```  2449   by (metis compactin_absolute compactin_def inf.absorb2)
```
```  2450
```
```  2451 lemma compact_space_subtopology: "compactin X S \<Longrightarrow> compact_space (subtopology X S)"
```
```  2452   by (simp add: compactin_subspace)
```
```  2453
```
```  2454 lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
```
```  2455 apply (simp add: compactin_subspace topspace_subtopology)
```
```  2456   by (metis inf.orderE inf_commute subtopology_subtopology)
```
```  2457
```
```  2458
```
```  2459 lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
```
```  2460   by (simp add: compactin_subspace)
```
```  2461
```
```  2462 lemma compactin_contractive:
```
```  2463    "\<lbrakk>compactin X' S; topspace X' = topspace X;
```
```  2464      \<And>U. openin X U \<Longrightarrow> openin X' U\<rbrakk> \<Longrightarrow> compactin X S"
```
```  2465   by (simp add: compactin_def)
```
```  2466
```
```  2467 lemma finite_imp_compactin:
```
```  2468    "\<lbrakk>S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> compactin X S"
```
```  2469   by (metis compactin_subspace compact_space finite_UnionD inf.absorb_iff2 order_refl topspace_subtopology)
```
```  2470
```
```  2471 lemma compactin_empty [iff]: "compactin X {}"
```
```  2472   by (simp add: finite_imp_compactin)
```
```  2473
```
```  2474 lemma compact_space_topspace_empty:
```
```  2475    "topspace X = {} \<Longrightarrow> compact_space X"
```
```  2476   by (simp add: compact_space_def)
```
```  2477
```
```  2478 lemma finite_imp_compactin_eq:
```
```  2479    "finite S \<Longrightarrow> (compactin X S \<longleftrightarrow> S \<subseteq> topspace X)"
```
```  2480   using compactin_subset_topspace finite_imp_compactin by blast
```
```  2481
```
```  2482 lemma compactin_sing [simp]: "compactin X {a} \<longleftrightarrow> a \<in> topspace X"
```
```  2483   by (simp add: finite_imp_compactin_eq)
```
```  2484
```
```  2485 lemma closed_compactin:
```
```  2486   assumes XK: "compactin X K" and "C \<subseteq> K" and XC: "closedin X C"
```
```  2487   shows "compactin X C"
```
```  2488   unfolding compactin_def
```
```  2489 proof (intro conjI allI impI)
```
```  2490   show "C \<subseteq> topspace X"
```
```  2491     by (simp add: XC closedin_subset)
```
```  2492 next
```
```  2493   fix \<U> :: "'a set set"
```
```  2494   assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
```
```  2495   have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
```
```  2496     using XC \<U> by blast
```
```  2497   moreover have "K \<subseteq> \<Union>insert (topspace X - C) \<U>"
```
```  2498     using \<U> XK compactin_subset_topspace by fastforce
```
```  2499   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
```
```  2500     using assms unfolding compactin_def by metis
```
```  2501   moreover have "openin X (topspace X - C)"
```
```  2502     using XC by auto
```
```  2503   ultimately show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> C \<subseteq> \<Union>\<F>"
```
```  2504     using \<open>C \<subseteq> K\<close>
```
```  2505     by (rule_tac x="\<F> - {topspace X - C}" in exI) auto
```
```  2506 qed
```
```  2507
```
```  2508 lemma closedin_compact_space:
```
```  2509    "\<lbrakk>compact_space X; closedin X S\<rbrakk> \<Longrightarrow> compactin X S"
```
```  2510   by (simp add: closed_compactin closedin_subset compact_space_def)
```
```  2511
```
```  2512 lemma compact_Int_closedin:
```
```  2513   assumes "compactin X S" "closedin X T" shows "compactin X (S \<inter> T)"
```
```  2514 proof -
```
```  2515   have "compactin (subtopology X S) (S \<inter> T)"
```
```  2516     by (metis assms closedin_compact_space closedin_subtopology compactin_subspace inf_commute)
```
```  2517   then show ?thesis
```
```  2518     by (simp add: compactin_subtopology)
```
```  2519 qed
```
```  2520
```
```  2521 lemma closed_Int_compactin: "\<lbrakk>closedin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
```
```  2522   by (metis compact_Int_closedin inf_commute)
```
```  2523
```
```  2524 lemma compactin_Un:
```
```  2525   assumes S: "compactin X S" and T: "compactin X T" shows "compactin X (S \<union> T)"
```
```  2526   unfolding compactin_def
```
```  2527 proof (intro conjI allI impI)
```
```  2528   show "S \<union> T \<subseteq> topspace X"
```
```  2529     using assms by (auto simp: compactin_def)
```
```  2530 next
```
```  2531   fix \<U> :: "'a set set"
```
```  2532   assume \<U>: "Ball \<U> (openin X) \<and> S \<union> T \<subseteq> \<Union>\<U>"
```
```  2533   with S obtain \<F> where \<V>: "finite \<F>" "\<F> \<subseteq> \<U>" "S \<subseteq> \<Union>\<F>"
```
```  2534     unfolding compactin_def by (meson sup.bounded_iff)
```
```  2535   obtain \<W> where "finite \<W>" "\<W> \<subseteq> \<U>" "T \<subseteq> \<Union>\<W>"
```
```  2536     using \<U> T
```
```  2537     unfolding compactin_def by (meson sup.bounded_iff)
```
```  2538   with \<V> show "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> S \<union> T \<subseteq> \<Union>\<V>"
```
```  2539     by (rule_tac x="\<F> \<union> \<W>" in exI) auto
```
```  2540 qed
```
```  2541
```
```  2542 lemma compactin_Union:
```
```  2543    "\<lbrakk>finite \<F>; \<And>S. S \<in> \<F> \<Longrightarrow> compactin X S\<rbrakk> \<Longrightarrow> compactin X (\<Union>\<F>)"
```
```  2544 by (induction rule: finite_induct) (simp_all add: compactin_Un)
```
```  2545
```
```  2546 lemma compactin_subtopology_imp_compact:
```
```  2547   assumes "compactin (subtopology X S) K" shows "compactin X K"
```
```  2548   using assms
```
```  2549 proof (clarsimp simp add: compactin_def topspace_subtopology)
```
```  2550   fix \<U>
```
```  2551   define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
```
```  2552   assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
```
```  2553   then have "\<forall>V \<in> \<V>. openin (subtopology X S) V" "K \<subseteq> \<Union>\<V>"
```
```  2554     unfolding \<V>_def by (auto simp: openin_subtopology)
```
```  2555   moreover
```
```  2556   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>)"
```
```  2557   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
```
```  2558     by meson
```
```  2559   then have \<F>: "\<exists>U. U \<in> \<U> \<and> V = U \<inter> S" if "V \<in> \<F>" for V
```
```  2560     unfolding \<V>_def using that by blast
```
```  2561   let ?\<F> = "(\<lambda>F. @U. U \<in> \<U> \<and> F = U \<inter> S) ` \<F>"
```
```  2562   show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
```
```  2563   proof (intro exI conjI)
```
```  2564     show "finite ?\<F>"
```
```  2565       using \<open>finite \<F>\<close> by blast
```
```  2566     show "?\<F> \<subseteq> \<U>"
```
```  2567       using someI_ex [OF \<F>] by blast
```
```  2568     show "K \<subseteq> \<Union>?\<F>"
```
```  2569     proof clarsimp
```
```  2570       fix x
```
```  2571       assume "x \<in> K"
```
```  2572       then show "\<exists>V \<in> \<F>. x \<in> (SOME U. U \<in> \<U> \<and> V = U \<inter> S)"
```
```  2573         using \<open>K \<subseteq> \<Union>\<F>\<close> someI_ex [OF \<F>]
```
```  2574         by (metis (no_types, lifting) IntD1 Union_iff subsetCE)
```
```  2575     qed
```
```  2576   qed
```
```  2577 qed
```
```  2578
```
```  2579 lemma compact_imp_compactin_subtopology:
```
```  2580   assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
```
```  2581   using assms
```
```  2582 proof (clarsimp simp add: compactin_def topspace_subtopology)
```
```  2583   fix \<U> :: "'a set set"
```
```  2584   define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
```
```  2585   assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
```
```  2586   then have "\<forall>V \<in> \<V>. openin X V" "K \<subseteq> \<Union>\<V>"
```
```  2587     unfolding \<V>_def by (fastforce simp: subset_eq openin_subtopology)+
```
```  2588   moreover
```
```  2589   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>)"
```
```  2590   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
```
```  2591     by meson
```
```  2592   let ?\<F> = "(\<lambda>F. F \<inter> S) ` \<F>"
```
```  2593   show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
```
```  2594   proof (intro exI conjI)
```
```  2595     show "finite ?\<F>"
```
```  2596       using \<open>finite \<F>\<close> by blast
```
```  2597     show "?\<F> \<subseteq> \<U>"
```
```  2598       using \<V>_def \<open>\<F> \<subseteq> \<V>\<close> by blast
```
```  2599     show "K \<subseteq> \<Union>?\<F>"
```
```  2600       using \<open>K \<subseteq> \<Union>\<F>\<close> assms(2) by auto
```
```  2601   qed
```
```  2602 qed
```
```  2603
```
```  2604
```
```  2605 proposition compact_space_fip:
```
```  2606    "compact_space X \<longleftrightarrow>
```
```  2607     (\<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> {})"
```
```  2608    (is "_ = ?rhs")
```
```  2609 proof (cases "topspace X = {}")
```
```  2610   case True
```
```  2611   then show ?thesis
```
```  2612     apply (clarsimp simp add: compact_space_def closedin_topspace_empty)
```
```  2613     by (metis finite.emptyI finite_insert infinite_super insertI1 subsetI)
```
```  2614 next
```
```  2615   case False
```
```  2616   show ?thesis
```
```  2617   proof safe
```
```  2618     fix \<U> :: "'a set set"
```
```  2619     assume * [rule_format]: "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
```
```  2620     define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
```
```  2621     assume clo: "\<forall>C\<in>\<U>. closedin X C" and [simp]: "\<Inter>\<U> = {}"
```
```  2622     then have "\<forall>V \<in> \<V>. openin X V" "topspace X \<subseteq> \<Union>\<V>"
```
```  2623       by (auto simp: \<V>_def)
```
```  2624     moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
```
```  2625     ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
```
```  2626       by (auto simp: exists_finite_subset_image \<V>_def)
```
```  2627     moreover have "\<F> \<noteq> {}"
```
```  2628       using \<F> \<open>topspace X \<noteq> {}\<close> by blast
```
```  2629     ultimately show "False"
```
```  2630       using * [of \<F>]
```
```  2631       by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
```
```  2632   next
```
```  2633     assume R [rule_format]: ?rhs
```
```  2634     show "compact_space X"
```
```  2635       unfolding compact_space_alt
```
```  2636     proof clarify
```
```  2637       fix \<U> :: "'a set set"
```
```  2638       define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
```
```  2639       assume "\<forall>C\<in>\<U>. openin X C" and "topspace X \<subseteq> \<Union>\<U>"
```
```  2640       with \<open>topspace X \<noteq> {}\<close> have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
```
```  2641         by (auto simp: \<V>_def)
```
```  2642       show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>"
```
```  2643       proof (rule ccontr; simp)
```
```  2644         assume "\<forall>\<F>\<subseteq>\<U>. finite \<F> \<longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>"
```
```  2645         then have "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<V> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
```
```  2646           by (simp add: \<V>_def all_finite_subset_image)
```
```  2647         with \<open>topspace X \<subseteq> \<Union>\<U>\<close> show False
```
```  2648           using R [of \<V>] * by (simp add: \<V>_def)
```
```  2649       qed
```
```  2650     qed
```
```  2651   qed
```
```  2652 qed
```
```  2653
```
```  2654 corollary compactin_fip:
```
```  2655   "compactin X S \<longleftrightarrow>
```
```  2656     S \<subseteq> topspace X \<and>
```
```  2657     (\<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> {})"
```
```  2658 proof (cases "S = {}")
```
```  2659   case False
```
```  2660   show ?thesis
```
```  2661   proof (cases "S \<subseteq> topspace X")
```
```  2662     case True
```
```  2663     then have "compactin X S \<longleftrightarrow>
```
```  2664           (\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
```
```  2665            (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
```
```  2666       by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
```
```  2667     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> ((\<inter>) S ` \<U>) \<noteq> {})"
```
```  2668       by (simp add: all_subset_image)
```
```  2669     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> {})"
```
```  2670     proof -
```
```  2671       have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
```
```  2672                 ((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"  for \<U>
```
```  2673         by simp (use \<open>S \<noteq> {}\<close> in blast)
```
```  2674       show ?thesis
```
```  2675         apply (simp only: imp_conjL [symmetric] all_finite_subset_image eq)
```
```  2676         apply (simp add: subset_eq)
```
```  2677         done
```
```  2678     qed
```
```  2679     finally show ?thesis
```
```  2680       using True by simp
```
```  2681   qed (simp add: compactin_subspace)
```
```  2682 qed force
```
```  2683
```
```  2684 corollary compact_space_imp_nest:
```
```  2685   fixes C :: "nat \<Rightarrow> 'a set"
```
```  2686   assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
```
```  2687     and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
```
```  2688   shows "(\<Inter>n. C n) \<noteq> {}"
```
```  2689 proof -
```
```  2690   let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
```
```  2691   have "closedin X A" if "A \<in> ?\<U>" for A
```
```  2692     using that clo by auto
```
```  2693   moreover have "(\<Inter>n\<in>K. \<Inter>m \<le> n. C m) \<noteq> {}" if "finite K" for K
```
```  2694   proof -
```
```  2695     obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
```
```  2696       using Max.coboundedI \<open>finite K\<close> by blast
```
```  2697     with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
```
```  2698     by blast
```
```  2699   with ne [of n] show ?thesis
```
```  2700     by blast
```
```  2701   qed
```
```  2702   ultimately show ?thesis
```
```  2703     using \<open>compact_space X\<close> [unfolded compact_space_fip, rule_format, of ?\<U>]
```
```  2704     by (simp add: all_finite_subset_image INT_extend_simps UN_atMost_UNIV del: INT_simps)
```
```  2705 qed
```
```  2706
```
```  2707 lemma compactin_discrete_topology:
```
```  2708    "compactin (discrete_topology X) S \<longleftrightarrow> S \<subseteq> X \<and> finite S" (is "?lhs = ?rhs")
```
```  2709 proof (intro iffI conjI)
```
```  2710   assume L: ?lhs
```
```  2711   then show "S \<subseteq> X"
```
```  2712     by (auto simp: compactin_def)
```
```  2713   have *: "\<And>\<U>. Ball \<U> (openin (discrete_topology X)) \<and> S \<subseteq> \<Union>\<U> \<Longrightarrow>
```
```  2714         (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>)"
```
```  2715     using L by (auto simp: compactin_def)
```
```  2716   show "finite S"
```
```  2717     using * [of "(\<lambda>x. {x}) ` X"] \<open>S \<subseteq> X\<close>
```
```  2718     by clarsimp (metis UN_singleton finite_subset_image infinite_super)
```
```  2719 next
```
```  2720   assume ?rhs
```
```  2721   then show ?lhs
```
```  2722     by (simp add: finite_imp_compactin)
```
```  2723 qed
```
```  2724
```
```  2725 lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
```
```  2726   by (simp add: compactin_discrete_topology compact_space_def)
```
```  2727
```
```  2728 lemma compact_space_imp_bolzano_weierstrass:
```
```  2729   assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
```
```  2730   shows "X derived_set_of S \<noteq> {}"
```
```  2731 proof
```
```  2732   assume X: "X derived_set_of S = {}"
```
```  2733   then have "closedin X S"
```
```  2734     by (simp add: closedin_contains_derived_set assms)
```
```  2735   then have "compactin X S"
```
```  2736     by (rule closedin_compact_space [OF \<open>compact_space X\<close>])
```
```  2737   with X show False
```
```  2738     by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
```
```  2739 qed
```
```  2740
```
```  2741 lemma compactin_imp_bolzano_weierstrass:
```
```  2742    "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
```
```  2743   using compact_space_imp_bolzano_weierstrass [of "subtopology X S"]
```
```  2744   by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
```
```  2745
```
```  2746 lemma compact_closure_of_imp_bolzano_weierstrass:
```
```  2747    "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
```
```  2748   using closure_of_mono closure_of_subset compactin_imp_bolzano_weierstrass by fastforce
```
```  2749
```
```  2750 lemma discrete_compactin_eq_finite:
```
```  2751    "S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
```
```  2752   apply (rule iffI)
```
```  2753   using compactin_imp_bolzano_weierstrass compactin_subset_topspace apply blast
```
```  2754   by (simp add: finite_imp_compactin_eq)
```
```  2755
```
```  2756 lemma discrete_compact_space_eq_finite:
```
```  2757    "X derived_set_of (topspace X) = {} \<Longrightarrow> (compact_space X \<longleftrightarrow> finite(topspace X))"
```
```  2758   by (metis compact_space_discrete_topology discrete_topology_unique_derived_set)
```
```  2759
```
```  2760 lemma image_compactin:
```
```  2761   assumes cpt: "compactin X S" and cont: "continuous_map X Y f"
```
```  2762   shows "compactin Y (f ` S)"
```
```  2763   unfolding compactin_def
```
```  2764 proof (intro conjI allI impI)
```
```  2765   show "f ` S \<subseteq> topspace Y"
```
```  2766     using compactin_subset_topspace cont continuous_map_image_subset_topspace cpt by blast
```
```  2767 next
```
```  2768   fix \<U> :: "'b set set"
```
```  2769   assume \<U>: "Ball \<U> (openin Y) \<and> f ` S \<subseteq> \<Union>\<U>"
```
```  2770   define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
```
```  2771   have "S \<subseteq> topspace X"
```
```  2772     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>"
```
```  2773     using cpt by (auto simp: compactin_def)
```
```  2774   obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<V>" "S \<subseteq> \<Union>\<F>"
```
```  2775   proof -
```
```  2776     have 1: "\<forall>U\<in>\<V>. openin X U"
```
```  2777       unfolding \<V>_def using \<U> cont continuous_map by blast
```
```  2778     have 2: "S \<subseteq> \<Union>\<V>"
```
```  2779       unfolding \<V>_def using compactin_subset_topspace cpt \<U> by fastforce
```
```  2780     show thesis
```
```  2781       using * [OF 1 2] that by metis
```
```  2782   qed
```
```  2783   have "\<forall>v \<in> \<V>. \<exists>U. U \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U}"
```
```  2784     using \<V>_def by blast
```
```  2785   then obtain U where U: "\<forall>v \<in> \<V>. U v \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U v}"
```
```  2786     by metis
```
```  2787   show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> f ` S \<subseteq> \<Union>\<F>"
```
```  2788   proof (intro conjI exI)
```
```  2789     show "finite (U ` \<F>)"
```
```  2790       by (simp add: \<open>finite \<F>\<close>)
```
```  2791   next
```
```  2792     show "U ` \<F> \<subseteq> \<U>"
```
```  2793       using \<open>\<F> \<subseteq> \<V>\<close> U by auto
```
```  2794   next
```
```  2795     show "f ` S \<subseteq> UNION \<F> U"
```
```  2796       using \<F>(2-3) U UnionE subset_eq U by fastforce
```
```  2797   qed
```
```  2798 qed
```
```  2799
```
```  2800
```
```  2801 lemma homeomorphic_compact_space:
```
```  2802   assumes "X homeomorphic_space Y"
```
```  2803   shows "compact_space X \<longleftrightarrow> compact_space Y"
```
```  2804     using homeomorphic_space_sym
```
```  2805     by (metis assms compact_space_def homeomorphic_eq_everything_map homeomorphic_space image_compactin)
```
```  2806
```
```  2807 lemma homeomorphic_map_compactness:
```
```  2808   assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
```
```  2809   shows "compactin Y (f ` U) \<longleftrightarrow> compactin X U"
```
```  2810 proof -
```
```  2811   have "f ` U \<subseteq> topspace Y"
```
```  2812     using hom U homeomorphic_imp_surjective_map by blast
```
```  2813   moreover have "homeomorphic_map (subtopology X U) (subtopology Y (f ` U)) f"
```
```  2814     using U hom homeomorphic_imp_surjective_map by (blast intro: homeomorphic_map_subtopologies)
```
```  2815   then have "compact_space (subtopology Y (f ` U)) = compact_space (subtopology X U)"
```
```  2816     using homeomorphic_compact_space homeomorphic_map_imp_homeomorphic_space by blast
```
```  2817   ultimately show ?thesis
```
```  2818     by (simp add: compactin_subspace U)
```
```  2819 qed
```
```  2820
```
```  2821 lemma homeomorphic_map_compactness_eq:
```
```  2822    "homeomorphic_map X Y f
```
```  2823         \<Longrightarrow> compactin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> compactin Y (f ` U)"
```
```  2824   by (meson compactin_subset_topspace homeomorphic_map_compactness)
```
```  2825
```
```  2826
```
```  2827 subsection\<open>Embedding maps\<close>
```
```  2828
```
```  2829 definition embedding_map
```
```  2830   where "embedding_map X Y f \<equiv> homeomorphic_map X (subtopology Y (f ` (topspace X))) f"
```
```  2831
```
```  2832 lemma embedding_map_eq:
```
```  2833    "\<lbrakk>embedding_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> embedding_map X Y g"
```
```  2834   unfolding embedding_map_def
```
```  2835   by (metis homeomorphic_map_eq image_cong)
```
```  2836
```
```  2837 lemma embedding_map_compose:
```
```  2838   assumes "embedding_map X X' f" "embedding_map X' X'' g"
```
```  2839   shows "embedding_map X X'' (g \<circ> f)"
```
```  2840 proof -
```
```  2841   have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g"
```
```  2842     using assms by (auto simp: embedding_map_def)
```
```  2843   then obtain C where "g ` topspace X' \<inter> C = (g \<circ> f) ` topspace X"
```
```  2844     by (metis (no_types) Int_absorb1 continuous_map_image_subset_topspace continuous_map_in_subtopology homeomorphic_eq_everything_map image_comp image_mono)
```
```  2845   then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \<circ> f) ` topspace X)) g"
```
```  2846     by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
```
```  2847   then show ?thesis
```
```  2848   unfolding embedding_map_def
```
```  2849   using hm(1) homeomorphic_map_compose by blast
```
```  2850 qed
```
```  2851
```
```  2852 lemma surjective_embedding_map:
```
```  2853    "embedding_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
```
```  2854   by (force simp: embedding_map_def homeomorphic_eq_everything_map)
```
```  2855
```
```  2856 lemma embedding_map_in_subtopology:
```
```  2857    "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
```
```  2858   apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
```
```  2859     apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
```
```  2860   apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
```
```  2861   done
```
```  2862
```
```  2863 lemma injective_open_imp_embedding_map:
```
```  2864    "\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
```
```  2865   unfolding embedding_map_def
```
```  2866   apply (rule bijective_open_imp_homeomorphic_map)
```
```  2867   using continuous_map_in_subtopology apply blast
```
```  2868     apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
```
```  2869   done
```
```  2870
```
```  2871 lemma injective_closed_imp_embedding_map:
```
```  2872   "\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
```
```  2873   unfolding embedding_map_def
```
```  2874   apply (rule bijective_closed_imp_homeomorphic_map)
```
```  2875      apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
```
```  2876   apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
```
```  2877   done
```
```  2878
```
```  2879 lemma embedding_map_imp_homeomorphic_space:
```
```  2880    "embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
```
```  2881   unfolding embedding_map_def
```
```  2882   using homeomorphic_space by blast
```
```  2883
```
```  2884 end
```