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