src/HOL/Analysis/Abstract_Topology.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69945 35ba13ac6e5c
child 69986 f2d327275065
permissions -rw-r--r--
more strict AFP properties;
     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
     8     Complex_Main
     9     "HOL-Library.Set_Idioms"
    10     "HOL-Library.FuncSet"
    11 begin
    12 
    13 subsection \<open>General notion of a topology as a value\<close>
    14 
    15 definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
    16 "istopology L \<longleftrightarrow>
    17   L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
    18 
    19 typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    20   morphisms "openin" "topology"
    21   unfolding istopology_def by blast
    22 
    23 lemma istopology_openin[intro]: "istopology(openin U)"
    24   using openin[of U] by blast
    25 
    26 lemma istopology_open: "istopology open"
    27   by (auto simp: istopology_def)
    28 
    29 lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
    30   using topology_inverse[unfolded mem_Collect_eq] .
    31 
    32 lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
    33   using topology_inverse[of U] istopology_openin[of "topology U"] by auto
    34 
    35 lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
    36 proof
    37   assume "T1 = T2"
    38   then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
    39 next
    40   assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
    41   then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
    42   then have "topology (openin T1) = topology (openin T2)" by simp
    43   then show "T1 = T2" unfolding openin_inverse .
    44 qed
    45 
    46 
    47 text\<open>The "universe": the union of all sets in the topology.\<close>
    48 definition "topspace T = \<Union>{S. openin T S}"
    49 
    50 subsubsection \<open>Main properties of open sets\<close>
    51 
    52 proposition openin_clauses:
    53   fixes U :: "'a topology"
    54   shows
    55     "openin U {}"
    56     "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
    57     "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
    58   using openin[of U] unfolding istopology_def mem_Collect_eq by fast+
    59 
    60 lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
    61   unfolding topspace_def by blast
    62 
    63 lemma openin_empty[simp]: "openin U {}"
    64   by (rule openin_clauses)
    65 
    66 lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
    67   by (rule openin_clauses)
    68 
    69 lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)"
    70   using openin_clauses by blast
    71 
    72 lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
    73   using openin_Union[of "{S,T}" U] by auto
    74 
    75 lemma openin_topspace[intro, simp]: "openin U (topspace U)"
    76   by (force simp: openin_Union topspace_def)
    77 
    78 lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
    79   (is "?lhs \<longleftrightarrow> ?rhs")
    80 proof
    81   assume ?lhs
    82   then show ?rhs by auto
    83 next
    84   assume H: ?rhs
    85   let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
    86   have "openin U ?t" by (force simp: openin_Union)
    87   also have "?t = S" using H by auto
    88   finally show "openin U S" .
    89 qed
    90 
    91 lemma openin_INT [intro]:
    92   assumes "finite I"
    93           "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
    94   shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
    95 using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)
    96 
    97 lemma openin_INT2 [intro]:
    98   assumes "finite I" "I \<noteq> {}"
    99           "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
   100   shows "openin T (\<Inter>i \<in> I. U i)"
   101 proof -
   102   have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
   103     using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
   104   then show ?thesis
   105     using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
   106 qed
   107 
   108 lemma openin_Inter [intro]:
   109   assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
   110   by (metis (full_types) assms openin_INT2 image_ident)
   111 
   112 lemma openin_Int_Inter:
   113   assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
   114   using openin_Inter [of "insert U \<F>"] assms by auto
   115 
   116 
   117 subsubsection \<open>Closed sets\<close>
   118 
   119 definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
   120 "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
   121 
   122 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
   123   by (metis closedin_def)
   124 
   125 lemma closedin_empty[simp]: "closedin U {}"
   126   by (simp add: closedin_def)
   127 
   128 lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
   129   by (simp add: closedin_def)
   130 
   131 lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
   132   by (auto simp: Diff_Un closedin_def)
   133 
   134 lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
   135   by auto
   136 
   137 lemma closedin_Union:
   138   assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T"
   139     shows "closedin U (\<Union>S)"
   140   using assms by induction auto
   141 
   142 lemma closedin_Inter[intro]:
   143   assumes Ke: "K \<noteq> {}"
   144     and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
   145   shows "closedin U (\<Inter>K)"
   146   using Ke Kc unfolding closedin_def Diff_Inter by auto
   147 
   148 lemma closedin_INT[intro]:
   149   assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
   150   shows "closedin U (\<Inter>x\<in>A. B x)"
   151   apply (rule closedin_Inter)
   152   using assms
   153   apply auto
   154   done
   155 
   156 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
   157   using closedin_Inter[of "{S,T}" U] by auto
   158 
   159 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
   160   apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2)
   161   apply (metis openin_subset subset_eq)
   162   done
   163 
   164 lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   165   by (simp add: openin_closedin_eq)
   166 
   167 lemma openin_diff[intro]:
   168   assumes oS: "openin U S"
   169     and cT: "closedin U T"
   170   shows "openin U (S - T)"
   171 proof -
   172   have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
   173     by (auto simp: topspace_def openin_subset)
   174   then show ?thesis using oS cT
   175     by (auto simp: closedin_def)
   176 qed
   177 
   178 lemma closedin_diff[intro]:
   179   assumes oS: "closedin U S"
   180     and cT: "openin U T"
   181   shows "closedin U (S - T)"
   182 proof -
   183   have "S - T = S \<inter> (topspace U - T)"
   184     using closedin_subset[of U S] oS cT by (auto simp: topspace_def)
   185   then show ?thesis
   186     using oS cT by (auto simp: openin_closedin_eq)
   187 qed
   188 
   189 
   190 subsection\<open>The discrete topology\<close>
   191 
   192 definition discrete_topology where "discrete_topology U \<equiv> topology (\<lambda>S. S \<subseteq> U)"
   193 
   194 lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
   195 proof -
   196   have "istopology (\<lambda>S. S \<subseteq> U)"
   197     by (auto simp: istopology_def)
   198   then show ?thesis
   199     by (simp add: discrete_topology_def topology_inverse')
   200 qed
   201 
   202 lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U"
   203   by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)
   204 
   205 lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
   206   by (simp add: closedin_def)
   207 
   208 lemma discrete_topology_unique:
   209    "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
   210 proof
   211   assume R: ?rhs
   212   then have "openin X S" if "S \<subseteq> U" for S
   213     using openin_subopen subsetD that by fastforce
   214   moreover have "x \<in> topspace X" if "openin X S" and "x \<in> S" for x S
   215     using openin_subset that by blast
   216   ultimately
   217   show ?lhs
   218     using R by (auto simp: topology_eq)
   219 qed auto
   220 
   221 lemma discrete_topology_unique_alt:
   222   "discrete_topology U = X \<longleftrightarrow> topspace X \<subseteq> U \<and> (\<forall>x \<in> U. openin X {x})"
   223   using openin_subset
   224   by (auto simp: discrete_topology_unique)
   225 
   226 lemma subtopology_eq_discrete_topology_empty:
   227    "X = discrete_topology {} \<longleftrightarrow> topspace X = {}"
   228   using discrete_topology_unique [of "{}" X] by auto
   229 
   230 lemma subtopology_eq_discrete_topology_sing:
   231    "X = discrete_topology {a} \<longleftrightarrow> topspace X = {a}"
   232   by (metis discrete_topology_unique openin_topspace singletonD)
   233 
   234 
   235 subsection \<open>Subspace topology\<close>
   236 
   237 definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
   238 "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   239 
   240 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   241   (is "istopology ?L")
   242 proof -
   243   have "?L {}" by blast
   244   {
   245     fix A B
   246     assume A: "?L A" and B: "?L B"
   247     from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V"
   248       by blast
   249     have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
   250       using Sa Sb by blast+
   251     then have "?L (A \<inter> B)" by blast
   252   }
   253   moreover
   254   {
   255     fix K
   256     assume K: "K \<subseteq> Collect ?L"
   257     have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
   258       by blast
   259     from K[unfolded th0 subset_image_iff]
   260     obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
   261       by blast
   262     have "\<Union>K = (\<Union>Sk) \<inter> V"
   263       using Sk by auto
   264     moreover have "openin U (\<Union>Sk)"
   265       using Sk by (auto simp: subset_eq)
   266     ultimately have "?L (\<Union>K)" by blast
   267   }
   268   ultimately show ?thesis
   269     unfolding subset_eq mem_Collect_eq istopology_def by auto
   270 qed
   271 
   272 lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
   273   unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
   274   by auto
   275 
   276 lemma openin_subtopology_Int:
   277    "openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
   278   using openin_subtopology by auto
   279 
   280 lemma openin_subtopology_Int2:
   281    "openin X T \<Longrightarrow> openin (subtopology X S) (S \<inter> T)"
   282   using openin_subtopology by auto
   283 
   284 lemma openin_subtopology_diff_closed:
   285    "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> openin (subtopology X S) (S - T)"
   286   unfolding closedin_def openin_subtopology
   287   by (rule_tac x="topspace X - T" in exI) auto
   288 
   289 lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
   290   by (force simp: relative_to_def openin_subtopology)
   291 
   292 lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U \<inter> V"
   293   by (auto simp: topspace_def openin_subtopology)
   294 
   295 lemma topspace_subtopology_subset:
   296    "S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
   297   by (simp add: inf.absorb_iff2 topspace_subtopology)
   298 
   299 lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
   300   unfolding closedin_def topspace_subtopology
   301   by (auto simp: openin_subtopology)
   302 
   303 lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
   304   unfolding openin_subtopology
   305   by auto (metis IntD1 in_mono openin_subset)
   306 
   307 lemma subtopology_subtopology:
   308    "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
   309 proof -
   310   have eq: "\<And>T'. (\<exists>S'. T' = S' \<inter> T \<and> (\<exists>T. openin X T \<and> S' = T \<inter> S)) = (\<exists>Sa. T' = Sa \<inter> (S \<inter> T) \<and> openin X Sa)"
   311     by (metis inf_assoc)
   312   have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
   313     by (simp add: subtopology_def)
   314   also have "\<dots> = subtopology X (S \<inter> T)"
   315     by (simp add: openin_subtopology eq) (simp add: subtopology_def)
   316   finally show ?thesis .
   317 qed
   318 
   319 lemma openin_subtopology_alt:
   320      "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
   321   by (simp add: image_iff inf_commute openin_subtopology)
   322 
   323 lemma closedin_subtopology_alt:
   324      "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
   325   by (simp add: image_iff inf_commute closedin_subtopology)
   326 
   327 lemma subtopology_superset:
   328   assumes UV: "topspace U \<subseteq> V"
   329   shows "subtopology U V = U"
   330 proof -
   331   {
   332     fix S
   333     {
   334       fix T
   335       assume T: "openin U T" "S = T \<inter> V"
   336       from T openin_subset[OF T(1)] UV have eq: "S = T"
   337         by blast
   338       have "openin U S"
   339         unfolding eq using T by blast
   340     }
   341     moreover
   342     {
   343       assume S: "openin U S"
   344       then have "\<exists>T. openin U T \<and> S = T \<inter> V"
   345         using openin_subset[OF S] UV by auto
   346     }
   347     ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
   348       by blast
   349   }
   350   then show ?thesis
   351     unfolding topology_eq openin_subtopology by blast
   352 qed
   353 
   354 lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
   355   by (simp add: subtopology_superset)
   356 
   357 lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
   358   by (simp add: subtopology_superset)
   359 
   360 lemma subtopology_restrict:
   361    "subtopology X (topspace X \<inter> S) = subtopology X S"
   362   by (metis subtopology_subtopology subtopology_topspace)
   363 
   364 lemma openin_subtopology_empty:
   365    "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
   366 by (metis Int_empty_right openin_empty openin_subtopology)
   367 
   368 lemma closedin_subtopology_empty:
   369    "closedin (subtopology U {}) S \<longleftrightarrow> S = {}"
   370 by (metis Int_empty_right closedin_empty closedin_subtopology)
   371 
   372 lemma closedin_subtopology_refl [simp]:
   373    "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
   374 by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
   375 
   376 lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
   377   by (simp add: closedin_def)
   378 
   379 lemma openin_imp_subset:
   380    "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
   381 by (metis Int_iff openin_subtopology subsetI)
   382 
   383 lemma closedin_imp_subset:
   384    "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
   385 by (simp add: closedin_def topspace_subtopology)
   386 
   387 lemma openin_open_subtopology:
   388      "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
   389   by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
   390 
   391 lemma closedin_closed_subtopology:
   392      "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
   393   by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
   394 
   395 lemma openin_subtopology_Un:
   396     "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
   397      \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
   398 by (simp add: openin_subtopology) blast
   399 
   400 lemma closedin_subtopology_Un:
   401     "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
   402      \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
   403 by (simp add: closedin_subtopology) blast
   404 
   405 lemma openin_trans_full:
   406    "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
   407   by (simp add: openin_open_subtopology)
   408 
   409 
   410 subsection \<open>The canonical topology from the underlying type class\<close>
   411 
   412 abbreviation%important euclidean :: "'a::topological_space topology"
   413   where "euclidean \<equiv> topology open"
   414 
   415 abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
   416   where "top_of_set \<equiv> subtopology (topology open)"
   417 
   418 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
   419   apply (rule cong[where x=S and y=S])
   420   apply (rule topology_inverse[symmetric])
   421   apply (auto simp: istopology_def)
   422   done
   423 
   424 declare open_openin [symmetric, simp]
   425 
   426 lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
   427   by (force simp: topspace_def)
   428 
   429 lemma topspace_euclidean_subtopology[simp]: "topspace (top_of_set S) = S"
   430   by (simp add: topspace_subtopology)
   431 
   432 lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
   433   by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
   434 
   435 declare closed_closedin [symmetric, simp]
   436 
   437 lemma openin_subtopology_self [simp]: "openin (top_of_set S) S"
   438   by (metis openin_topspace topspace_euclidean_subtopology)
   439 
   440 subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>
   441 
   442 abbreviation euclideanreal :: "real topology"
   443   where "euclideanreal \<equiv> topology open"
   444 
   445 subsection \<open>Basic "localization" results are handy for connectedness.\<close>
   446 
   447 lemma openin_open: "openin (top_of_set U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
   448   by (auto simp: openin_subtopology)
   449 
   450 lemma openin_Int_open:
   451    "\<lbrakk>openin (top_of_set U) S; open T\<rbrakk>
   452         \<Longrightarrow> openin (top_of_set U) (S \<inter> T)"
   453 by (metis open_Int Int_assoc openin_open)
   454 
   455 lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (top_of_set U) (U \<inter> S)"
   456   by (auto simp: openin_open)
   457 
   458 lemma open_openin_trans[trans]:
   459   "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (top_of_set S) T"
   460   by (metis Int_absorb1  openin_open_Int)
   461 
   462 lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (top_of_set T) S"
   463   by (auto simp: openin_open)
   464 
   465 lemma closedin_closed: "closedin (top_of_set U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
   466   by (simp add: closedin_subtopology Int_ac)
   467 
   468 lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (top_of_set U) (U \<inter> S)"
   469   by (metis closedin_closed)
   470 
   471 lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (top_of_set T) S"
   472   by (auto simp: closedin_closed)
   473 
   474 lemma closedin_closed_subset:
   475  "\<lbrakk>closedin (top_of_set U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
   476              \<Longrightarrow> closedin (top_of_set T) S"
   477   by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)
   478 
   479 lemma finite_imp_closedin:
   480   fixes S :: "'a::t1_space set"
   481   shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (top_of_set T) S"
   482     by (simp add: finite_imp_closed closed_subset)
   483 
   484 lemma closedin_singleton [simp]:
   485   fixes a :: "'a::t1_space"
   486   shows "closedin (top_of_set U) {a} \<longleftrightarrow> a \<in> U"
   487 using closedin_subset  by (force intro: closed_subset)
   488 
   489 lemma openin_euclidean_subtopology_iff:
   490   fixes S U :: "'a::metric_space set"
   491   shows "openin (top_of_set U) S \<longleftrightarrow>
   492     S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
   493   (is "?lhs \<longleftrightarrow> ?rhs")
   494 proof
   495   assume ?lhs
   496   then show ?rhs
   497     unfolding openin_open open_dist by blast
   498 next
   499   define T where "T = {x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}"
   500   have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
   501     unfolding T_def
   502     apply clarsimp
   503     apply (rule_tac x="d - dist x a" in exI)
   504     apply (clarsimp simp add: less_diff_eq)
   505     by (metis dist_commute dist_triangle_lt)
   506   assume ?rhs then have 2: "S = U \<inter> T"
   507     unfolding T_def
   508     by auto (metis dist_self)
   509   from 1 2 show ?lhs
   510     unfolding openin_open open_dist by fast
   511 qed
   512 
   513 lemma connected_openin:
   514       "connected S \<longleftrightarrow>
   515        \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
   516                  openin (top_of_set S) E2 \<and>
   517                  S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   518   apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
   519   by (simp_all, blast+)  (* SLOW *)
   520 
   521 lemma connected_openin_eq:
   522       "connected S \<longleftrightarrow>
   523        \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
   524                  openin (top_of_set S) E2 \<and>
   525                  E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   526                  E1 \<noteq> {} \<and> E2 \<noteq> {})"
   527   apply (simp add: connected_openin, safe, blast)
   528   by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
   529 
   530 lemma connected_closedin:
   531       "connected S \<longleftrightarrow>
   532        (\<nexists>E1 E2.
   533         closedin (top_of_set S) E1 \<and>
   534         closedin (top_of_set S) E2 \<and>
   535         S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   536        (is "?lhs = ?rhs")
   537 proof
   538   assume ?lhs
   539   then show ?rhs 
   540     by (auto simp add: connected_closed closedin_closed)
   541 next
   542   assume R: ?rhs
   543   then show ?lhs 
   544   proof (clarsimp simp add: connected_closed closedin_closed)
   545     fix A B 
   546     assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
   547       and disj: "A \<inter> B \<inter> S = {}"
   548       and cl: "closed A" "closed B"
   549     have "S \<inter> (A \<union> B) = S"
   550       using s_sub(1) by auto
   551     have "S - A = B \<inter> S"
   552       using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
   553     then have "S \<inter> A = {}"
   554       by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
   555     then show "A \<inter> S = {}"
   556       by blast
   557   qed
   558 qed
   559 
   560 lemma connected_closedin_eq:
   561       "connected S \<longleftrightarrow>
   562            \<not>(\<exists>E1 E2.
   563                  closedin (top_of_set S) E1 \<and>
   564                  closedin (top_of_set S) E2 \<and>
   565                  E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   566                  E1 \<noteq> {} \<and> E2 \<noteq> {})"
   567   apply (simp add: connected_closedin, safe, blast)
   568   by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
   569 
   570 text \<open>These "transitivity" results are handy too\<close>
   571 
   572 lemma openin_trans[trans]:
   573   "openin (top_of_set T) S \<Longrightarrow> openin (top_of_set U) T \<Longrightarrow>
   574     openin (top_of_set U) S"
   575   by (metis openin_Int_open openin_open)
   576 
   577 lemma openin_open_trans: "openin (top_of_set T) S \<Longrightarrow> open T \<Longrightarrow> open S"
   578   by (auto simp: openin_open intro: openin_trans)
   579 
   580 lemma closedin_trans[trans]:
   581   "closedin (top_of_set T) S \<Longrightarrow> closedin (top_of_set U) T \<Longrightarrow>
   582     closedin (top_of_set U) S"
   583   by (auto simp: closedin_closed closed_Inter Int_assoc)
   584 
   585 lemma closedin_closed_trans: "closedin (top_of_set T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   586   by (auto simp: closedin_closed intro: closedin_trans)
   587 
   588 lemma openin_subtopology_Int_subset:
   589    "\<lbrakk>openin (top_of_set u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (top_of_set v) (v \<inter> S)"
   590   by (auto simp: openin_subtopology)
   591 
   592 lemma openin_open_eq: "open s \<Longrightarrow> (openin (top_of_set s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
   593   using open_subset openin_open_trans openin_subset by fastforce
   594 
   595 
   596 subsection\<open>Derived set (set of limit points)\<close>
   597 
   598 definition derived_set_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "derived'_set'_of" 80)
   599   where "X derived_set_of S \<equiv>
   600          {x \<in> topspace X.
   601                 (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
   602 
   603 lemma derived_set_of_restrict [simp]:
   604    "X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
   605   by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
   606 
   607 lemma in_derived_set_of:
   608    "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))"
   609   by (simp add: derived_set_of_def)
   610 
   611 lemma derived_set_of_subset_topspace:
   612    "X derived_set_of S \<subseteq> topspace X"
   613   by (auto simp add: derived_set_of_def)
   614 
   615 lemma derived_set_of_subtopology:
   616    "(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
   617   by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast
   618 
   619 lemma derived_set_of_subset_subtopology:
   620    "(subtopology X S) derived_set_of T \<subseteq> S"
   621   by (simp add: derived_set_of_subtopology)
   622 
   623 lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}"
   624   by (auto simp: derived_set_of_def)
   625 
   626 lemma derived_set_of_mono:
   627    "S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
   628   unfolding derived_set_of_def by blast
   629 
   630 lemma derived_set_of_Un:
   631    "X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
   632 proof
   633   show "?lhs \<subseteq> ?rhs"
   634     apply (clarsimp simp: in_derived_set_of)
   635     by (metis IntE IntI openin_Int)
   636   show "?rhs \<subseteq> ?lhs"
   637     by (simp add: derived_set_of_mono)
   638 qed
   639 
   640 lemma derived_set_of_Union:
   641    "finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
   642 proof (induction \<F> rule: finite_induct)
   643   case (insert S \<F>)
   644   then show ?case
   645     by (simp add: derived_set_of_Un)
   646 qed auto
   647 
   648 lemma derived_set_of_topspace:
   649   "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
   650   apply (auto simp: in_derived_set_of)
   651   by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)
   652 
   653 lemma discrete_topology_unique_derived_set:
   654      "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
   655   by (auto simp: discrete_topology_unique derived_set_of_topspace)
   656 
   657 lemma subtopology_eq_discrete_topology_eq:
   658    "subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
   659   using discrete_topology_unique_derived_set [of U "subtopology X U"]
   660   by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)
   661 
   662 lemma subtopology_eq_discrete_topology:
   663    "S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
   664         \<Longrightarrow> subtopology X S = discrete_topology S"
   665   by (simp add: subtopology_eq_discrete_topology_eq)
   666 
   667 lemma subtopology_eq_discrete_topology_gen:
   668    "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
   669   by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
   670 
   671 lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
   672 proof -
   673   have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
   674     by force
   675   then show ?thesis
   676     by (simp add: subtopology_def) (simp add: discrete_topology_def)
   677 qed
   678 lemma openin_Int_derived_set_of_subset:
   679    "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
   680   by (auto simp: derived_set_of_def)
   681 
   682 lemma openin_Int_derived_set_of_eq:
   683   "openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
   684   apply auto
   685    apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
   686   by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)
   687 
   688 
   689 subsection\<open> Closure with respect to a topological space\<close>
   690 
   691 definition closure_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "closure'_of" 80)
   692   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)}"
   693 
   694 lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
   695   unfolding closure_of_def
   696   apply safe
   697   apply (meson IntI openin_subset subset_iff)
   698   by auto
   699 
   700 lemma in_closure_of:
   701    "x \<in> X closure_of S \<longleftrightarrow>
   702     x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
   703   by (auto simp: closure_of_def)
   704 
   705 lemma closure_of: "X closure_of S = topspace X \<inter> (S \<union> X derived_set_of S)"
   706   by (fastforce simp: in_closure_of in_derived_set_of)
   707 
   708 lemma closure_of_alt: "X closure_of S = topspace X \<inter> S \<union> X derived_set_of S"
   709   using derived_set_of_subset_topspace [of X S]
   710   unfolding closure_of_def in_derived_set_of
   711   by safe (auto simp: in_derived_set_of)
   712 
   713 lemma derived_set_of_subset_closure_of:
   714    "X derived_set_of S \<subseteq> X closure_of S"
   715   by (fastforce simp: closure_of_def in_derived_set_of)
   716 
   717 lemma closure_of_subtopology:
   718   "(subtopology X U) closure_of S = U \<inter> (X closure_of (U \<inter> S))"
   719   unfolding closure_of_def topspace_subtopology openin_subtopology
   720   by safe (metis (full_types) IntI Int_iff inf.commute)+
   721 
   722 lemma closure_of_empty [simp]: "X closure_of {} = {}"
   723   by (simp add: closure_of_alt)
   724 
   725 lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"
   726   by (simp add: closure_of)
   727 
   728 lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"
   729   by (simp add: closure_of)
   730 
   731 lemma closure_of_subset_topspace: "X closure_of S \<subseteq> topspace X"
   732   by (simp add: closure_of)
   733 
   734 lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T \<subseteq> S"
   735   by (simp add: closure_of_subtopology)
   736 
   737 lemma closure_of_mono: "S \<subseteq> T \<Longrightarrow> X closure_of S \<subseteq> X closure_of T"
   738   by (fastforce simp add: closure_of_def)
   739 
   740 lemma closure_of_subtopology_subset:
   741    "(subtopology X U) closure_of S \<subseteq> (X closure_of S)"
   742   unfolding closure_of_subtopology
   743   by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2)
   744 
   745 lemma closure_of_subtopology_mono:
   746    "T \<subseteq> U \<Longrightarrow> (subtopology X T) closure_of S \<subseteq> (subtopology X U) closure_of S"
   747   unfolding closure_of_subtopology
   748   by auto (meson closure_of_mono inf_mono subset_iff)
   749 
   750 lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
   751   by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_Un inf_sup_distrib1)
   752 
   753 lemma closure_of_Union:
   754    "finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
   755 by (induction \<F> rule: finite_induct) auto
   756 
   757 lemma closure_of_subset: "S \<subseteq> topspace X \<Longrightarrow> S \<subseteq> X closure_of S"
   758   by (auto simp: closure_of_def)
   759 
   760 lemma closure_of_subset_Int: "topspace X \<inter> S \<subseteq> X closure_of S"
   761   by (auto simp: closure_of_def)
   762 
   763 lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
   764 proof (cases "S \<subseteq> topspace X")
   765   case True
   766   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
   767              \<Longrightarrow> openin X (topspace X - S)"
   768     apply (subst openin_subopen, safe)
   769     by (metis DiffI subset_eq openin_subset [of X])
   770   then show ?thesis
   771     by (auto simp: closedin_def closure_of_def)
   772 next
   773   case False
   774   then show ?thesis
   775     by (simp add: closedin_def)
   776 qed
   777 
   778 lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
   779 proof (cases "S \<subseteq> topspace X")
   780   case True
   781   then show ?thesis
   782     by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
   783 next
   784   case False
   785   then show ?thesis
   786     using closure_of closure_of_subset_eq by fastforce
   787 qed
   788 
   789 lemma closedin_contains_derived_set:
   790    "closedin X S \<longleftrightarrow> X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X"
   791 proof (intro iffI conjI)
   792   show "closedin X S \<Longrightarrow> X derived_set_of S \<subseteq> S"
   793     using closure_of_eq derived_set_of_subset_closure_of by fastforce
   794   show "closedin X S \<Longrightarrow> S \<subseteq> topspace X"
   795     using closedin_subset by blast
   796   show "X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X \<Longrightarrow> closedin X S"
   797     by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
   798 qed
   799 
   800 lemma derived_set_subset_gen:
   801    "X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X (topspace X \<inter> S)"
   802   by (simp add: closedin_contains_derived_set derived_set_of_restrict derived_set_of_subset_topspace)
   803 
   804 lemma derived_set_subset: "S \<subseteq> topspace X \<Longrightarrow> (X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X S)"
   805   by (simp add: closedin_contains_derived_set)
   806 
   807 lemma closedin_derived_set:
   808      "closedin (subtopology X T) S \<longleftrightarrow>
   809       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)"
   810   by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)
   811 
   812 lemma closedin_Int_closure_of:
   813      "closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
   814   by (metis Int_left_absorb closure_of_eq closure_of_subtopology)
   815 
   816 lemma closure_of_closedin: "closedin X S \<Longrightarrow> X closure_of S = S"
   817   by (simp add: closure_of_eq)
   818 
   819 lemma closure_of_eq_diff: "X closure_of S = topspace X - \<Union>{T. openin X T \<and> disjnt S T}"
   820   by (auto simp: closure_of_def disjnt_iff)
   821 
   822 lemma closedin_closure_of [simp]: "closedin X (X closure_of S)"
   823   unfolding closure_of_eq_diff by blast
   824 
   825 lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S"
   826   by (simp add: closure_of_eq)
   827 
   828 lemma closure_of_hull:
   829   assumes "S \<subseteq> topspace X" shows "X closure_of S = (closedin X) hull S"
   830 proof (rule hull_unique [THEN sym])
   831   show "S \<subseteq> X closure_of S"
   832     by (simp add: closure_of_subset assms)
   833 next
   834   show "closedin X (X closure_of S)"
   835     by simp
   836   show "\<And>T. \<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> X closure_of S \<subseteq> T"
   837     by (metis closure_of_eq closure_of_mono)
   838 qed
   839 
   840 lemma closure_of_minimal:
   841    "\<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T"
   842   by (metis closure_of_eq closure_of_mono)
   843 
   844 lemma closure_of_minimal_eq:
   845    "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T \<longleftrightarrow> S \<subseteq> T"
   846   by (meson closure_of_minimal closure_of_subset subset_trans)
   847 
   848 lemma closure_of_unique:
   849    "\<lbrakk>S \<subseteq> T; closedin X T;
   850      \<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
   851     \<Longrightarrow> X closure_of S = T"
   852   by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)
   853 
   854 lemma closure_of_eq_empty_gen: "X closure_of S = {} \<longleftrightarrow> disjnt (topspace X) S"
   855   unfolding disjnt_def closure_of_restrict [where S=S]
   856   using closure_of by fastforce
   857 
   858 lemma closure_of_eq_empty: "S \<subseteq> topspace X \<Longrightarrow> X closure_of S = {} \<longleftrightarrow> S = {}"
   859   using closure_of_subset by fastforce
   860 
   861 lemma openin_Int_closure_of_subset:
   862   assumes "openin X S"
   863   shows "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
   864 proof -
   865   have "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
   866     by (meson assms openin_Int_derived_set_of_eq)
   867   moreover have "S \<inter> (S \<inter> T) = S \<inter> T"
   868     by fastforce
   869   ultimately show ?thesis
   870     by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1)
   871 qed
   872 
   873 lemma closure_of_openin_Int_closure_of:
   874   assumes "openin X S"
   875   shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)"
   876 proof
   877   show "X closure_of (S \<inter> X closure_of T) \<subseteq> X closure_of (S \<inter> T)"
   878     by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
   879 next
   880   show "X closure_of (S \<inter> T) \<subseteq> X closure_of (S \<inter> X closure_of T)"
   881     by (metis Int_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
   882 qed
   883 
   884 lemma openin_Int_closure_of_eq:
   885   "openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
   886   apply (rule equalityI)
   887    apply (simp add: openin_Int_closure_of_subset)
   888   by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)
   889 
   890 lemma openin_Int_closure_of_eq_empty:
   891    "openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
   892   apply (subst openin_Int_closure_of_eq, auto)
   893   by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)
   894 
   895 lemma closure_of_openin_Int_superset:
   896    "openin X S \<and> S \<subseteq> X closure_of T
   897         \<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
   898   by (metis closure_of_openin_Int_closure_of inf.orderE)
   899 
   900 lemma closure_of_openin_subtopology_Int_closure_of:
   901   assumes S: "openin (subtopology X U) S" and "T \<subseteq> U"
   902   shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
   903 proof
   904   obtain S0 where S0: "openin X S0" "S = S0 \<inter> U"
   905     using assms by (auto simp: openin_subtopology)
   906   show "?lhs \<subseteq> ?rhs"
   907   proof -
   908     have "S0 \<inter> X closure_of T = S0 \<inter> X closure_of (S0 \<inter> T)"
   909       by (meson S0(1) openin_Int_closure_of_eq)
   910     moreover have "S0 \<inter> T = S0 \<inter> U \<inter> T"
   911       using \<open>T \<subseteq> U\<close> by fastforce
   912     ultimately have "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
   913       using S0(2) by auto
   914     then show ?thesis
   915       by (meson closedin_closure_of closure_of_minimal)
   916   qed
   917 next
   918   show "?rhs \<subseteq> ?lhs"
   919   proof -
   920     have "T \<inter> S \<subseteq> T \<union> X derived_set_of T"
   921       by force
   922     then show ?thesis
   923       by (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
   924   qed
   925 qed
   926 
   927 lemma closure_of_subtopology_open:
   928      "openin X U \<or> S \<subseteq> U \<Longrightarrow> (subtopology X U) closure_of S = U \<inter> X closure_of S"
   929   by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq)
   930 
   931 lemma discrete_topology_closure_of:
   932      "(discrete_topology U) closure_of S = U \<inter> S"
   933   by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)
   934 
   935 
   936 text\<open> Interior with respect to a topological space.                             \<close>
   937 
   938 definition interior_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "interior'_of" 80)
   939   where "X interior_of S \<equiv> {x. \<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> S}"
   940 
   941 lemma interior_of_restrict:
   942    "X interior_of S = X interior_of (topspace X \<inter> S)"
   943   using openin_subset by (auto simp: interior_of_def)
   944 
   945 lemma interior_of_eq: "(X interior_of S = S) \<longleftrightarrow> openin X S"
   946   unfolding interior_of_def  using openin_subopen by blast
   947 
   948 lemma interior_of_openin: "openin X S \<Longrightarrow> X interior_of S = S"
   949   by (simp add: interior_of_eq)
   950 
   951 lemma interior_of_empty [simp]: "X interior_of {} = {}"
   952   by (simp add: interior_of_eq)
   953 
   954 lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X"
   955   by (simp add: interior_of_eq)
   956 
   957 lemma openin_interior_of [simp]: "openin X (X interior_of S)"
   958   unfolding interior_of_def
   959   using openin_subopen by fastforce
   960 
   961 lemma interior_of_interior_of [simp]:
   962    "X interior_of X interior_of S = X interior_of S"
   963   by (simp add: interior_of_eq)
   964 
   965 lemma interior_of_subset: "X interior_of S \<subseteq> S"
   966   by (auto simp: interior_of_def)
   967 
   968 lemma interior_of_subset_closure_of: "X interior_of S \<subseteq> X closure_of S"
   969   by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset)
   970 
   971 lemma subset_interior_of_eq: "S \<subseteq> X interior_of S \<longleftrightarrow> openin X S"
   972   by (metis interior_of_eq interior_of_subset subset_antisym)
   973 
   974 lemma interior_of_mono: "S \<subseteq> T \<Longrightarrow> X interior_of S \<subseteq> X interior_of T"
   975   by (auto simp: interior_of_def)
   976 
   977 lemma interior_of_maximal: "\<lbrakk>T \<subseteq> S; openin X T\<rbrakk> \<Longrightarrow> T \<subseteq> X interior_of S"
   978   by (auto simp: interior_of_def)
   979 
   980 lemma interior_of_maximal_eq: "openin X T \<Longrightarrow> T \<subseteq> X interior_of S \<longleftrightarrow> T \<subseteq> S"
   981   by (meson interior_of_maximal interior_of_subset order_trans)
   982 
   983 lemma interior_of_unique:
   984    "\<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"
   985   by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym)
   986 
   987 lemma interior_of_subset_topspace: "X interior_of S \<subseteq> topspace X"
   988   by (simp add: openin_subset)
   989 
   990 lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
   991   by (meson openin_imp_subset openin_interior_of)
   992 
   993 lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
   994   apply (rule equalityI)
   995    apply (simp add: interior_of_mono)
   996   apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
   997   done
   998 
   999 lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
  1000   by (simp add: INT_greatest Inf_lower interior_of_mono)
  1001 
  1002 lemma union_interior_of_subset:
  1003    "X interior_of S \<union> X interior_of T \<subseteq> X interior_of (S \<union> T)"
  1004   by (simp add: interior_of_mono)
  1005 
  1006 lemma interior_of_eq_empty:
  1007    "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<subseteq> S \<longrightarrow> T = {})"
  1008   by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of)
  1009 
  1010 lemma interior_of_eq_empty_alt:
  1011    "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> T - S \<noteq> {})"
  1012   by (auto simp: interior_of_eq_empty)
  1013 
  1014 lemma interior_of_Union_openin_subsets:
  1015    "\<Union>{T. openin X T \<and> T \<subseteq> S} = X interior_of S"
  1016   by (rule interior_of_unique [symmetric]) auto
  1017 
  1018 lemma interior_of_complement:
  1019    "X interior_of (topspace X - S) = topspace X - X closure_of S"
  1020   by (auto simp: interior_of_def closure_of_def)
  1021 
  1022 lemma interior_of_closure_of:
  1023    "X interior_of S = topspace X - X closure_of (topspace X - S)"
  1024   unfolding interior_of_complement [symmetric]
  1025   by (metis Diff_Diff_Int interior_of_restrict)
  1026 
  1027 lemma closure_of_interior_of:
  1028    "X closure_of S = topspace X - X interior_of (topspace X - S)"
  1029   by (simp add: interior_of_complement Diff_Diff_Int closure_of)
  1030 
  1031 lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S"
  1032   unfolding interior_of_def closure_of_def
  1033   by (blast dest: openin_subset)
  1034 
  1035 lemma interior_of_eq_empty_complement:
  1036   "X interior_of S = {} \<longleftrightarrow> X closure_of (topspace X - S) = topspace X"
  1037   using interior_of_subset_topspace [of X S] closure_of_complement by fastforce
  1038 
  1039 lemma closure_of_eq_topspace:
  1040    "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
  1041   using closure_of_subset_topspace [of X S] interior_of_complement by fastforce
  1042 
  1043 lemma interior_of_subtopology_subset:
  1044      "U \<inter> X interior_of S \<subseteq> (subtopology X U) interior_of S"
  1045   by (auto simp: interior_of_def openin_subtopology)
  1046 
  1047 lemma interior_of_subtopology_subsets:
  1048    "T \<subseteq> U \<Longrightarrow> T \<inter> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
  1049   by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)
  1050 
  1051 lemma interior_of_subtopology_mono:
  1052    "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
  1053   by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets)
  1054 
  1055 lemma interior_of_subtopology_open:
  1056   assumes "openin X U"
  1057   shows "(subtopology X U) interior_of S = U \<inter> X interior_of S"
  1058 proof -
  1059   have "\<forall>A. U \<inter> X closure_of (U \<inter> A) = U \<inter> X closure_of A"
  1060     using assms openin_Int_closure_of_eq by blast
  1061   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))"
  1062     by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
  1063   then show ?thesis
  1064     unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
  1065     using openin_Int_closure_of_eq [OF assms]
  1066     by (metis assms closure_of_subtopology_open)
  1067 qed
  1068 
  1069 lemma dense_intersects_open:
  1070    "X closure_of S = topspace X \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
  1071 proof -
  1072   have "X closure_of S = topspace X \<longleftrightarrow> (topspace X - X interior_of (topspace X - S) = topspace X)"
  1073     by (simp add: closure_of_interior_of)
  1074   also have "\<dots> \<longleftrightarrow> X interior_of (topspace X - S) = {}"
  1075     by (simp add: closure_of_complement interior_of_eq_empty_complement)
  1076   also have "\<dots> \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
  1077     unfolding interior_of_eq_empty_alt
  1078     using openin_subset by fastforce
  1079   finally show ?thesis .
  1080 qed
  1081 
  1082 lemma interior_of_closedin_union_empty_interior_of:
  1083   assumes "closedin X S" and disj: "X interior_of T = {}"
  1084   shows "X interior_of (S \<union> T) = X interior_of S"
  1085 proof -
  1086   have "X closure_of (topspace X - T) = topspace X"
  1087     by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of)
  1088   then show ?thesis
  1089     unfolding interior_of_closure_of
  1090     by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset)
  1091 qed
  1092 
  1093 lemma interior_of_union_eq_empty:
  1094    "closedin X S
  1095         \<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
  1096              X interior_of S = {} \<and> X interior_of T = {})"
  1097   by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)
  1098 
  1099 lemma discrete_topology_interior_of [simp]:
  1100     "(discrete_topology U) interior_of S = U \<inter> S"
  1101   by (simp add: interior_of_restrict [of _ S] interior_of_eq)
  1102 
  1103 
  1104 subsection \<open>Frontier with respect to topological space \<close>
  1105 
  1106 definition frontier_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "frontier'_of" 80)
  1107   where "X frontier_of S \<equiv> X closure_of S - X interior_of S"
  1108 
  1109 lemma frontier_of_closures:
  1110      "X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
  1111   by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)
  1112 
  1113 
  1114 lemma interior_of_union_frontier_of [simp]:
  1115      "X interior_of S \<union> X frontier_of S = X closure_of S"
  1116   by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)
  1117 
  1118 lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X \<inter> S)"
  1119   by (metis closure_of_restrict frontier_of_def interior_of_restrict)
  1120 
  1121 lemma closedin_frontier_of: "closedin X (X frontier_of S)"
  1122   by (simp add: closedin_Int frontier_of_closures)
  1123 
  1124 lemma frontier_of_subset_topspace: "X frontier_of S \<subseteq> topspace X"
  1125   by (simp add: closedin_frontier_of closedin_subset)
  1126 
  1127 lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T \<subseteq> S"
  1128   by (metis (no_types) closedin_derived_set closedin_frontier_of)
  1129 
  1130 lemma frontier_of_subtopology_subset:
  1131   "U \<inter> (subtopology X U) frontier_of S \<subseteq> (X frontier_of S)"
  1132 proof -
  1133   have "U \<inter> X interior_of S - subtopology X U interior_of S = {}"
  1134     by (simp add: interior_of_subtopology_subset)
  1135   moreover have "X closure_of S \<inter> subtopology X U closure_of S = subtopology X U closure_of S"
  1136     by (meson closure_of_subtopology_subset inf.absorb_iff2)
  1137   ultimately show ?thesis
  1138     unfolding frontier_of_def
  1139     by blast
  1140 qed
  1141 
  1142 lemma frontier_of_subtopology_mono:
  1143    "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X T) frontier_of S \<subseteq> (subtopology X U) frontier_of S"
  1144     by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono)
  1145 
  1146 lemma clopenin_eq_frontier_of:
  1147    "closedin X S \<and> openin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> X frontier_of S = {}"
  1148 proof (cases "S \<subseteq> topspace X")
  1149   case True
  1150   then show ?thesis
  1151     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)
  1152 next
  1153   case False
  1154   then show ?thesis
  1155     by (simp add: frontier_of_closures openin_closedin_eq)
  1156 qed
  1157 
  1158 lemma frontier_of_eq_empty:
  1159      "S \<subseteq> topspace X \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> closedin X S \<and> openin X S)"
  1160   by (simp add: clopenin_eq_frontier_of)
  1161 
  1162 lemma frontier_of_openin:
  1163      "openin X S \<Longrightarrow> X frontier_of S = X closure_of S - S"
  1164   by (metis (no_types) frontier_of_def interior_of_eq)
  1165 
  1166 lemma frontier_of_openin_straddle_Int:
  1167   assumes "openin X U" "U \<inter> X frontier_of S \<noteq> {}"
  1168   shows "U \<inter> S \<noteq> {}" "U - S \<noteq> {}"
  1169 proof -
  1170   have "U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}"
  1171     using assms by (simp add: frontier_of_closures)
  1172   then show "U \<inter> S \<noteq> {}"
  1173     using assms openin_Int_closure_of_eq_empty by fastforce
  1174   show "U - S \<noteq> {}"
  1175   proof -
  1176     have "\<exists>A. X closure_of (A - S) \<inter> U \<noteq> {}"
  1177       using \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> by blast
  1178     then have "\<not> U \<subseteq> S"
  1179       by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty)
  1180     then show ?thesis
  1181       by blast
  1182   qed
  1183 qed
  1184 
  1185 lemma frontier_of_subset_closedin: "closedin X S \<Longrightarrow> (X frontier_of S) \<subseteq> S"
  1186   using closure_of_eq frontier_of_def by fastforce
  1187 
  1188 lemma frontier_of_empty [simp]: "X frontier_of {} = {}"
  1189   by (simp add: frontier_of_def)
  1190 
  1191 lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"
  1192   by (simp add: frontier_of_def)
  1193 
  1194 lemma frontier_of_subset_eq:
  1195   assumes "S \<subseteq> topspace X"
  1196   shows "(X frontier_of S) \<subseteq> S \<longleftrightarrow> closedin X S"
  1197 proof
  1198   show "X frontier_of S \<subseteq> S \<Longrightarrow> closedin X S"
  1199     by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff)
  1200   show "closedin X S \<Longrightarrow> X frontier_of S \<subseteq> S"
  1201     by (simp add: frontier_of_subset_closedin)
  1202 qed
  1203 
  1204 lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S"
  1205   by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute)
  1206 
  1207 lemma frontier_of_disjoint_eq:
  1208   assumes "S \<subseteq> topspace X"
  1209   shows "((X frontier_of S) \<inter> S = {} \<longleftrightarrow> openin X S)"
  1210 proof
  1211   assume "X frontier_of S \<inter> S = {}"
  1212   then have "closedin X (topspace X - S)"
  1213     using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce
  1214   then show "openin X S"
  1215     using assms by (simp add: openin_closedin)
  1216 next
  1217   show "openin X S \<Longrightarrow> X frontier_of S \<inter> S = {}"
  1218     by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute)
  1219 qed
  1220 
  1221 lemma frontier_of_disjoint_eq_alt:
  1222   "S \<subseteq> (topspace X - X frontier_of S) \<longleftrightarrow> openin X S"
  1223 proof (cases "S \<subseteq> topspace X")
  1224   case True
  1225   show ?thesis
  1226     using True frontier_of_disjoint_eq by auto
  1227 next
  1228   case False
  1229   then show ?thesis
  1230     by (meson Diff_subset openin_subset subset_trans)
  1231 qed
  1232 
  1233 lemma frontier_of_Int:
  1234      "X frontier_of (S \<inter> T) =
  1235       X closure_of (S \<inter> T) \<inter> (X frontier_of S \<union> X frontier_of T)"
  1236 proof -
  1237   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"
  1238     by blast
  1239   show ?thesis
  1240     by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un)
  1241 qed
  1242 
  1243 lemma frontier_of_Int_subset: "X frontier_of (S \<inter> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
  1244   by (simp add: frontier_of_Int)
  1245 
  1246 lemma frontier_of_Int_closedin:
  1247   "\<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"
  1248   apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
  1249   using frontier_of_subset_closedin by blast
  1250 
  1251 lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
  1252   by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)
  1253 
  1254 lemma frontier_of_Union_subset:
  1255    "finite \<F> \<Longrightarrow> X frontier_of (\<Union>\<F>) \<subseteq> (\<Union>T \<in> \<F>. X frontier_of T)"
  1256 proof (induction \<F> rule: finite_induct)
  1257   case (insert A \<F>)
  1258   then show ?case
  1259     using frontier_of_Un_subset by fastforce
  1260 qed simp
  1261 
  1262 lemma frontier_of_frontier_of_subset:
  1263      "X frontier_of (X frontier_of S) \<subseteq> X frontier_of S"
  1264   by (simp add: closedin_frontier_of frontier_of_subset_closedin)
  1265 
  1266 lemma frontier_of_subtopology_open:
  1267      "openin X U \<Longrightarrow> (subtopology X U) frontier_of S = U \<inter> X frontier_of S"
  1268   by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open)
  1269 
  1270 lemma discrete_topology_frontier_of [simp]:
  1271      "(discrete_topology U) frontier_of S = {}"
  1272   by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
  1273 
  1274 
  1275 subsection\<open>Locally finite collections\<close>
  1276 
  1277 definition locally_finite_in
  1278   where
  1279  "locally_finite_in X \<A> \<longleftrightarrow>
  1280         (\<Union>\<A> \<subseteq> topspace X) \<and>
  1281         (\<forall>x \<in> topspace X. \<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}})"
  1282 
  1283 lemma finite_imp_locally_finite_in:
  1284    "\<lbrakk>finite \<A>; \<Union>\<A> \<subseteq> topspace X\<rbrakk> \<Longrightarrow> locally_finite_in X \<A>"
  1285   by (auto simp: locally_finite_in_def)
  1286 
  1287 lemma locally_finite_in_subset:
  1288   assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
  1289   shows "locally_finite_in X \<B>"
  1290 proof -
  1291   have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
  1292     apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
  1293   then show ?thesis
  1294   using assms unfolding locally_finite_in_def by (fastforce simp add:)
  1295 qed
  1296 
  1297 lemma locally_finite_in_refinement:
  1298   assumes \<A>: "locally_finite_in X \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> S"
  1299   shows "locally_finite_in X (f ` \<A>)"
  1300 proof -
  1301   show ?thesis
  1302     unfolding locally_finite_in_def
  1303   proof safe
  1304     fix x
  1305     assume "x \<in> topspace X"
  1306     then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  1307       using \<A> unfolding locally_finite_in_def by blast
  1308     moreover have "{U \<in> \<A>. f U \<inter> V \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}" for V
  1309       using f by blast
  1310     ultimately have "finite {U \<in> \<A>. f U \<inter> V \<noteq> {}}"
  1311       using finite_subset by blast
  1312     moreover have "f ` {U \<in> \<A>. f U \<inter> V \<noteq> {}} = {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
  1313       by blast
  1314     ultimately have "finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
  1315       by (metis (no_types, lifting) finite_imageI)
  1316     then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
  1317       using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
  1318   next
  1319     show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
  1320       by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
  1321   qed
  1322 qed
  1323 
  1324 lemma locally_finite_in_subtopology:
  1325   assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
  1326   shows "locally_finite_in (subtopology X S) \<A>"
  1327   unfolding locally_finite_in_def
  1328 proof safe
  1329   fix x
  1330   assume x: "x \<in> topspace (subtopology X S)"
  1331   then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  1332     using \<A> unfolding locally_finite_in_def topspace_subtopology by blast
  1333   show "\<exists>V. openin (subtopology X S) V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  1334   proof (intro exI conjI)
  1335     show "openin (subtopology X S) (S \<inter> V)"
  1336       by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
  1337     have "{U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  1338       by auto
  1339     with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
  1340       using finite_subset by auto
  1341     show "x \<in> S \<inter> V"
  1342       using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
  1343   qed
  1344 next
  1345   show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
  1346     using assms unfolding locally_finite_in_def topspace_subtopology by blast
  1347 qed
  1348 
  1349 
  1350 lemma closedin_locally_finite_Union:
  1351   assumes clo: "\<And>S. S \<in> \<A> \<Longrightarrow> closedin X S" and \<A>: "locally_finite_in X \<A>"
  1352   shows "closedin X (\<Union>\<A>)"
  1353   using \<A> unfolding locally_finite_in_def closedin_def
  1354 proof clarify
  1355   show "openin X (topspace X - \<Union>\<A>)"
  1356   proof (subst openin_subopen, clarify)
  1357     fix x
  1358     assume "x \<in> topspace X" and "x \<notin> \<Union>\<A>"
  1359     then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  1360       using \<A> unfolding locally_finite_in_def by blast
  1361     let ?T = "V - \<Union>{S \<in> \<A>. S \<inter> V \<noteq> {}}"
  1362     show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - \<Union>\<A>"
  1363     proof (intro exI conjI)
  1364       show "openin X ?T"
  1365         by (metis (no_types, lifting) fin \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
  1366       show "x \<in> ?T"
  1367         using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
  1368       show "?T \<subseteq> topspace X - \<Union>\<A>"
  1369         using \<open>openin X V\<close> openin_subset by auto
  1370     qed
  1371   qed
  1372 qed
  1373 
  1374 lemma locally_finite_in_closure:
  1375   assumes \<A>: "locally_finite_in X \<A>"
  1376   shows "locally_finite_in X ((\<lambda>S. X closure_of S) ` \<A>)"
  1377   using \<A> unfolding locally_finite_in_def
  1378 proof (intro conjI; clarsimp)
  1379   fix x A
  1380   assume "x \<in> X closure_of A"
  1381   then show "x \<in> topspace X"
  1382     by (meson in_closure_of)
  1383 next
  1384   fix x
  1385   assume "x \<in> topspace X" and "\<Union>\<A> \<subseteq> topspace X"
  1386   then obtain V where V: "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  1387     using \<A> unfolding locally_finite_in_def by blast
  1388   have eq: "{y \<in> f ` \<A>. Q y} = f ` {x. x \<in> \<A> \<and> Q(f x)}" for f Q
  1389     by blast
  1390   have eq2: "{A \<in> \<A>. X closure_of A \<inter> V \<noteq> {}} = {A \<in> \<A>. A \<inter> V \<noteq> {}}"
  1391     using openin_Int_closure_of_eq_empty V  by blast
  1392   have "finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
  1393     by (simp add: eq eq2 fin)
  1394   with V show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
  1395     by blast
  1396 qed
  1397 
  1398 lemma closedin_Union_locally_finite_closure:
  1399    "locally_finite_in X \<A> \<Longrightarrow> closedin X (\<Union>((\<lambda>S. X closure_of S) ` \<A>))"
  1400   by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
  1401 
  1402 lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
  1403   by clarify (meson Union_upper closure_of_mono subsetD)
  1404 
  1405 lemma closure_of_locally_finite_Union:
  1406    "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
  1407   apply (rule closure_of_unique)
  1408   apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
  1409   apply (simp add: closedin_Union_locally_finite_closure)
  1410   by (simp add: Sup_le_iff closure_of_minimal)
  1411 
  1412 
  1413 subsection%important \<open>Continuous maps\<close>
  1414 
  1415 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
  1416 of type classes, as defined below.\<close>
  1417 
  1418 definition continuous_map where
  1419   "continuous_map X Y f \<equiv>
  1420      (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
  1421      (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
  1422 
  1423 lemma continuous_map:
  1424    "continuous_map X Y f \<longleftrightarrow>
  1425         f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
  1426   by (auto simp: continuous_map_def)
  1427 
  1428 lemma continuous_map_image_subset_topspace:
  1429    "continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
  1430   by (auto simp: continuous_map_def)
  1431 
  1432 lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
  1433   by (auto simp: continuous_map_def)
  1434 
  1435 lemma continuous_map_closedin:
  1436    "continuous_map X Y f \<longleftrightarrow>
  1437          (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
  1438          (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
  1439 proof -
  1440   have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
  1441         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
  1442     if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
  1443   proof -
  1444     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
  1445       using that by blast
  1446     show ?thesis
  1447     proof (intro iffI allI impI)
  1448       fix C
  1449       assume "\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}" and "closedin Y C"
  1450       then have "openin X {x \<in> topspace X. f x \<in> topspace Y - C}" by blast
  1451       then show "closedin X {x \<in> topspace X. f x \<in> C}"
  1452         by (auto simp add: closedin_def eq)
  1453     next
  1454       fix U
  1455       assume "\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}" and "openin Y U"
  1456       then have "closedin X {x \<in> topspace X. f x \<in> topspace Y - U}" by blast
  1457       then show "openin X {x \<in> topspace X. f x \<in> U}"
  1458         by (auto simp add: openin_closedin_eq eq)
  1459     qed
  1460   qed
  1461   then show ?thesis
  1462     by (auto simp: continuous_map_def)
  1463 qed
  1464 
  1465 lemma openin_continuous_map_preimage:
  1466    "\<lbrakk>continuous_map X Y f; openin Y U\<rbrakk> \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
  1467   by (simp add: continuous_map_def)
  1468 
  1469 lemma closedin_continuous_map_preimage:
  1470    "\<lbrakk>continuous_map X Y f; closedin Y C\<rbrakk> \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}"
  1471   by (simp add: continuous_map_closedin)
  1472 
  1473 lemma openin_continuous_map_preimage_gen:
  1474   assumes "continuous_map X Y f" "openin X U" "openin Y V"
  1475   shows "openin X {x \<in> U. f x \<in> V}"
  1476 proof -
  1477   have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
  1478     using assms(2) openin_closedin_eq by fastforce
  1479   show ?thesis
  1480     unfolding eq
  1481     using assms openin_continuous_map_preimage by fastforce
  1482 qed
  1483 
  1484 lemma closedin_continuous_map_preimage_gen:
  1485   assumes "continuous_map X Y f" "closedin X U" "closedin Y V"
  1486   shows "closedin X {x \<in> U. f x \<in> V}"
  1487 proof -
  1488   have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
  1489     using assms(2) closedin_def by fastforce
  1490   show ?thesis
  1491     unfolding eq
  1492     using assms closedin_continuous_map_preimage by fastforce
  1493 qed
  1494 
  1495 lemma continuous_map_image_closure_subset:
  1496   assumes "continuous_map X Y f"
  1497   shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
  1498 proof -
  1499   have *: "f ` (topspace X) \<subseteq> topspace Y"
  1500     by (meson assms continuous_map)
  1501   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
  1502   proof (rule closure_of_minimal)
  1503     show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
  1504       using closure_of_subset * that  by (fastforce simp: in_closure_of)
  1505   next
  1506     show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
  1507       using assms closedin_continuous_map_preimage_gen by fastforce
  1508   qed
  1509   then have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (f ` (topspace X \<inter> S))"
  1510     by blast
  1511   also have "\<dots> \<subseteq> Y closure_of (topspace Y \<inter> f ` S)"
  1512     using * by (blast intro!: closure_of_mono)
  1513   finally have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (topspace Y \<inter> f ` S)" .
  1514   then show ?thesis
  1515     by (metis closure_of_restrict)
  1516 qed
  1517 
  1518 lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
  1519        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  1520   using continuous_map_image_closure_subset by blast
  1521 
  1522 lemma continuous_map_subset_aux2:
  1523   assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
  1524   shows "continuous_map X Y f"
  1525   unfolding continuous_map_closedin
  1526 proof (intro conjI ballI allI impI)
  1527   fix x
  1528   assume "x \<in> topspace X"
  1529   then show "f x \<in> topspace Y"
  1530     using assms closure_of_subset_topspace by fastforce
  1531 next
  1532   fix C
  1533   assume "closedin Y C"
  1534   then show "closedin X {x \<in> topspace X. f x \<in> C}"
  1535   proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
  1536     fix x
  1537     assume x: "x \<in> X closure_of {x \<in> topspace X. f x \<in> C}"
  1538       and "C \<subseteq> topspace Y" and "Y closure_of C \<subseteq> C"
  1539     show "x \<in> topspace X"
  1540       by (meson x in_closure_of)
  1541     have "{a \<in> topspace X. f a \<in> C} \<subseteq> topspace X"
  1542       by simp
  1543     moreover have "Y closure_of f ` {a \<in> topspace X. f a \<in> C} \<subseteq> C"
  1544       by (simp add: \<open>closedin Y C\<close> closure_of_minimal image_subset_iff)
  1545     ultimately have "f ` (X closure_of {a \<in> topspace X. f a \<in> C}) \<subseteq> C"
  1546       using assms by blast
  1547     then show "f x \<in> C"
  1548       using x by auto
  1549   qed
  1550 qed
  1551 
  1552 lemma continuous_map_eq_image_closure_subset:
  1553      "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  1554   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
  1555 
  1556 lemma continuous_map_eq_image_closure_subset_alt:
  1557      "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  1558   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
  1559 
  1560 lemma continuous_map_eq_image_closure_subset_gen:
  1561      "continuous_map X Y f \<longleftrightarrow>
  1562         f ` (topspace X) \<subseteq> topspace Y \<and>
  1563         (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  1564   using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
  1565 
  1566 lemma continuous_map_closure_preimage_subset:
  1567    "continuous_map X Y f
  1568         \<Longrightarrow> X closure_of {x \<in> topspace X. f x \<in> T}
  1569             \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
  1570   unfolding continuous_map_closedin
  1571   by (rule closure_of_minimal) (use in_closure_of in \<open>fastforce+\<close>)
  1572 
  1573 
  1574 lemma continuous_map_frontier_frontier_preimage_subset:
  1575   assumes "continuous_map X Y f"
  1576   shows "X frontier_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y frontier_of T}"
  1577 proof -
  1578   have eq: "topspace X - {x \<in> topspace X. f x \<in> T} = {x \<in> topspace X. f x \<in> topspace Y - T}"
  1579     using assms unfolding continuous_map_def by blast
  1580   have "X closure_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
  1581     by (simp add: assms continuous_map_closure_preimage_subset)
  1582   moreover
  1583   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)}"
  1584     using continuous_map_closure_preimage_subset [OF assms] eq by presburger
  1585   ultimately show ?thesis
  1586     by (auto simp: frontier_of_closures)
  1587 qed
  1588 
  1589 lemma topology_finer_continuous_id:
  1590   "topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
  1591   unfolding continuous_map_def
  1592   apply auto
  1593   using openin_subopen openin_subset apply fastforce
  1594   using openin_subopen topspace_def by fastforce
  1595 
  1596 lemma continuous_map_const [simp]:
  1597    "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
  1598 proof (cases "topspace X = {}")
  1599   case False
  1600   show ?thesis
  1601   proof (cases "C \<in> topspace Y")
  1602     case True
  1603     with openin_subopen show ?thesis
  1604       by (auto simp: continuous_map_def)
  1605   next
  1606     case False
  1607     then show ?thesis
  1608       unfolding continuous_map_def by fastforce
  1609   qed
  1610 qed (auto simp: continuous_map_on_empty)
  1611 
  1612 lemma continuous_map_compose:
  1613   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
  1614   shows "continuous_map X X'' (g \<circ> f)"
  1615   unfolding continuous_map_def
  1616 proof (intro conjI ballI allI impI)
  1617   fix x
  1618   assume "x \<in> topspace X"
  1619   then show "(g \<circ> f) x \<in> topspace X''"
  1620     using assms unfolding continuous_map_def by force
  1621 next
  1622   fix U
  1623   assume "openin X'' U"
  1624   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}}"
  1625     by auto (meson f continuous_map_def)
  1626   show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
  1627     unfolding eq
  1628     using assms unfolding continuous_map_def
  1629     using \<open>openin X'' U\<close> by blast
  1630 qed
  1631 
  1632 lemma continuous_map_eq:
  1633   assumes "continuous_map X X' f" and "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x" shows "continuous_map X X' g"
  1634 proof -
  1635   have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
  1636     using assms by auto
  1637   show ?thesis
  1638     using assms by (simp add: continuous_map_def eq)
  1639 qed
  1640 
  1641 lemma restrict_continuous_map [simp]:
  1642      "topspace X \<subseteq> S \<Longrightarrow> continuous_map X X' (restrict f S) \<longleftrightarrow> continuous_map X X' f"
  1643   by (auto simp: elim!: continuous_map_eq)
  1644 
  1645 lemma continuous_map_in_subtopology:
  1646   "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
  1647   (is "?lhs = ?rhs")
  1648 proof
  1649   assume L: ?lhs
  1650   show ?rhs
  1651   proof -
  1652     have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
  1653       by (meson L continuous_map_image_closure_subset)
  1654     then show ?thesis
  1655       by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset dual_order.trans)
  1656   qed
  1657 next
  1658   assume R: ?rhs
  1659   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
  1660     by auto
  1661   show ?lhs
  1662     using R
  1663     unfolding continuous_map
  1664     by (auto simp: topspace_subtopology openin_subtopology eq)
  1665 qed
  1666 
  1667 
  1668 lemma continuous_map_from_subtopology:
  1669      "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
  1670   by (auto simp: continuous_map topspace_subtopology openin_subtopology)
  1671 
  1672 lemma continuous_map_into_fulltopology:
  1673    "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
  1674   by (auto simp: continuous_map_in_subtopology)
  1675 
  1676 lemma continuous_map_into_subtopology:
  1677    "\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
  1678   by (auto simp: continuous_map_in_subtopology)
  1679 
  1680 lemma continuous_map_from_subtopology_mono:
  1681      "\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
  1682       \<Longrightarrow> continuous_map (subtopology X S) X' f"
  1683   by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)
  1684 
  1685 lemma continuous_map_from_discrete_topology [simp]:
  1686   "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
  1687   by (auto simp: continuous_map_def)
  1688 
  1689 lemma continuous_map_iff_continuous [simp]: "continuous_map (subtopology euclidean S) euclidean g = continuous_on S g"
  1690   by (fastforce simp add: continuous_map openin_subtopology continuous_on_open_invariant)
  1691 
  1692 lemma continuous_map_iff_continuous2 [simp]: "continuous_map euclidean euclidean g = continuous_on UNIV g"
  1693   by (metis continuous_map_iff_continuous subtopology_UNIV)
  1694 
  1695 lemma continuous_map_openin_preimage_eq:
  1696    "continuous_map X Y f \<longleftrightarrow>
  1697         f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
  1698   by (auto simp: continuous_map_def vimage_def Int_def)
  1699 
  1700 lemma continuous_map_closedin_preimage_eq:
  1701    "continuous_map X Y f \<longleftrightarrow>
  1702         f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
  1703   by (auto simp: continuous_map_closedin vimage_def Int_def)
  1704 
  1705 lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt"
  1706   by (simp add: continuous_at_imp_continuous_on isCont_real_sqrt)
  1707 
  1708 lemma continuous_map_sqrt [continuous_intros]:
  1709    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
  1710   by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)
  1711 
  1712 lemma continuous_map_id [simp]: "continuous_map X X id"
  1713   unfolding continuous_map_def  using openin_subopen topspace_def by fastforce
  1714 
  1715 declare continuous_map_id [unfolded id_def, simp]
  1716 
  1717 lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id"
  1718   by (simp add: continuous_map_from_subtopology)
  1719 
  1720 declare continuous_map_id_subt [unfolded id_def, simp]
  1721 
  1722 
  1723 lemma%important continuous_map_alt:
  1724    "continuous_map T1 T2 f 
  1725     = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
  1726   by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
  1727 
  1728 lemma continuous_map_open [intro]:
  1729   "continuous_map T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
  1730   unfolding continuous_map_alt by auto
  1731 
  1732 lemma continuous_map_preimage_topspace [intro]:
  1733   assumes "continuous_map T1 T2 f"
  1734   shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
  1735 using assms unfolding continuous_map_def by auto
  1736 
  1737 
  1738 
  1739 subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
  1740 
  1741 definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  1742   where "open_map X1 X2 f \<equiv> \<forall>U. openin X1 U \<longrightarrow> openin X2 (f ` U)"
  1743 
  1744 definition closed_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  1745   where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"
  1746 
  1747 lemma open_map_imp_subset_topspace:
  1748      "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
  1749   unfolding open_map_def by (simp add: openin_subset)
  1750 
  1751 lemma open_map_imp_subset:
  1752     "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
  1753   by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
  1754 
  1755 lemma topology_finer_open_id:
  1756      "(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
  1757   unfolding open_map_def by auto
  1758 
  1759 lemma open_map_id: "open_map X X id"
  1760   unfolding open_map_def by auto
  1761 
  1762 lemma open_map_eq:
  1763      "\<lbrakk>open_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> open_map X X' g"
  1764   unfolding open_map_def
  1765   by (metis image_cong openin_subset subset_iff)
  1766 
  1767 lemma open_map_inclusion_eq:
  1768   "open_map (subtopology X S) X id \<longleftrightarrow> openin X (topspace X \<inter> S)"
  1769 proof -
  1770   have *: "openin X (T \<inter> S)" if "openin X (S \<inter> topspace X)" "openin X T" for T
  1771   proof -
  1772     have "T \<subseteq> topspace X"
  1773       using that by (simp add: openin_subset)
  1774     with that show "openin X (T \<inter> S)"
  1775       by (metis inf.absorb1 inf.left_commute inf_commute openin_Int)
  1776   qed
  1777   show ?thesis
  1778     by (fastforce simp add: open_map_def Int_commute openin_subtopology_alt intro: *)
  1779 qed
  1780 
  1781 lemma open_map_inclusion:
  1782      "openin X S \<Longrightarrow> open_map (subtopology X S) X id"
  1783   by (simp add: open_map_inclusion_eq openin_Int)
  1784 
  1785 lemma open_map_compose:
  1786      "\<lbrakk>open_map X X' f; open_map X' X'' g\<rbrakk> \<Longrightarrow> open_map X X'' (g \<circ> f)"
  1787   by (metis (no_types, lifting) image_comp open_map_def)
  1788 
  1789 lemma closed_map_imp_subset_topspace:
  1790      "closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
  1791   by (simp add: closed_map_def closedin_subset)
  1792 
  1793 lemma closed_map_imp_subset:
  1794      "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
  1795   using closed_map_imp_subset_topspace by blast
  1796 
  1797 lemma topology_finer_closed_id:
  1798     "(\<forall>S. closedin X S \<longrightarrow> closedin X' S) \<longleftrightarrow> closed_map X X' id"
  1799   by (simp add: closed_map_def)
  1800 
  1801 lemma closed_map_id: "closed_map X X id"
  1802   by (simp add: closed_map_def)
  1803 
  1804 lemma closed_map_eq:
  1805    "\<lbrakk>closed_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> closed_map X X' g"
  1806   unfolding closed_map_def
  1807   by (metis image_cong closedin_subset subset_iff)
  1808 
  1809 lemma closed_map_compose:
  1810     "\<lbrakk>closed_map X X' f; closed_map X' X'' g\<rbrakk> \<Longrightarrow> closed_map X X'' (g \<circ> f)"
  1811   by (metis (no_types, lifting) closed_map_def image_comp)
  1812 
  1813 lemma closed_map_inclusion_eq:
  1814    "closed_map (subtopology X S) X id \<longleftrightarrow>
  1815         closedin X (topspace X \<inter> S)"
  1816 proof -
  1817   have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
  1818   proof -
  1819     have "T \<subseteq> topspace X"
  1820       using that by (simp add: closedin_subset)
  1821     with that show "closedin X (T \<inter> S)"
  1822       by (metis inf.absorb1 inf.left_commute inf_commute closedin_Int)
  1823   qed
  1824   show ?thesis
  1825     by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *)
  1826 qed
  1827 
  1828 lemma closed_map_inclusion: "closedin X S \<Longrightarrow> closed_map (subtopology X S) X id"
  1829   by (simp add: closed_map_inclusion_eq closedin_Int)
  1830 
  1831 lemma open_map_into_subtopology:
  1832     "\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
  1833   unfolding open_map_def openin_subtopology
  1834   using openin_subset by fastforce
  1835 
  1836 lemma closed_map_into_subtopology:
  1837     "\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
  1838   unfolding closed_map_def closedin_subtopology
  1839   using closedin_subset by fastforce
  1840 
  1841 lemma open_map_into_discrete_topology:
  1842     "open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
  1843   unfolding open_map_def openin_discrete_topology using openin_subset by blast
  1844 
  1845 lemma closed_map_into_discrete_topology:
  1846     "closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
  1847   unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast
  1848 
  1849 lemma bijective_open_imp_closed_map:
  1850      "\<lbrakk>open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> closed_map X X' f"
  1851   unfolding open_map_def closed_map_def closedin_def
  1852   by auto (metis Diff_subset inj_on_image_set_diff)
  1853 
  1854 lemma bijective_closed_imp_open_map:
  1855      "\<lbrakk>closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> open_map X X' f"
  1856   unfolding closed_map_def open_map_def openin_closedin_eq
  1857   by auto (metis Diff_subset inj_on_image_set_diff)
  1858 
  1859 lemma open_map_from_subtopology:
  1860      "\<lbrakk>open_map X X' f; openin X U\<rbrakk> \<Longrightarrow> open_map (subtopology X U) X' f"
  1861   unfolding open_map_def openin_subtopology_alt by blast
  1862 
  1863 lemma closed_map_from_subtopology:
  1864      "\<lbrakk>closed_map X X' f; closedin X U\<rbrakk> \<Longrightarrow> closed_map (subtopology X U) X' f"
  1865   unfolding closed_map_def closedin_subtopology_alt by blast
  1866 
  1867 lemma open_map_restriction:
  1868      "\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
  1869       \<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
  1870   unfolding open_map_def openin_subtopology_alt
  1871   apply clarify
  1872   apply (rename_tac T)
  1873   apply (rule_tac x="f ` T" in image_eqI)
  1874   using openin_closedin_eq by fastforce+
  1875 
  1876 lemma closed_map_restriction:
  1877      "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
  1878       \<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
  1879   unfolding closed_map_def closedin_subtopology_alt
  1880   apply clarify
  1881   apply (rename_tac T)
  1882   apply (rule_tac x="f ` T" in image_eqI)
  1883   using closedin_def by fastforce+
  1884 
  1885 subsection\<open>Quotient maps\<close>
  1886                                       
  1887 definition quotient_map where
  1888  "quotient_map X X' f \<longleftrightarrow>
  1889         f ` (topspace X) = topspace X' \<and>
  1890         (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (openin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> openin X' U))"
  1891 
  1892 lemma quotient_map_eq:
  1893   assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
  1894   shows "quotient_map X X' g"
  1895 proof -
  1896   have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
  1897     using assms by auto
  1898   show ?thesis
  1899   using assms
  1900   unfolding quotient_map_def
  1901   by (metis (mono_tags, lifting) eq image_cong)
  1902 qed
  1903 
  1904 lemma quotient_map_compose:
  1905   assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
  1906   shows "quotient_map X X'' (g \<circ> f)"
  1907   unfolding quotient_map_def
  1908 proof (intro conjI allI impI)
  1909   show "(g \<circ> f) ` topspace X = topspace X''"
  1910     using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def)
  1911 next
  1912   fix U''
  1913   assume "U'' \<subseteq> topspace X''"
  1914   define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}"
  1915   have "U' \<subseteq> topspace X'"
  1916     by (auto simp add: U'_def)
  1917   then have U': "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
  1918     using assms unfolding quotient_map_def by simp
  1919   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''}"
  1920     using f quotient_map_def by fastforce
  1921   have "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X {x \<in> topspace X. f x \<in> U'}"
  1922     using assms  by (simp add: quotient_map_def U'_def eq)
  1923   also have "\<dots> = openin X'' U''"
  1924     using U'_def \<open>U'' \<subseteq> topspace X''\<close> U' g quotient_map_def by fastforce
  1925   finally show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X'' U''" .
  1926 qed
  1927 
  1928 lemma quotient_map_from_composition:
  1929   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \<circ> f)"
  1930   shows  "quotient_map X' X'' g"
  1931   unfolding quotient_map_def
  1932 proof (intro conjI allI impI)
  1933   show "g ` topspace X' = topspace X''"
  1934     using assms unfolding continuous_map_def quotient_map_def by fastforce
  1935 next
  1936   fix U'' :: "'c set"
  1937   assume U'': "U'' \<subseteq> topspace X''"
  1938   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''}}"
  1939     using continuous_map_def f by fastforce
  1940   show "openin X' {x \<in> topspace X'. g x \<in> U''} = openin X'' U''"
  1941     using assms unfolding continuous_map_def quotient_map_def
  1942     by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq)
  1943 qed
  1944 
  1945 lemma quotient_imp_continuous_map:
  1946     "quotient_map X X' f \<Longrightarrow> continuous_map X X' f"
  1947   by (simp add: continuous_map openin_subset quotient_map_def)
  1948 
  1949 lemma quotient_imp_surjective_map:
  1950     "quotient_map X X' f \<Longrightarrow> f ` (topspace X) = topspace X'"
  1951   by (simp add: quotient_map_def)
  1952 
  1953 lemma quotient_map_closedin:
  1954   "quotient_map X X' f \<longleftrightarrow>
  1955         f ` (topspace X) = topspace X' \<and>
  1956         (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (closedin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> closedin X' U))"
  1957 proof -
  1958   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'}"
  1959     if "f ` topspace X = topspace X'" "U' \<subseteq> topspace X'" for U'
  1960       using that by auto
  1961   have "(\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U) =
  1962           (\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U)"
  1963     if "f ` topspace X = topspace X'"
  1964   proof (rule iffI; intro allI impI subsetI)
  1965     fix U'
  1966     assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
  1967       and U': "U' \<subseteq> topspace X'"
  1968     show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
  1969       using U'  by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
  1970   next
  1971     fix U' :: "'b set"
  1972     assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
  1973       and U': "U' \<subseteq> topspace X'"
  1974     show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
  1975       using U'  by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
  1976   qed
  1977   then show ?thesis
  1978     unfolding quotient_map_def by force
  1979 qed
  1980 
  1981 lemma continuous_open_imp_quotient_map:
  1982   assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
  1983   shows "quotient_map X X' f"
  1984 proof -
  1985   { fix U
  1986     assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
  1987     then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
  1988       using om unfolding open_map_def by blast
  1989     then have "openin X' U"
  1990       using U feq by (subst openin_subopen) force
  1991   }
  1992   moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
  1993     using that assms unfolding continuous_map_def by blast
  1994   ultimately show ?thesis
  1995     unfolding quotient_map_def using assms by blast
  1996 qed
  1997 
  1998 lemma continuous_closed_imp_quotient_map:
  1999   assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'"
  2000   shows "quotient_map X X' f"
  2001 proof -
  2002   have "f ` {x \<in> topspace X. f x \<in> U} = U" if "U \<subseteq> topspace X'" for U
  2003     using that feq by auto
  2004   with assms show ?thesis
  2005     unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto
  2006 qed
  2007 
  2008 lemma continuous_open_quotient_map:
  2009    "\<lbrakk>continuous_map X X' f; open_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
  2010   by (meson continuous_open_imp_quotient_map quotient_map_def)
  2011 
  2012 lemma continuous_closed_quotient_map:
  2013      "\<lbrakk>continuous_map X X' f; closed_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
  2014   by (meson continuous_closed_imp_quotient_map quotient_map_def)
  2015 
  2016 lemma injective_quotient_map:
  2017   assumes "inj_on f (topspace X)"
  2018   shows "quotient_map X X' f \<longleftrightarrow>
  2019          continuous_map X X' f \<and> open_map X X' f \<and> closed_map X X' f \<and> f ` (topspace X) = topspace X'"
  2020          (is "?lhs = ?rhs")
  2021 proof
  2022   assume L: ?lhs
  2023   have "open_map X X' f"
  2024   proof (clarsimp simp add: open_map_def)
  2025     fix U
  2026     assume "openin X U"
  2027     then have "U \<subseteq> topspace X"
  2028       by (simp add: openin_subset)
  2029     moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
  2030       using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
  2031     ultimately show "openin X' (f ` U)"
  2032       using L unfolding quotient_map_def
  2033       by (metis (no_types, lifting) Collect_cong \<open>openin X U\<close> image_mono)
  2034   qed
  2035   moreover have "closed_map X X' f"
  2036   proof (clarsimp simp add: closed_map_def)
  2037     fix U
  2038     assume "closedin X U"
  2039     then have "U \<subseteq> topspace X"
  2040       by (simp add: closedin_subset)
  2041     moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
  2042       using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
  2043     ultimately show "closedin X' (f ` U)"
  2044       using L unfolding quotient_map_closedin
  2045       by (metis (no_types, lifting) Collect_cong \<open>closedin X U\<close> image_mono)
  2046   qed
  2047   ultimately show ?rhs
  2048     using L by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
  2049 next
  2050   assume ?rhs
  2051   then show ?lhs
  2052     by (simp add: continuous_closed_imp_quotient_map)
  2053 qed
  2054 
  2055 lemma continuous_compose_quotient_map:
  2056   assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
  2057   shows "continuous_map X' X'' g"
  2058   unfolding quotient_map_def continuous_map_def
  2059 proof (intro conjI ballI allI impI)
  2060   show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
  2061     using assms unfolding quotient_map_def
  2062     by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
  2063 next
  2064   fix U'' :: "'c set"
  2065   assume U'': "openin X'' U''"
  2066   have "f ` topspace X = topspace X'"
  2067     by (simp add: f quotient_imp_surjective_map)
  2068   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
  2069     by auto
  2070   have "openin X {x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''}"
  2071     unfolding eq using U'' g openin_continuous_map_preimage by fastforce
  2072   then have *: "openin X {x \<in> topspace X. f x \<in> {x \<in> topspace X'. g x \<in> U''}}"
  2073     by auto
  2074   show "openin X' {x \<in> topspace X'. g x \<in> U''}"
  2075     using f unfolding quotient_map_def
  2076     by (metis (no_types) Collect_subset *)
  2077 qed
  2078 
  2079 lemma continuous_compose_quotient_map_eq:
  2080    "quotient_map X X' f \<Longrightarrow> continuous_map X X'' (g \<circ> f) \<longleftrightarrow> continuous_map X' X'' g"
  2081   using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast
  2082 
  2083 lemma quotient_map_compose_eq:
  2084    "quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
  2085   apply safe
  2086   apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
  2087   by (simp add: quotient_map_compose)
  2088 
  2089 lemma quotient_map_restriction:
  2090   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"
  2091  shows "quotient_map (subtopology X U) (subtopology Y V) f"
  2092   using disj
  2093 proof
  2094   assume V: "openin Y V"
  2095   with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
  2096     by (auto simp: openin_subset)
  2097   have fim: "f ` topspace X = topspace Y"
  2098      and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
  2099     using quo unfolding quotient_map_def by auto
  2100   have "openin X U"
  2101     using U V Y sub(2) by blast
  2102   show ?thesis
  2103     unfolding quotient_map_def
  2104   proof (intro conjI allI impI)
  2105     show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
  2106       using sub U fim by (auto simp: topspace_subtopology)
  2107   next
  2108     fix Y' :: "'b set"
  2109     assume "Y' \<subseteq> topspace (subtopology Y V)"
  2110     then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
  2111       by (simp_all add: topspace_subtopology)
  2112     then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
  2113       using U by blast
  2114     then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
  2115       using U V Y \<open>openin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
  2116       by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
  2117   qed
  2118 next
  2119   assume V: "closedin Y V"
  2120   with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
  2121     by (auto simp: closedin_subset)
  2122   have fim: "f ` topspace X = topspace Y"
  2123      and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U} = closedin Y U"
  2124     using quo unfolding quotient_map_closedin by auto
  2125   have "closedin X U"
  2126     using U V Y sub(2) by blast
  2127   show ?thesis
  2128     unfolding quotient_map_closedin
  2129   proof (intro conjI allI impI)
  2130     show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
  2131       using sub U fim by (auto simp: topspace_subtopology)
  2132   next
  2133     fix Y' :: "'b set"
  2134     assume "Y' \<subseteq> topspace (subtopology Y V)"
  2135     then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
  2136       by (simp_all add: topspace_subtopology)
  2137     then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
  2138       using U by blast
  2139     then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
  2140       using U V Y \<open>closedin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
  2141       by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
  2142   qed
  2143 qed
  2144 
  2145 lemma quotient_map_saturated_open:
  2146      "quotient_map X Y f \<longleftrightarrow>
  2147         continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
  2148         (\<forall>U. openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> openin Y (f ` U))"
  2149      (is "?lhs = ?rhs")
  2150 proof
  2151   assume L: ?lhs
  2152   then have fim: "f ` topspace X = topspace Y"
  2153     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin Y U = openin X {x \<in> topspace X. f x \<in> U}"
  2154     unfolding quotient_map_def by auto
  2155   show ?rhs
  2156   proof (intro conjI allI impI)
  2157     show "continuous_map X Y f"
  2158       by (simp add: L quotient_imp_continuous_map)
  2159     show "f ` topspace X = topspace Y"
  2160       by (simp add: fim)
  2161   next
  2162     fix U :: "'a set"
  2163     assume U: "openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
  2164     then have sub:  "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
  2165       using fim openin_subset by fastforce+
  2166     show "openin Y (f ` U)"
  2167       by (simp add: sub Y eq U)
  2168   qed
  2169 next
  2170   assume ?rhs
  2171   then have YX: "\<And>U. openin Y U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
  2172        and fim: "f ` topspace X = topspace Y"
  2173        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)"
  2174     by (auto simp: quotient_map_def continuous_map_def)
  2175   show ?lhs
  2176   proof (simp add: quotient_map_def fim, intro allI impI iffI)
  2177     fix U :: "'b set"
  2178     assume "U \<subseteq> topspace Y" and X: "openin X {x \<in> topspace X. f x \<in> U}"
  2179     have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
  2180       using \<open>U \<subseteq> topspace Y\<close> fim by auto
  2181     show "openin Y U"
  2182       using XY [OF X] by (simp add: feq)
  2183   next
  2184     fix U :: "'b set"
  2185     assume "U \<subseteq> topspace Y" and Y: "openin Y U"
  2186     show "openin X {x \<in> topspace X. f x \<in> U}"
  2187       by (metis YX [OF Y])
  2188   qed
  2189 qed
  2190 
  2191 subsection\<open> Separated Sets\<close>
  2192 
  2193 definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
  2194   where "separatedin X S T \<equiv>
  2195            S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
  2196            S \<inter> X closure_of T = {} \<and> T \<inter> X closure_of S = {}"
  2197 
  2198 lemma separatedin_empty [simp]:
  2199      "separatedin X S {} \<longleftrightarrow> S \<subseteq> topspace X"
  2200      "separatedin X {} S \<longleftrightarrow> S \<subseteq> topspace X"
  2201   by (simp_all add: separatedin_def)
  2202 
  2203 lemma separatedin_refl [simp]:
  2204      "separatedin X S S \<longleftrightarrow> S = {}"
  2205 proof -
  2206   have "\<And>x. \<lbrakk>separatedin X S S; x \<in> S\<rbrakk> \<Longrightarrow> False"
  2207     by (metis all_not_in_conv closure_of_subset inf.orderE separatedin_def)
  2208   then show ?thesis
  2209     by auto
  2210 qed
  2211 
  2212 lemma separatedin_sym:
  2213      "separatedin X S T \<longleftrightarrow> separatedin X T S"
  2214   by (auto simp: separatedin_def)
  2215 
  2216 lemma separatedin_imp_disjoint:
  2217      "separatedin X S T \<Longrightarrow> disjnt S T"
  2218   by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def)
  2219 
  2220 lemma separatedin_mono:
  2221    "\<lbrakk>separatedin X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separatedin X S' T'"
  2222   unfolding separatedin_def
  2223   using closure_of_mono by blast
  2224 
  2225 lemma separatedin_open_sets:
  2226      "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
  2227   unfolding disjnt_def separatedin_def
  2228   by (auto simp: openin_Int_closure_of_eq_empty openin_subset)
  2229 
  2230 lemma separatedin_closed_sets:
  2231      "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
  2232   by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)
  2233 
  2234 lemma separatedin_subtopology:
  2235      "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
  2236   apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
  2237   apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
  2238   done
  2239 
  2240 lemma separatedin_discrete_topology:
  2241      "separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
  2242   by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology)
  2243 
  2244 lemma separated_eq_distinguishable:
  2245    "separatedin X {x} {y} \<longleftrightarrow>
  2246         x \<in> topspace X \<and> y \<in> topspace X \<and>
  2247         (\<exists>U. openin X U \<and> x \<in> U \<and> (y \<notin> U)) \<and>
  2248         (\<exists>v. openin X v \<and> y \<in> v \<and> (x \<notin> v))"
  2249   by (force simp: separatedin_def closure_of_def)
  2250 
  2251 lemma separatedin_Un [simp]:
  2252    "separatedin X S (T \<union> U) \<longleftrightarrow> separatedin X S T \<and> separatedin X S U"
  2253    "separatedin X (S \<union> T) U \<longleftrightarrow> separatedin X S U \<and> separatedin X T U"
  2254   by (auto simp: separatedin_def)
  2255 
  2256 lemma separatedin_Union:
  2257   "finite \<F> \<Longrightarrow> separatedin X S (\<Union>\<F>) \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<forall>T \<in> \<F>. separatedin X S T)"
  2258   "finite \<F> \<Longrightarrow> separatedin X (\<Union>\<F>) S \<longleftrightarrow> (\<forall>T \<in> \<F>. separatedin X S T) \<and> S \<subseteq> topspace X"
  2259   by (auto simp: separatedin_def closure_of_Union)
  2260 
  2261 lemma separatedin_openin_diff:
  2262    "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
  2263   unfolding separatedin_def
  2264   apply (intro conjI)
  2265   apply (meson Diff_subset openin_subset subset_trans)+
  2266   using openin_Int_closure_of_eq_empty by fastforce+
  2267 
  2268 lemma separatedin_closedin_diff:
  2269      "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
  2270   apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
  2271   apply (meson Diff_subset closedin_subset subset_trans)
  2272   done
  2273 
  2274 lemma separation_closedin_Un_gen:
  2275      "separatedin X S T \<longleftrightarrow>
  2276         S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
  2277         closedin (subtopology X (S \<union> T)) S \<and>
  2278         closedin (subtopology X (S \<union> T)) T"
  2279   apply (simp add: separatedin_def closedin_Int_closure_of disjnt_iff)
  2280   using closure_of_subset apply blast
  2281   done
  2282 
  2283 lemma separation_openin_Un_gen:
  2284      "separatedin X S T \<longleftrightarrow>
  2285         S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
  2286         openin (subtopology X (S \<union> T)) S \<and>
  2287         openin (subtopology X (S \<union> T)) T"
  2288   unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
  2289   by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)
  2290 
  2291 
  2292 subsection\<open>Homeomorphisms\<close>
  2293 text\<open>(1-way and 2-way versions may be useful in places)\<close>
  2294 
  2295 definition homeomorphic_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  2296   where
  2297  "homeomorphic_map X Y f \<equiv> quotient_map X Y f \<and> inj_on f (topspace X)"
  2298 
  2299 definition homeomorphic_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
  2300   where
  2301  "homeomorphic_maps X Y f g \<equiv>
  2302     continuous_map X Y f \<and> continuous_map Y X g \<and>
  2303      (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
  2304 
  2305 
  2306 lemma homeomorphic_map_eq:
  2307    "\<lbrakk>homeomorphic_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> homeomorphic_map X Y g"
  2308   by (meson homeomorphic_map_def inj_on_cong quotient_map_eq)
  2309 
  2310 lemma homeomorphic_maps_eq:
  2311      "\<lbrakk>homeomorphic_maps X Y f g;
  2312        \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
  2313       \<Longrightarrow> homeomorphic_maps X Y f' g'"
  2314   apply (simp add: homeomorphic_maps_def)
  2315   by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
  2316 
  2317 lemma homeomorphic_maps_sym:
  2318      "homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
  2319   by (auto simp: homeomorphic_maps_def)
  2320 
  2321 lemma homeomorphic_maps_id:
  2322      "homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
  2323   (is "?lhs = ?rhs")
  2324 proof
  2325   assume L: ?lhs
  2326   then have "topspace X = topspace Y"
  2327     by (auto simp: homeomorphic_maps_def continuous_map_def)
  2328   with L show ?rhs
  2329     unfolding homeomorphic_maps_def
  2330     by (metis topology_finer_continuous_id topology_eq)
  2331 next
  2332   assume ?rhs
  2333   then show ?lhs
  2334     unfolding homeomorphic_maps_def by auto
  2335 qed
  2336 
  2337 lemma homeomorphic_map_id [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
  2338        (is "?lhs = ?rhs")
  2339 proof
  2340   assume L: ?lhs
  2341   then have eq: "topspace X = topspace Y"
  2342     by (auto simp: homeomorphic_map_def continuous_map_def quotient_map_def)
  2343   then have "\<And>S. openin X S \<longrightarrow> openin Y S"
  2344     by (meson L homeomorphic_map_def injective_quotient_map topology_finer_open_id)
  2345   then show ?rhs
  2346     using L unfolding homeomorphic_map_def
  2347     by (metis eq quotient_imp_continuous_map topology_eq topology_finer_continuous_id)
  2348 next
  2349   assume ?rhs
  2350   then show ?lhs
  2351     unfolding homeomorphic_map_def
  2352     by (simp add: closed_map_id continuous_closed_imp_quotient_map)
  2353 qed
  2354 
  2355 lemma homeomorphic_maps_i [simp]:"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
  2356   by (metis (full_types) eq_id_iff homeomorphic_maps_id)
  2357 
  2358 lemma homeomorphic_map_i [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
  2359   by (metis (no_types) eq_id_iff homeomorphic_map_id)
  2360 
  2361 lemma homeomorphic_map_compose:
  2362   assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g"
  2363   shows "homeomorphic_map X X'' (g \<circ> f)"
  2364 proof -
  2365   have "inj_on g (f ` topspace X)"
  2366     by (metis (no_types) assms homeomorphic_map_def quotient_imp_surjective_map)
  2367   then show ?thesis
  2368     using assms by (meson comp_inj_on homeomorphic_map_def quotient_map_compose_eq)
  2369 qed
  2370 
  2371 lemma homeomorphic_maps_compose:
  2372    "homeomorphic_maps X Y f h \<and>
  2373         homeomorphic_maps Y X'' g k
  2374         \<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
  2375   unfolding homeomorphic_maps_def
  2376   by (auto simp: continuous_map_compose; simp add: continuous_map_def)
  2377 
  2378 lemma homeomorphic_eq_everything_map:
  2379    "homeomorphic_map X Y f \<longleftrightarrow>
  2380         continuous_map X Y f \<and> open_map X Y f \<and> closed_map X Y f \<and>
  2381         f ` (topspace X) = topspace Y \<and> inj_on f (topspace X)"
  2382   unfolding homeomorphic_map_def
  2383   by (force simp: injective_quotient_map intro: injective_quotient_map)
  2384 
  2385 lemma homeomorphic_imp_continuous_map:
  2386      "homeomorphic_map X Y f \<Longrightarrow> continuous_map X Y f"
  2387   by (simp add: homeomorphic_eq_everything_map)
  2388 
  2389 lemma homeomorphic_imp_open_map:
  2390    "homeomorphic_map X Y f \<Longrightarrow> open_map X Y f"
  2391   by (simp add: homeomorphic_eq_everything_map)
  2392 
  2393 lemma homeomorphic_imp_closed_map:
  2394    "homeomorphic_map X Y f \<Longrightarrow> closed_map X Y f"
  2395   by (simp add: homeomorphic_eq_everything_map)
  2396 
  2397 lemma homeomorphic_imp_surjective_map:
  2398    "homeomorphic_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
  2399   by (simp add: homeomorphic_eq_everything_map)
  2400 
  2401 lemma homeomorphic_imp_injective_map:
  2402     "homeomorphic_map X Y f \<Longrightarrow> inj_on f (topspace X)"
  2403   by (simp add: homeomorphic_eq_everything_map)
  2404 
  2405 lemma bijective_open_imp_homeomorphic_map:
  2406    "\<lbrakk>continuous_map X Y f; open_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
  2407         \<Longrightarrow> homeomorphic_map X Y f"
  2408   by (simp add: homeomorphic_map_def continuous_open_imp_quotient_map)
  2409 
  2410 lemma bijective_closed_imp_homeomorphic_map:
  2411    "\<lbrakk>continuous_map X Y f; closed_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
  2412         \<Longrightarrow> homeomorphic_map X Y f"
  2413   by (simp add: continuous_closed_quotient_map homeomorphic_map_def)
  2414 
  2415 lemma open_eq_continuous_inverse_map:
  2416   assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
  2417     and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
  2418   shows "open_map X Y f \<longleftrightarrow> continuous_map Y X g"
  2419 proof -
  2420   have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "openin X U" for U
  2421     using openin_subset [OF that] by (force simp: X Y image_iff)
  2422   show ?thesis
  2423     by (auto simp: Y open_map_def continuous_map_def eq)
  2424 qed
  2425 
  2426 lemma closed_eq_continuous_inverse_map:
  2427   assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
  2428     and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
  2429   shows "closed_map X Y f \<longleftrightarrow> continuous_map Y X g"
  2430 proof -
  2431   have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "closedin X U" for U
  2432     using closedin_subset [OF that] by (force simp: X Y image_iff)
  2433   show ?thesis
  2434     by (auto simp: Y closed_map_def continuous_map_closedin eq)
  2435 qed
  2436 
  2437 lemma homeomorphic_maps_map:
  2438   "homeomorphic_maps X Y f g \<longleftrightarrow>
  2439         homeomorphic_map X Y f \<and> homeomorphic_map Y X g \<and>
  2440         (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
  2441   (is "?lhs = ?rhs")
  2442 proof
  2443   assume ?lhs
  2444   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'"
  2445     by (auto simp: homeomorphic_maps_def)
  2446   show ?rhs
  2447   proof (intro conjI bijective_open_imp_homeomorphic_map L)
  2448     show "open_map X Y f"
  2449       using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
  2450     show "open_map Y X g"
  2451       using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
  2452     show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
  2453       using L by (force simp: continuous_map_closedin)+
  2454     show "inj_on f (topspace X)" "inj_on g (topspace Y)"
  2455       using L unfolding inj_on_def by metis+
  2456   qed
  2457 next
  2458   assume ?rhs
  2459   then show ?lhs
  2460     by (auto simp: homeomorphic_maps_def homeomorphic_imp_continuous_map)
  2461 qed
  2462 
  2463 lemma homeomorphic_maps_imp_map:
  2464     "homeomorphic_maps X Y f g \<Longrightarrow> homeomorphic_map X Y f"
  2465   using homeomorphic_maps_map by blast
  2466 
  2467 lemma homeomorphic_map_maps:
  2468      "homeomorphic_map X Y f \<longleftrightarrow> (\<exists>g. homeomorphic_maps X Y f g)"
  2469   (is "?lhs = ?rhs")
  2470 proof
  2471   assume ?lhs
  2472   then have L: "continuous_map X Y f" "open_map X Y f" "closed_map X Y f"
  2473     "f ` (topspace X) = topspace Y" "inj_on f (topspace X)"
  2474     by (auto simp: homeomorphic_eq_everything_map)
  2475   have X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> inv_into (topspace X) f (f x) = x"
  2476     using L by auto
  2477   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"
  2478     by (simp add: L f_inv_into_f inv_into_into)
  2479   have "homeomorphic_maps X Y f (inv_into (topspace X) f)"
  2480     unfolding homeomorphic_maps_def
  2481   proof (intro conjI L)
  2482     show "continuous_map Y X (inv_into (topspace X) f)"
  2483       by (simp add: L X Y flip: open_eq_continuous_inverse_map [where f=f])
  2484   next
  2485     show "\<forall>x\<in>topspace X. inv_into (topspace X) f (f x) = x"
  2486          "\<forall>y\<in>topspace Y. f (inv_into (topspace X) f y) = y"
  2487       using X Y by auto
  2488   qed
  2489   then show ?rhs
  2490     by metis
  2491 next
  2492   assume ?rhs
  2493   then show ?lhs
  2494     using homeomorphic_maps_map by blast
  2495 qed
  2496 
  2497 lemma homeomorphic_maps_involution:
  2498    "\<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"
  2499   by (auto simp: homeomorphic_maps_def)
  2500 
  2501 lemma homeomorphic_map_involution:
  2502    "\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_map X X f"
  2503   using homeomorphic_maps_involution homeomorphic_maps_map by blast
  2504 
  2505 lemma homeomorphic_map_openness:
  2506   assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  2507   shows "openin Y (f ` U) \<longleftrightarrow> openin X U"
  2508 proof -
  2509   obtain g where "homeomorphic_maps X Y f g"
  2510     using assms by (auto simp: homeomorphic_map_maps)
  2511   then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
  2512     by (auto simp: homeomorphic_maps_map)
  2513   then have "openin X U \<Longrightarrow> openin Y (f ` U)"
  2514     using hom homeomorphic_imp_open_map open_map_def by blast
  2515   show "openin Y (f ` U) = openin X U"
  2516   proof
  2517     assume L: "openin Y (f ` U)"
  2518     have "U = g ` (f ` U)"
  2519       using U gf by force
  2520     then show "openin X U"
  2521       by (metis L homeomorphic_imp_open_map open_map_def g)
  2522   next
  2523     assume "openin X U"
  2524     then show "openin Y (f ` U)"
  2525       using hom homeomorphic_imp_open_map open_map_def by blast
  2526   qed
  2527 qed
  2528 
  2529 
  2530 lemma homeomorphic_map_closedness:
  2531   assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  2532   shows "closedin Y (f ` U) \<longleftrightarrow> closedin X U"
  2533 proof -
  2534   obtain g where "homeomorphic_maps X Y f g"
  2535     using assms by (auto simp: homeomorphic_map_maps)
  2536   then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
  2537     by (auto simp: homeomorphic_maps_map)
  2538   then have "closedin X U \<Longrightarrow> closedin Y (f ` U)"
  2539     using hom homeomorphic_imp_closed_map closed_map_def by blast
  2540   show "closedin Y (f ` U) = closedin X U"
  2541   proof
  2542     assume L: "closedin Y (f ` U)"
  2543     have "U = g ` (f ` U)"
  2544       using U gf by force
  2545     then show "closedin X U"
  2546       by (metis L homeomorphic_imp_closed_map closed_map_def g)
  2547   next
  2548     assume "closedin X U"
  2549     then show "closedin Y (f ` U)"
  2550       using hom homeomorphic_imp_closed_map closed_map_def by blast
  2551   qed
  2552 qed
  2553 
  2554 lemma homeomorphic_map_openness_eq:
  2555      "homeomorphic_map X Y f \<Longrightarrow> openin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> openin Y (f ` U)"
  2556   by (meson homeomorphic_map_openness openin_closedin_eq)
  2557 
  2558 lemma homeomorphic_map_closedness_eq:
  2559     "homeomorphic_map X Y f \<Longrightarrow> closedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> closedin Y (f ` U)"
  2560   by (meson closedin_subset homeomorphic_map_closedness)
  2561 
  2562 lemma all_openin_homeomorphic_image:
  2563   assumes "homeomorphic_map X Y f"
  2564   shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
  2565 proof
  2566   assume ?lhs
  2567   then show ?rhs
  2568     by (meson assms homeomorphic_map_openness_eq)
  2569 next
  2570   assume ?rhs
  2571   then show ?lhs
  2572     by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff)
  2573 qed
  2574 
  2575 lemma all_closedin_homeomorphic_image:
  2576   assumes "homeomorphic_map X Y f"
  2577   shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
  2578 proof
  2579   assume ?lhs
  2580   then show ?rhs
  2581     by (meson assms homeomorphic_map_closedness_eq)
  2582 next
  2583   assume ?rhs
  2584   then show ?lhs
  2585     by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff)
  2586 qed
  2587 
  2588 
  2589 lemma homeomorphic_map_derived_set_of:
  2590   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  2591   shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
  2592 proof -
  2593   have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
  2594     using hom by (auto simp: homeomorphic_eq_everything_map)
  2595   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)) =
  2596             (\<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))"
  2597     if "x \<in> topspace X" for x
  2598   proof -
  2599     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
  2600       by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
  2601     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")
  2602       if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
  2603     proof
  2604       show "?lhs \<Longrightarrow> ?rhs"
  2605         by (meson "1" imageI inj inj_on_eq_iff inj_on_subset that)
  2606       show "?rhs \<Longrightarrow> ?lhs"
  2607         using S inj inj_onD that by fastforce
  2608     qed
  2609     show ?thesis
  2610       apply (simp flip: fim add: all_subset_image)
  2611       apply (simp flip: imp_conjL)
  2612       by (intro all_cong1 imp_cong 1 2)
  2613   qed
  2614   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
  2615     by auto
  2616   show ?thesis
  2617     unfolding derived_set_of_def
  2618     apply (rule *)
  2619     using fim apply blast
  2620     using iff openin_subset by force
  2621 qed
  2622 
  2623 
  2624 lemma homeomorphic_map_closure_of:
  2625   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  2626   shows "Y closure_of (f ` S) = f ` (X closure_of S)"
  2627   unfolding closure_of
  2628   using homeomorphic_imp_surjective_map [OF hom] S
  2629   by (auto simp: in_derived_set_of homeomorphic_map_derived_set_of [OF assms])
  2630 
  2631 lemma homeomorphic_map_interior_of:
  2632   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  2633   shows "Y interior_of (f ` S) = f ` (X interior_of S)"
  2634 proof -
  2635   { fix y
  2636     assume "y \<in> topspace Y" and "y \<notin> Y closure_of (topspace Y - f ` S)"
  2637     then have "y \<in> f ` (topspace X - X closure_of (topspace X - S))"
  2638       using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom]
  2639       by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) }
  2640   moreover
  2641   { fix x
  2642     assume "x \<in> topspace X"
  2643     then have "f x \<in> topspace Y"
  2644       using hom homeomorphic_imp_surjective_map by blast }
  2645   moreover
  2646   { fix x
  2647     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)"
  2648     then have "False"
  2649       using homeomorphic_map_closure_of [OF hom] hom
  2650       unfolding homeomorphic_eq_everything_map
  2651       by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
  2652   ultimately  show ?thesis
  2653     by (auto simp: interior_of_closure_of)
  2654 qed
  2655 
  2656 lemma homeomorphic_map_frontier_of:
  2657   assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  2658   shows "Y frontier_of (f ` S) = f ` (X frontier_of S)"
  2659   unfolding frontier_of_def
  2660 proof (intro equalityI subsetI DiffI)
  2661   fix y
  2662   assume "y \<in> Y closure_of f ` S - Y interior_of f ` S"
  2663   then show "y \<in> f ` (X closure_of S - X interior_of S)"
  2664     using S hom homeomorphic_map_closure_of homeomorphic_map_interior_of by fastforce
  2665 next
  2666   fix y
  2667   assume "y \<in> f ` (X closure_of S - X interior_of S)"
  2668   then show "y \<in> Y closure_of f ` S"
  2669     using S hom homeomorphic_map_closure_of by fastforce
  2670 next
  2671   fix x
  2672   assume "x \<in> f ` (X closure_of S - X interior_of S)"
  2673   then obtain y where y: "x = f y" "y \<in> X closure_of S" "y \<notin> X interior_of S"
  2674     by blast
  2675   then have "y \<in> topspace X"
  2676     by (simp add: in_closure_of)
  2677   then have "f y \<notin> f ` (X interior_of S)"
  2678     by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
  2679   then show "x \<notin> Y interior_of f ` S"
  2680     using S hom homeomorphic_map_interior_of y(1) by blast
  2681 qed
  2682 
  2683 lemma homeomorphic_maps_subtopologies:
  2684    "\<lbrakk>homeomorphic_maps X Y f g;  f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
  2685         \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
  2686   unfolding homeomorphic_maps_def
  2687   by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
  2688 
  2689 lemma homeomorphic_maps_subtopologies_alt:
  2690      "\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
  2691       \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
  2692   unfolding homeomorphic_maps_def
  2693   by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
  2694 
  2695 lemma homeomorphic_map_subtopologies:
  2696    "\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
  2697         \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
  2698   by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies)
  2699 
  2700 lemma homeomorphic_map_subtopologies_alt:
  2701    "\<lbrakk>homeomorphic_map X Y f;
  2702      \<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S\<rbrakk>
  2703     \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
  2704   unfolding homeomorphic_map_maps
  2705   apply (erule ex_forward)
  2706   apply (rule homeomorphic_maps_subtopologies)
  2707   apply (auto simp: homeomorphic_maps_def continuous_map_def)
  2708   by (metis IntI image_iff)
  2709 
  2710 
  2711 subsection\<open>Relation of homeomorphism between topological spaces\<close>
  2712 
  2713 definition homeomorphic_space (infixr "homeomorphic'_space" 50)
  2714   where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
  2715 
  2716 lemma homeomorphic_space_refl: "X homeomorphic_space X"
  2717   by (meson homeomorphic_maps_id homeomorphic_space_def)
  2718 
  2719 lemma homeomorphic_space_sym:
  2720    "X homeomorphic_space Y \<longleftrightarrow> Y homeomorphic_space X"
  2721   unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym)
  2722 
  2723 lemma homeomorphic_space_trans:
  2724      "\<lbrakk>X1 homeomorphic_space X2; X2 homeomorphic_space X3\<rbrakk> \<Longrightarrow> X1 homeomorphic_space X3"
  2725   unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose)
  2726 
  2727 lemma homeomorphic_space:
  2728      "X homeomorphic_space Y \<longleftrightarrow> (\<exists>f. homeomorphic_map X Y f)"
  2729   by (simp add: homeomorphic_map_maps homeomorphic_space_def)
  2730 
  2731 lemma homeomorphic_maps_imp_homeomorphic_space:
  2732      "homeomorphic_maps X Y f g \<Longrightarrow> X homeomorphic_space Y"
  2733   unfolding homeomorphic_space_def by metis
  2734 
  2735 lemma homeomorphic_map_imp_homeomorphic_space:
  2736      "homeomorphic_map X Y f \<Longrightarrow> X homeomorphic_space Y"
  2737   unfolding homeomorphic_map_maps
  2738   using homeomorphic_space_def by blast
  2739 
  2740 lemma homeomorphic_empty_space:
  2741      "X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
  2742   by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty)
  2743 
  2744 lemma homeomorphic_empty_space_eq:
  2745   assumes "topspace X = {}"
  2746     shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
  2747 proof -
  2748   have "\<forall>f t. continuous_map X (t::'b topology) f"
  2749     using assms continuous_map_on_empty by blast
  2750   then show ?thesis
  2751     by (metis (no_types) assms continuous_map_on_empty empty_iff homeomorphic_empty_space homeomorphic_maps_def homeomorphic_space_def)
  2752 qed
  2753 
  2754 subsection\<open>Connected topological spaces\<close>
  2755 
  2756 definition connected_space :: "'a topology \<Rightarrow> bool" where
  2757   "connected_space X \<equiv>
  2758         \<not>(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
  2759                   topspace X \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
  2760 
  2761 definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
  2762   "connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
  2763 
  2764 lemma connected_spaceD:
  2765   "\<lbrakk>connected_space X;
  2766     openin X U; openin X V; topspace X \<subseteq> U \<union> V; U \<inter> V = {}; U \<noteq> {}; V \<noteq> {}\<rbrakk> \<Longrightarrow> False"
  2767   by (auto simp: connected_space_def)
  2768 
  2769 lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
  2770   by (simp add: connectedin_def)
  2771 
  2772 lemma connectedin_topspace:
  2773      "connectedin X (topspace X) \<longleftrightarrow> connected_space X"
  2774   by (simp add: connectedin_def)
  2775 
  2776 lemma connected_space_subtopology:
  2777      "connectedin X S \<Longrightarrow> connected_space (subtopology X S)"
  2778   by (simp add: connectedin_def)
  2779 
  2780 lemma connectedin_subtopology:
  2781      "connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> S"
  2782   by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2)
  2783 
  2784 lemma connected_space_eq:
  2785      "connected_space X \<longleftrightarrow>
  2786       (\<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> {})"
  2787   unfolding connected_space_def
  2788   by (metis openin_Un openin_subset subset_antisym)
  2789 
  2790 lemma connected_space_closedin:
  2791      "connected_space X \<longleftrightarrow>
  2792       (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and> topspace X \<subseteq> E1 \<union> E2 \<and>
  2793                E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" (is "?lhs = ?rhs")
  2794 proof
  2795   assume ?lhs
  2796   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 = {}"
  2797     by (simp add: connected_space_def)
  2798   show ?rhs
  2799     unfolding connected_space_def
  2800   proof clarify
  2801     fix E1 E2
  2802     assume "closedin X E1" and "closedin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
  2803       and "E1 \<noteq> {}" and "E2 \<noteq> {}"
  2804     have "E1 \<union> E2 = topspace X"
  2805       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)
  2806     then have "topspace X - E2 = E1"
  2807       using \<open>E1 \<inter> E2 = {}\<close> by fastforce
  2808     then have "topspace X = E1"
  2809       using \<open>E1 \<noteq> {}\<close> L \<open>closedin X E1\<close> \<open>closedin X E2\<close> by blast
  2810     then show "False"
  2811       using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
  2812   qed
  2813 next
  2814   assume R: ?rhs
  2815   show ?lhs
  2816     unfolding connected_space_def
  2817   proof clarify
  2818     fix E1 E2
  2819     assume "openin X E1" and "openin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
  2820       and "E1 \<noteq> {}" and "E2 \<noteq> {}"
  2821     have "E1 \<union> E2 = topspace X"
  2822       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)
  2823     then have "topspace X - E2 = E1"
  2824       using \<open>E1 \<inter> E2 = {}\<close> by fastforce
  2825     then have "topspace X = E1"
  2826       using \<open>E1 \<noteq> {}\<close> R \<open>openin X E1\<close> \<open>openin X E2\<close> by blast
  2827     then show "False"
  2828       using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
  2829   qed
  2830 qed
  2831 
  2832 lemma connected_space_closedin_eq:
  2833      "connected_space X \<longleftrightarrow>
  2834        (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
  2835                 E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
  2836   apply (simp add: connected_space_closedin)
  2837   apply (intro all_cong)
  2838   using closedin_subset apply blast
  2839   done
  2840 
  2841 lemma connected_space_clopen_in:
  2842      "connected_space X \<longleftrightarrow>
  2843         (\<forall>T. openin X T \<and> closedin X T \<longrightarrow> T = {} \<or> T = topspace X)"
  2844 proof -
  2845   have eq: "openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> P
  2846         \<longleftrightarrow> E2 = topspace X - E1 \<and> openin X E1 \<and> openin X E2 \<and> P" for E1 E2 P
  2847     using openin_subset by blast
  2848   show ?thesis
  2849     unfolding connected_space_eq eq closedin_def
  2850     by (auto simp: openin_closedin_eq)
  2851 qed
  2852 
  2853 lemma connectedin:
  2854      "connectedin X S \<longleftrightarrow>
  2855         S \<subseteq> topspace X \<and>
  2856          (\<nexists>E1 E2.
  2857              openin X E1 \<and> openin X E2 \<and>
  2858              S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
  2859 proof -
  2860   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>
  2861              R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
  2862     by auto
  2863   show ?thesis
  2864     unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology Not_eq_iff *
  2865     apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
  2866     apply (blast elim: dest!: openin_subset)+
  2867     done
  2868 qed
  2869 
  2870 lemma connectedin_iff_connected [simp]: "connectedin euclidean S \<longleftrightarrow> connected S"
  2871   by (simp add: connected_def connectedin)
  2872 
  2873 lemma connectedin_closedin:
  2874    "connectedin X S \<longleftrightarrow>
  2875         S \<subseteq> topspace X \<and>
  2876         \<not>(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
  2877                   S \<subseteq> (E1 \<union> E2) \<and>
  2878                   (E1 \<inter> E2 \<inter> S = {}) \<and>
  2879                   \<not>(E1 \<inter> S = {}) \<and> \<not>(E2 \<inter> S = {}))"
  2880 proof -
  2881   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>
  2882              R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
  2883     by auto
  2884   show ?thesis
  2885     unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology Not_eq_iff *
  2886     apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
  2887     apply (blast elim: dest!: openin_subset)+
  2888     done
  2889 qed
  2890 
  2891 lemma connectedin_empty [simp]: "connectedin X {}"
  2892   by (simp add: connectedin)
  2893 
  2894 lemma connected_space_topspace_empty:
  2895      "topspace X = {} \<Longrightarrow> connected_space X"
  2896   using connectedin_topspace by fastforce
  2897 
  2898 lemma connectedin_sing [simp]: "connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
  2899   by (simp add: connectedin)
  2900 
  2901 lemma connectedin_absolute [simp]:
  2902   "connectedin (subtopology X S) S \<longleftrightarrow> connectedin X S"
  2903   apply (simp only: connectedin_def topspace_subtopology subtopology_subtopology)
  2904   apply (intro conj_cong imp_cong arg_cong [where f=Not] all_cong1 ex_cong1 refl)
  2905   by auto
  2906 
  2907 lemma connectedin_Union:
  2908   assumes \<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> connectedin X S" and ne: "\<Inter>\<U> \<noteq> {}"
  2909   shows "connectedin X (\<Union>\<U>)"
  2910 proof -
  2911   have "\<Union>\<U> \<subseteq> topspace X"
  2912     using \<U> by (simp add: Union_least connectedin_def)
  2913   moreover have False
  2914     if "openin X E1" "openin X E2" and cover: "\<Union>\<U> \<subseteq> E1 \<union> E2" and disj: "E1 \<inter> E2 \<inter> \<Union>\<U> = {}"
  2915        and overlap1: "E1 \<inter> \<Union>\<U> \<noteq> {}" and overlap2: "E2 \<inter> \<Union>\<U> \<noteq> {}"
  2916       for E1 E2
  2917   proof -
  2918     have disjS: "E1 \<inter> E2 \<inter> S = {}" if "S \<in> \<U>" for S
  2919       using Diff_triv that disj by auto
  2920     have coverS: "S \<subseteq> E1 \<union> E2" if "S \<in> \<U>" for S
  2921       using that cover by blast
  2922     have "\<U> \<noteq> {}"
  2923       using overlap1 by blast
  2924     obtain a where a: "\<And>U. U \<in> \<U> \<Longrightarrow> a \<in> U"
  2925       using ne by force
  2926     with \<open>\<U> \<noteq> {}\<close> have "a \<in> \<Union>\<U>"
  2927       by blast
  2928     then consider "a \<in> E1" | "a \<in> E2"
  2929       using \<open>\<Union>\<U> \<subseteq> E1 \<union> E2\<close> by auto
  2930     then show False
  2931     proof cases
  2932       case 1
  2933       then obtain b S where "b \<in> E2" "b \<in> S" "S \<in> \<U>"
  2934         using overlap2 by blast
  2935       then show ?thesis
  2936         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>]
  2937         unfolding connectedin
  2938         by (meson disjoint_iff_not_equal)
  2939     next
  2940       case 2
  2941       then obtain b S where "b \<in> E1" "b \<in> S" "S \<in> \<U>"
  2942         using overlap1 by blast
  2943       then show ?thesis
  2944         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>]
  2945         unfolding connectedin
  2946         by (meson disjoint_iff_not_equal)
  2947     qed
  2948   qed
  2949   ultimately show ?thesis
  2950     unfolding connectedin by blast
  2951 qed
  2952 
  2953 lemma connectedin_Un:
  2954      "\<lbrakk>connectedin X S; connectedin X T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
  2955   using connectedin_Union [of "{S,T}"] by auto
  2956 
  2957 lemma connected_space_subconnected:
  2958   "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")
  2959 proof
  2960   assume ?lhs
  2961   then show ?rhs
  2962     using connectedin_topspace by blast
  2963 next
  2964   assume R [rule_format]: ?rhs
  2965   have False if "openin X U" "openin X V" and disj: "U \<inter> V = {}" and cover: "topspace X \<subseteq> U \<union> V"
  2966     and "U \<noteq> {}" "V \<noteq> {}" for U V
  2967   proof -
  2968     obtain u v where "u \<in> U" "v \<in> V"
  2969       using \<open>U \<noteq> {}\<close> \<open>V \<noteq> {}\<close> by auto
  2970     then obtain T where "u \<in> T" "v \<in> T" and T: "connectedin X T"
  2971       using R [of u v] that
  2972       by (meson \<open>openin X U\<close> \<open>openin X V\<close> subsetD openin_subset)
  2973     then show False
  2974       using that unfolding connectedin
  2975       by (metis IntI \<open>u \<in> U\<close> \<open>v \<in> V\<close> empty_iff inf_bot_left subset_trans)
  2976   qed
  2977   then show ?lhs
  2978     by (auto simp: connected_space_def)
  2979 qed
  2980 
  2981 lemma connectedin_intermediate_closure_of:
  2982   assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
  2983   shows "connectedin X T"
  2984 proof -
  2985   have S: "S \<subseteq> topspace X"and T: "T \<subseteq> topspace X"
  2986     using assms by (meson closure_of_subset_topspace dual_order.trans)+
  2987   show ?thesis
  2988   using assms
  2989   apply (simp add: connectedin closure_of_subset_topspace S T)
  2990   apply (elim all_forward imp_forward2 asm_rl)
  2991   apply (blast dest: openin_Int_closure_of_eq_empty [of X _ S])+
  2992   done
  2993 qed
  2994 
  2995 lemma connectedin_closure_of:
  2996      "connectedin X S \<Longrightarrow> connectedin X (X closure_of S)"
  2997   by (meson closure_of_subset connectedin_def connectedin_intermediate_closure_of subset_refl)
  2998 
  2999 lemma connectedin_separation:
  3000   "connectedin X S \<longleftrightarrow>
  3001         S \<subseteq> topspace X \<and>
  3002         (\<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")
  3003   unfolding connectedin_def connected_space_closedin_eq closedin_Int_closure_of topspace_subtopology
  3004   apply (intro conj_cong refl arg_cong [where f=Not])
  3005   apply (intro ex_cong1 iffI, blast)
  3006   using closure_of_subset_Int by force
  3007 
  3008 lemma connectedin_eq_not_separated:
  3009    "connectedin X S \<longleftrightarrow>
  3010          S \<subseteq> topspace X \<and>
  3011          (\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
  3012   apply (simp add: separatedin_def connectedin_separation)
  3013   apply (intro conj_cong all_cong1 refl, blast)
  3014   done
  3015 
  3016 lemma connectedin_eq_not_separated_subset:
  3017   "connectedin X S \<longleftrightarrow>
  3018       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)"
  3019 proof -
  3020   have *: "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
  3021     if "\<And>C1 C2. C1 \<union> C2 = S \<longrightarrow> C1 = {} \<or> C2 = {} \<or> \<not> separatedin X C1 C2"
  3022   proof (intro allI)
  3023     fix C1 C2
  3024     show "S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
  3025       using that [of "S \<inter> C1" "S \<inter> C2"]
  3026       by (auto simp: separatedin_mono)
  3027   qed
  3028   show ?thesis
  3029     apply (simp add: connectedin_eq_not_separated)
  3030     apply (intro conj_cong refl iffI *)
  3031     apply (blast elim!: all_forward)+
  3032     done
  3033 qed
  3034 
  3035 lemma connected_space_eq_not_separated:
  3036      "connected_space X \<longleftrightarrow>
  3037       (\<nexists>C1 C2. C1 \<union> C2 = topspace X \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
  3038   by (simp add: connectedin_eq_not_separated flip: connectedin_topspace)
  3039 
  3040 lemma connected_space_eq_not_separated_subset:
  3041   "connected_space X \<longleftrightarrow>
  3042     (\<nexists>C1 C2. topspace X \<subseteq> C1 \<union> C2 \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
  3043   apply (simp add: connected_space_eq_not_separated)
  3044   apply (intro all_cong1)
  3045   by (metis Un_absorb dual_order.antisym separatedin_def subset_refl sup_mono)
  3046 
  3047 lemma connectedin_subset_separated_union:
  3048      "\<lbrakk>connectedin X C; separatedin X S T; C \<subseteq> S \<union> T\<rbrakk> \<Longrightarrow> C \<subseteq> S \<or> C \<subseteq> T"
  3049   unfolding connectedin_eq_not_separated_subset  by blast
  3050 
  3051 lemma connectedin_nonseparated_union:
  3052    "\<lbrakk>connectedin X S; connectedin X T; \<not>separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
  3053   apply (simp add: connectedin_eq_not_separated_subset, auto)
  3054     apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
  3055   apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
  3056   by (meson disjoint_iff_not_equal)
  3057 
  3058 lemma connected_space_closures:
  3059      "connected_space X \<longleftrightarrow>
  3060         (\<nexists>e1 e2. e1 \<union> e2 = topspace X \<and> X closure_of e1 \<inter> X closure_of e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
  3061      (is "?lhs = ?rhs")
  3062 proof
  3063   assume ?lhs
  3064   then show ?rhs
  3065     unfolding connected_space_closedin_eq
  3066     by (metis Un_upper1 Un_upper2 closedin_closure_of closure_of_Un closure_of_eq_empty closure_of_topspace)
  3067 next
  3068   assume ?rhs
  3069   then show ?lhs
  3070     unfolding connected_space_closedin_eq
  3071     by (metis closure_of_eq)
  3072 qed
  3073 
  3074 lemma connectedin_inter_frontier_of:
  3075   assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
  3076   shows "S \<inter> X frontier_of T \<noteq> {}"
  3077 proof -
  3078   have "S \<subseteq> topspace X" and *:
  3079     "\<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 = {}"
  3080     using \<open>connectedin X S\<close> by (auto simp: connectedin)
  3081   have "S - (topspace X \<inter> T) \<noteq> {}"
  3082     using assms(3) by blast
  3083   moreover
  3084   have "S \<inter> topspace X \<inter> T \<noteq> {}"
  3085     using assms(1) assms(2) connectedin by fastforce
  3086   moreover
  3087   have False if "S \<inter> T \<noteq> {}" "S - T \<noteq> {}" "T \<subseteq> topspace X" "S \<inter> X frontier_of T = {}" for T
  3088   proof -
  3089     have null: "S \<inter> (X closure_of T - X interior_of T) = {}"
  3090       using that unfolding frontier_of_def by blast
  3091     have 1: "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
  3092       by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty)
  3093     have 2: "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
  3094       using that \<open>S \<subseteq> topspace X\<close> null by auto
  3095     have 3: "S \<inter> X interior_of T \<noteq> {}"
  3096       using closure_of_subset that(1) that(3) null by fastforce
  3097     show ?thesis
  3098       using null \<open>S \<subseteq> topspace X\<close> that * [of "X interior_of T" "topspace X - X closure_of T"]
  3099       apply (clarsimp simp add: openin_diff 1 2)
  3100       apply (simp add: Int_commute Diff_Int_distrib 3)
  3101       by (metis Int_absorb2 contra_subsetD interior_of_subset)
  3102   qed
  3103   ultimately show ?thesis
  3104     by (metis Int_lower1 frontier_of_restrict inf_assoc)
  3105 qed
  3106 
  3107 lemma connectedin_continuous_map_image:
  3108   assumes f: "continuous_map X Y f" and "connectedin X S"
  3109   shows "connectedin Y (f ` S)"
  3110 proof -
  3111   have "S \<subseteq> topspace X" and *:
  3112     "\<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 = {}"
  3113     using \<open>connectedin X S\<close> by (auto simp: connectedin)
  3114   show ?thesis
  3115     unfolding connectedin connected_space_def
  3116   proof (intro conjI notI; clarify)
  3117     show "f x \<in> topspace Y" if  "x \<in> S" for x
  3118       using \<open>S \<subseteq> topspace X\<close> continuous_map_image_subset_topspace f that by blast
  3119   next
  3120     fix U V
  3121     let ?U = "{x \<in> topspace X. f x \<in> U}"
  3122     let ?V = "{x \<in> topspace X. f x \<in> V}"
  3123     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> {}"
  3124     then have 1: "?U \<inter> ?V \<inter> S = {}"
  3125       by auto
  3126     have 2: "openin X ?U" "openin X ?V"
  3127       using \<open>openin Y U\<close> \<open>openin Y V\<close> continuous_map f by fastforce+
  3128     show "False"
  3129       using  * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
  3130       by (auto simp: 1 2)
  3131   qed
  3132 qed
  3133 
  3134 lemma homeomorphic_connected_space:
  3135      "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
  3136   unfolding homeomorphic_space_def homeomorphic_maps_def
  3137   apply safe
  3138   apply (metis connectedin_continuous_map_image connected_space_subconnected continuous_map_image_subset_topspace image_eqI image_subset_iff)
  3139   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)
  3140 
  3141 lemma homeomorphic_map_connectedness:
  3142   assumes f: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  3143   shows "connectedin Y (f ` U) \<longleftrightarrow> connectedin X U"
  3144 proof -
  3145   have 1: "f ` U \<subseteq> topspace Y \<longleftrightarrow> U \<subseteq> topspace X"
  3146     using U f homeomorphic_imp_surjective_map by blast
  3147   moreover have "connected_space (subtopology Y (f ` U)) \<longleftrightarrow> connected_space (subtopology X U)"
  3148   proof (rule homeomorphic_connected_space)
  3149     have "f ` U \<subseteq> topspace Y"
  3150       by (simp add: U 1)
  3151     then have "topspace Y \<inter> f ` U = f ` U"
  3152       by (simp add: subset_antisym)
  3153     then show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
  3154       by (metis (no_types) Int_subset_iff U f homeomorphic_map_imp_homeomorphic_space homeomorphic_map_subtopologies homeomorphic_space_sym subset_antisym subset_refl)
  3155   qed
  3156   ultimately show ?thesis
  3157     by (auto simp: connectedin_def)
  3158 qed
  3159 
  3160 lemma homeomorphic_map_connectedness_eq:
  3161    "homeomorphic_map X Y f
  3162         \<Longrightarrow> connectedin X U \<longleftrightarrow>
  3163              U \<subseteq> topspace X \<and> connectedin Y (f ` U)"
  3164   using homeomorphic_map_connectedness connectedin_subset_topspace by metis
  3165 
  3166 lemma connectedin_discrete_topology:
  3167    "connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
  3168 proof (cases "S \<subseteq> U")
  3169   case True
  3170   show ?thesis
  3171   proof (cases "S = {}")
  3172     case False
  3173     moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
  3174       apply safe
  3175       using False connectedin_inter_frontier_of insert_Diff apply fastforce
  3176       using True by auto
  3177     ultimately show ?thesis
  3178       by auto
  3179   qed simp
  3180 next
  3181   case False
  3182   then show ?thesis
  3183     by (simp add: connectedin_def)
  3184 qed
  3185 
  3186 lemma connected_space_discrete_topology:
  3187      "connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
  3188   by (metis connectedin_discrete_topology connectedin_topspace order_refl topspace_discrete_topology)
  3189 
  3190 
  3191 subsection\<open>Compact sets\<close>
  3192 
  3193 definition compactin where
  3194  "compactin X S \<longleftrightarrow>
  3195      S \<subseteq> topspace X \<and>
  3196      (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
  3197           \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>))"
  3198 
  3199 definition compact_space where
  3200    "compact_space X \<equiv> compactin X (topspace X)"
  3201 
  3202 lemma compact_space_alt:
  3203    "compact_space X \<longleftrightarrow>
  3204         (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
  3205             \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>))"
  3206   by (simp add: compact_space_def compactin_def)
  3207 
  3208 lemma compact_space:
  3209    "compact_space X \<longleftrightarrow>
  3210         (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
  3211             \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> \<Union>\<F> = topspace X))"
  3212   unfolding compact_space_alt
  3213   using openin_subset by fastforce
  3214 
  3215 lemma compactin_euclidean_iff [simp]: "compactin euclidean S \<longleftrightarrow> compact S"
  3216   by (simp add: compact_eq_Heine_Borel compactin_def) meson
  3217 
  3218 lemma compactin_absolute [simp]:
  3219    "compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
  3220 proof -
  3221   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>
  3222     by auto
  3223   show ?thesis
  3224     by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
  3225 qed
  3226 
  3227 lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
  3228   unfolding compact_space_def topspace_subtopology
  3229   by (metis compactin_absolute compactin_def inf.absorb2)
  3230 
  3231 lemma compact_space_subtopology: "compactin X S \<Longrightarrow> compact_space (subtopology X S)"
  3232   by (simp add: compactin_subspace)
  3233 
  3234 lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
  3235 apply (simp add: compactin_subspace topspace_subtopology)
  3236   by (metis inf.orderE inf_commute subtopology_subtopology)
  3237 
  3238 
  3239 lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
  3240   by (simp add: compactin_subspace)
  3241 
  3242 lemma compactin_contractive:
  3243    "\<lbrakk>compactin X' S; topspace X' = topspace X;
  3244      \<And>U. openin X U \<Longrightarrow> openin X' U\<rbrakk> \<Longrightarrow> compactin X S"
  3245   by (simp add: compactin_def)
  3246 
  3247 lemma finite_imp_compactin:
  3248    "\<lbrakk>S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> compactin X S"
  3249   by (metis compactin_subspace compact_space finite_UnionD inf.absorb_iff2 order_refl topspace_subtopology)
  3250 
  3251 lemma compactin_empty [iff]: "compactin X {}"
  3252   by (simp add: finite_imp_compactin)
  3253 
  3254 lemma compact_space_topspace_empty:
  3255    "topspace X = {} \<Longrightarrow> compact_space X"
  3256   by (simp add: compact_space_def)
  3257 
  3258 lemma finite_imp_compactin_eq:
  3259    "finite S \<Longrightarrow> (compactin X S \<longleftrightarrow> S \<subseteq> topspace X)"
  3260   using compactin_subset_topspace finite_imp_compactin by blast
  3261 
  3262 lemma compactin_sing [simp]: "compactin X {a} \<longleftrightarrow> a \<in> topspace X"
  3263   by (simp add: finite_imp_compactin_eq)
  3264 
  3265 lemma closed_compactin:
  3266   assumes XK: "compactin X K" and "C \<subseteq> K" and XC: "closedin X C"
  3267   shows "compactin X C"
  3268   unfolding compactin_def
  3269 proof (intro conjI allI impI)
  3270   show "C \<subseteq> topspace X"
  3271     by (simp add: XC closedin_subset)
  3272 next
  3273   fix \<U> :: "'a set set"
  3274   assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
  3275   have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
  3276     using XC \<U> by blast
  3277   moreover have "K \<subseteq> \<Union>(insert (topspace X - C) \<U>)"
  3278     using \<U> XK compactin_subset_topspace by fastforce
  3279   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
  3280     using assms unfolding compactin_def by metis
  3281   moreover have "openin X (topspace X - C)"
  3282     using XC by auto
  3283   ultimately show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> C \<subseteq> \<Union>\<F>"
  3284     using \<open>C \<subseteq> K\<close>
  3285     by (rule_tac x="\<F> - {topspace X - C}" in exI) auto
  3286 qed
  3287 
  3288 lemma closedin_compact_space:
  3289    "\<lbrakk>compact_space X; closedin X S\<rbrakk> \<Longrightarrow> compactin X S"
  3290   by (simp add: closed_compactin closedin_subset compact_space_def)
  3291 
  3292 lemma compact_Int_closedin:
  3293   assumes "compactin X S" "closedin X T" shows "compactin X (S \<inter> T)"
  3294 proof -
  3295   have "compactin (subtopology X S) (S \<inter> T)"
  3296     by (metis assms closedin_compact_space closedin_subtopology compactin_subspace inf_commute)
  3297   then show ?thesis
  3298     by (simp add: compactin_subtopology)
  3299 qed
  3300 
  3301 lemma closed_Int_compactin: "\<lbrakk>closedin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
  3302   by (metis compact_Int_closedin inf_commute)
  3303 
  3304 lemma compactin_Un:
  3305   assumes S: "compactin X S" and T: "compactin X T" shows "compactin X (S \<union> T)"
  3306   unfolding compactin_def
  3307 proof (intro conjI allI impI)
  3308   show "S \<union> T \<subseteq> topspace X"
  3309     using assms by (auto simp: compactin_def)
  3310 next
  3311   fix \<U> :: "'a set set"
  3312   assume \<U>: "Ball \<U> (openin X) \<and> S \<union> T \<subseteq> \<Union>\<U>"
  3313   with S obtain \<F> where \<V>: "finite \<F>" "\<F> \<subseteq> \<U>" "S \<subseteq> \<Union>\<F>"
  3314     unfolding compactin_def by (meson sup.bounded_iff)
  3315   obtain \<W> where "finite \<W>" "\<W> \<subseteq> \<U>" "T \<subseteq> \<Union>\<W>"
  3316     using \<U> T
  3317     unfolding compactin_def by (meson sup.bounded_iff)
  3318   with \<V> show "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> S \<union> T \<subseteq> \<Union>\<V>"
  3319     by (rule_tac x="\<F> \<union> \<W>" in exI) auto
  3320 qed
  3321 
  3322 lemma compactin_Union:
  3323    "\<lbrakk>finite \<F>; \<And>S. S \<in> \<F> \<Longrightarrow> compactin X S\<rbrakk> \<Longrightarrow> compactin X (\<Union>\<F>)"
  3324 by (induction rule: finite_induct) (simp_all add: compactin_Un)
  3325 
  3326 lemma compactin_subtopology_imp_compact:
  3327   assumes "compactin (subtopology X S) K" shows "compactin X K"
  3328   using assms
  3329 proof (clarsimp simp add: compactin_def topspace_subtopology)
  3330   fix \<U>
  3331   define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
  3332   assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
  3333   then have "\<forall>V \<in> \<V>. openin (subtopology X S) V" "K \<subseteq> \<Union>\<V>"
  3334     unfolding \<V>_def by (auto simp: openin_subtopology)
  3335   moreover
  3336   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>)"
  3337   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
  3338     by meson
  3339   then have \<F>: "\<exists>U. U \<in> \<U> \<and> V = U \<inter> S" if "V \<in> \<F>" for V
  3340     unfolding \<V>_def using that by blast
  3341   let ?\<F> = "(\<lambda>F. @U. U \<in> \<U> \<and> F = U \<inter> S) ` \<F>"
  3342   show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
  3343   proof (intro exI conjI)
  3344     show "finite ?\<F>"
  3345       using \<open>finite \<F>\<close> by blast
  3346     show "?\<F> \<subseteq> \<U>"
  3347       using someI_ex [OF \<F>] by blast
  3348     show "K \<subseteq> \<Union>?\<F>"
  3349     proof clarsimp
  3350       fix x
  3351       assume "x \<in> K"
  3352       then show "\<exists>V \<in> \<F>. x \<in> (SOME U. U \<in> \<U> \<and> V = U \<inter> S)"
  3353         using \<open>K \<subseteq> \<Union>\<F>\<close> someI_ex [OF \<F>]
  3354         by (metis (no_types, lifting) IntD1 Union_iff subsetCE)
  3355     qed
  3356   qed
  3357 qed
  3358 
  3359 lemma compact_imp_compactin_subtopology:
  3360   assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
  3361   using assms
  3362 proof (clarsimp simp add: compactin_def topspace_subtopology)
  3363   fix \<U> :: "'a set set"
  3364   define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
  3365   assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
  3366   then have "\<forall>V \<in> \<V>. openin X V" "K \<subseteq> \<Union>\<V>"
  3367     unfolding \<V>_def by (fastforce simp: subset_eq openin_subtopology)+
  3368   moreover
  3369   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>)"
  3370   ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
  3371     by meson
  3372   let ?\<F> = "(\<lambda>F. F \<inter> S) ` \<F>"
  3373   show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
  3374   proof (intro exI conjI)
  3375     show "finite ?\<F>"
  3376       using \<open>finite \<F>\<close> by blast
  3377     show "?\<F> \<subseteq> \<U>"
  3378       using \<V>_def \<open>\<F> \<subseteq> \<V>\<close> by blast
  3379     show "K \<subseteq> \<Union>?\<F>"
  3380       using \<open>K \<subseteq> \<Union>\<F>\<close> assms(2) by auto
  3381   qed
  3382 qed
  3383 
  3384 
  3385 proposition compact_space_fip:
  3386    "compact_space X \<longleftrightarrow>
  3387     (\<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> {})"
  3388    (is "_ = ?rhs")
  3389 proof (cases "topspace X = {}")
  3390   case True
  3391   then show ?thesis
  3392     apply (clarsimp simp add: compact_space_def closedin_topspace_empty)
  3393     by (metis finite.emptyI finite_insert infinite_super insertI1 subsetI)
  3394 next
  3395   case False
  3396   show ?thesis
  3397   proof safe
  3398     fix \<U> :: "'a set set"
  3399     assume * [rule_format]: "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
  3400     define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
  3401     assume clo: "\<forall>C\<in>\<U>. closedin X C" and [simp]: "\<Inter>\<U> = {}"
  3402     then have "\<forall>V \<in> \<V>. openin X V" "topspace X \<subseteq> \<Union>\<V>"
  3403       by (auto simp: \<V>_def)
  3404     moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
  3405     ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
  3406       by (auto simp: exists_finite_subset_image \<V>_def)
  3407     moreover have "\<F> \<noteq> {}"
  3408       using \<F> \<open>topspace X \<noteq> {}\<close> by blast
  3409     ultimately show "False"
  3410       using * [of \<F>]
  3411       by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
  3412   next
  3413     assume R [rule_format]: ?rhs
  3414     show "compact_space X"
  3415       unfolding compact_space_alt
  3416     proof clarify
  3417       fix \<U> :: "'a set set"
  3418       define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
  3419       assume "\<forall>C\<in>\<U>. openin X C" and "topspace X \<subseteq> \<Union>\<U>"
  3420       with \<open>topspace X \<noteq> {}\<close> have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
  3421         by (auto simp: \<V>_def)
  3422       show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>"
  3423       proof (rule ccontr; simp)
  3424         assume "\<forall>\<F>\<subseteq>\<U>. finite \<F> \<longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>"
  3425         then have "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<V> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
  3426           by (simp add: \<V>_def all_finite_subset_image)
  3427         with \<open>topspace X \<subseteq> \<Union>\<U>\<close> show False
  3428           using R [of \<V>] * by (simp add: \<V>_def)
  3429       qed
  3430     qed
  3431   qed
  3432 qed
  3433 
  3434 corollary compactin_fip:
  3435   "compactin X S \<longleftrightarrow>
  3436     S \<subseteq> topspace X \<and>
  3437     (\<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> {})"
  3438 proof (cases "S = {}")
  3439   case False
  3440   show ?thesis
  3441   proof (cases "S \<subseteq> topspace X")
  3442     case True
  3443     then have "compactin X S \<longleftrightarrow>
  3444           (\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
  3445            (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
  3446       by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
  3447     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> {})"
  3448       by (simp add: all_subset_image)
  3449     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> {})"
  3450     proof -
  3451       have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
  3452                 ((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"  for \<U>
  3453         by simp (use \<open>S \<noteq> {}\<close> in blast)
  3454       show ?thesis
  3455         apply (simp only: imp_conjL [symmetric] all_finite_subset_image eq)
  3456         apply (simp add: subset_eq)
  3457         done
  3458     qed
  3459     finally show ?thesis
  3460       using True by simp
  3461   qed (simp add: compactin_subspace)
  3462 qed force
  3463 
  3464 corollary compact_space_imp_nest:
  3465   fixes C :: "nat \<Rightarrow> 'a set"
  3466   assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
  3467     and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
  3468   shows "(\<Inter>n. C n) \<noteq> {}"
  3469 proof -
  3470   let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
  3471   have "closedin X A" if "A \<in> ?\<U>" for A
  3472     using that clo by auto
  3473   moreover have "(\<Inter>n\<in>K. \<Inter>m \<le> n. C m) \<noteq> {}" if "finite K" for K
  3474   proof -
  3475     obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
  3476       using Max.coboundedI \<open>finite K\<close> by blast
  3477     with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
  3478     by blast
  3479   with ne [of n] show ?thesis
  3480     by blast
  3481   qed
  3482   ultimately show ?thesis
  3483     using \<open>compact_space X\<close> [unfolded compact_space_fip, rule_format, of ?\<U>]
  3484     by (simp add: all_finite_subset_image INT_extend_simps UN_atMost_UNIV del: INT_simps)
  3485 qed
  3486 
  3487 lemma compactin_discrete_topology:
  3488    "compactin (discrete_topology X) S \<longleftrightarrow> S \<subseteq> X \<and> finite S" (is "?lhs = ?rhs")
  3489 proof (intro iffI conjI)
  3490   assume L: ?lhs
  3491   then show "S \<subseteq> X"
  3492     by (auto simp: compactin_def)
  3493   have *: "\<And>\<U>. Ball \<U> (openin (discrete_topology X)) \<and> S \<subseteq> \<Union>\<U> \<Longrightarrow>
  3494         (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>)"
  3495     using L by (auto simp: compactin_def)
  3496   show "finite S"
  3497     using * [of "(\<lambda>x. {x}) ` X"] \<open>S \<subseteq> X\<close>
  3498     by clarsimp (metis UN_singleton finite_subset_image infinite_super)
  3499 next
  3500   assume ?rhs
  3501   then show ?lhs
  3502     by (simp add: finite_imp_compactin)
  3503 qed
  3504 
  3505 lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
  3506   by (simp add: compactin_discrete_topology compact_space_def)
  3507 
  3508 lemma compact_space_imp_Bolzano_Weierstrass:
  3509   assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
  3510   shows "X derived_set_of S \<noteq> {}"
  3511 proof
  3512   assume X: "X derived_set_of S = {}"
  3513   then have "closedin X S"
  3514     by (simp add: closedin_contains_derived_set assms)
  3515   then have "compactin X S"
  3516     by (rule closedin_compact_space [OF \<open>compact_space X\<close>])
  3517   with X show False
  3518     by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
  3519 qed
  3520 
  3521 lemma compactin_imp_Bolzano_Weierstrass:
  3522    "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
  3523   using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
  3524   by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
  3525 
  3526 lemma compact_closure_of_imp_Bolzano_Weierstrass:
  3527    "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
  3528   using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce
  3529 
  3530 lemma discrete_compactin_eq_finite:
  3531    "S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
  3532   apply (rule iffI)
  3533   using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
  3534   by (simp add: finite_imp_compactin_eq)
  3535 
  3536 lemma discrete_compact_space_eq_finite:
  3537    "X derived_set_of (topspace X) = {} \<Longrightarrow> (compact_space X \<longleftrightarrow> finite(topspace X))"
  3538   by (metis compact_space_discrete_topology discrete_topology_unique_derived_set)
  3539 
  3540 lemma image_compactin:
  3541   assumes cpt: "compactin X S" and cont: "continuous_map X Y f"
  3542   shows "compactin Y (f ` S)"
  3543   unfolding compactin_def
  3544 proof (intro conjI allI impI)
  3545   show "f ` S \<subseteq> topspace Y"
  3546     using compactin_subset_topspace cont continuous_map_image_subset_topspace cpt by blast
  3547 next
  3548   fix \<U> :: "'b set set"
  3549   assume \<U>: "Ball \<U> (openin Y) \<and> f ` S \<subseteq> \<Union>\<U>"
  3550   define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
  3551   have "S \<subseteq> topspace X"
  3552     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>"
  3553     using cpt by (auto simp: compactin_def)
  3554   obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<V>" "S \<subseteq> \<Union>\<F>"
  3555   proof -
  3556     have 1: "\<forall>U\<in>\<V>. openin X U"
  3557       unfolding \<V>_def using \<U> cont[unfolded continuous_map] by blast
  3558     have 2: "S \<subseteq> \<Union>\<V>"
  3559       unfolding \<V>_def using compactin_subset_topspace cpt \<U> by fastforce
  3560     show thesis
  3561       using * [OF 1 2] that by metis
  3562   qed
  3563   have "\<forall>v \<in> \<V>. \<exists>U. U \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U}"
  3564     using \<V>_def by blast
  3565   then obtain U where U: "\<forall>v \<in> \<V>. U v \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U v}"
  3566     by metis
  3567   show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> f ` S \<subseteq> \<Union>\<F>"
  3568   proof (intro conjI exI)
  3569     show "finite (U ` \<F>)"
  3570       by (simp add: \<open>finite \<F>\<close>)
  3571   next
  3572     show "U ` \<F> \<subseteq> \<U>"
  3573       using \<open>\<F> \<subseteq> \<V>\<close> U by auto
  3574   next
  3575     show "f ` S \<subseteq> \<Union> (U ` \<F>)"
  3576       using \<F>(2-3) U UnionE subset_eq U by fastforce
  3577   qed
  3578 qed
  3579 
  3580 
  3581 lemma homeomorphic_compact_space:
  3582   assumes "X homeomorphic_space Y"
  3583   shows "compact_space X \<longleftrightarrow> compact_space Y"
  3584     using homeomorphic_space_sym
  3585     by (metis assms compact_space_def homeomorphic_eq_everything_map homeomorphic_space image_compactin)
  3586 
  3587 lemma homeomorphic_map_compactness:
  3588   assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  3589   shows "compactin Y (f ` U) \<longleftrightarrow> compactin X U"
  3590 proof -
  3591   have "f ` U \<subseteq> topspace Y"
  3592     using hom U homeomorphic_imp_surjective_map by blast
  3593   moreover have "homeomorphic_map (subtopology X U) (subtopology Y (f ` U)) f"
  3594     using U hom homeomorphic_imp_surjective_map by (blast intro: homeomorphic_map_subtopologies)
  3595   then have "compact_space (subtopology Y (f ` U)) = compact_space (subtopology X U)"
  3596     using homeomorphic_compact_space homeomorphic_map_imp_homeomorphic_space by blast
  3597   ultimately show ?thesis
  3598     by (simp add: compactin_subspace U)
  3599 qed
  3600 
  3601 lemma homeomorphic_map_compactness_eq:
  3602    "homeomorphic_map X Y f
  3603         \<Longrightarrow> compactin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> compactin Y (f ` U)"
  3604   by (meson compactin_subset_topspace homeomorphic_map_compactness)
  3605 
  3606 
  3607 subsection\<open>Embedding maps\<close>
  3608 
  3609 definition embedding_map
  3610   where "embedding_map X Y f \<equiv> homeomorphic_map X (subtopology Y (f ` (topspace X))) f"
  3611 
  3612 lemma embedding_map_eq:
  3613    "\<lbrakk>embedding_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> embedding_map X Y g"
  3614   unfolding embedding_map_def
  3615   by (metis homeomorphic_map_eq image_cong)
  3616 
  3617 lemma embedding_map_compose:
  3618   assumes "embedding_map X X' f" "embedding_map X' X'' g"
  3619   shows "embedding_map X X'' (g \<circ> f)"
  3620 proof -
  3621   have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g"
  3622     using assms by (auto simp: embedding_map_def)
  3623   then obtain C where "g ` topspace X' \<inter> C = (g \<circ> f) ` topspace X"
  3624     by (metis (no_types) Int_absorb1 continuous_map_image_subset_topspace continuous_map_in_subtopology homeomorphic_eq_everything_map image_comp image_mono)
  3625   then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \<circ> f) ` topspace X)) g"
  3626     by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
  3627   then show ?thesis
  3628   unfolding embedding_map_def
  3629   using hm(1) homeomorphic_map_compose by blast
  3630 qed
  3631 
  3632 lemma surjective_embedding_map:
  3633    "embedding_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
  3634   by (force simp: embedding_map_def homeomorphic_eq_everything_map)
  3635 
  3636 lemma embedding_map_in_subtopology:
  3637    "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
  3638   apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
  3639     apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
  3640   apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
  3641   done
  3642 
  3643 lemma injective_open_imp_embedding_map:
  3644    "\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
  3645   unfolding embedding_map_def
  3646   apply (rule bijective_open_imp_homeomorphic_map)
  3647   using continuous_map_in_subtopology apply blast
  3648     apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
  3649   done
  3650 
  3651 lemma injective_closed_imp_embedding_map:
  3652   "\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
  3653   unfolding embedding_map_def
  3654   apply (rule bijective_closed_imp_homeomorphic_map)
  3655      apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
  3656   apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
  3657   done
  3658 
  3659 lemma embedding_map_imp_homeomorphic_space:
  3660    "embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
  3661   unfolding embedding_map_def
  3662   using homeomorphic_space by blast
  3663 
  3664 
  3665 subsection\<open>Retraction and section maps\<close>
  3666 
  3667 definition retraction_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
  3668   where "retraction_maps X Y f g \<equiv>
  3669            continuous_map X Y f \<and> continuous_map Y X g \<and> (\<forall>x \<in> topspace Y. f(g x) = x)"
  3670 
  3671 definition section_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  3672   where "section_map X Y f \<equiv> \<exists>g. retraction_maps Y X g f"
  3673 
  3674 definition retraction_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  3675   where "retraction_map X Y f \<equiv> \<exists>g. retraction_maps X Y f g"
  3676 
  3677 lemma retraction_maps_eq:
  3678    "\<lbrakk>retraction_maps X Y f g; \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>x. x \<in> topspace Y \<Longrightarrow> g x = g' x\<rbrakk>
  3679         \<Longrightarrow> retraction_maps X Y f' g'"
  3680   unfolding retraction_maps_def by (metis (no_types, lifting) continuous_map_def continuous_map_eq)
  3681 
  3682 lemma section_map_eq:
  3683    "\<lbrakk>section_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> section_map X Y g"
  3684   unfolding section_map_def using retraction_maps_eq by blast
  3685 
  3686 lemma retraction_map_eq:
  3687    "\<lbrakk>retraction_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> retraction_map X Y g"
  3688   unfolding retraction_map_def using retraction_maps_eq by blast
  3689 
  3690 lemma homeomorphic_imp_retraction_maps:
  3691    "homeomorphic_maps X Y f g \<Longrightarrow> retraction_maps X Y f g"
  3692   by (simp add: homeomorphic_maps_def retraction_maps_def)
  3693 
  3694 lemma section_and_retraction_eq_homeomorphic_map:
  3695    "section_map X Y f \<and> retraction_map X Y f \<longleftrightarrow> homeomorphic_map X Y f"
  3696   apply (auto simp: section_map_def retraction_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def)
  3697   by (metis (full_types) continuous_map_image_subset_topspace image_subset_iff)
  3698 
  3699 lemma section_imp_embedding_map:
  3700    "section_map X Y f \<Longrightarrow> embedding_map X Y f"
  3701   unfolding section_map_def embedding_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def
  3702   by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology topspace_subtopology)
  3703 
  3704 lemma retraction_imp_quotient_map:
  3705   assumes "retraction_map X Y f"
  3706   shows "quotient_map X Y f"
  3707   unfolding quotient_map_def
  3708 proof (intro conjI subsetI allI impI)
  3709   show "f ` topspace X = topspace Y"
  3710     using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def)
  3711 next
  3712   fix U
  3713   assume U: "U \<subseteq> topspace Y"
  3714   have "openin Y U"
  3715     if "\<forall>x\<in>topspace Y. g x \<in> topspace X" "\<forall>x\<in>topspace Y. f (g x) = x"
  3716        "openin Y {x \<in> topspace Y. g x \<in> {x \<in> topspace X. f x \<in> U}}" for g
  3717     using openin_subopen U that by fastforce
  3718   then show "openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
  3719     using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def)
  3720 qed
  3721 
  3722 lemma retraction_maps_compose:
  3723    "\<lbrakk>retraction_maps X Y f f'; retraction_maps Y Z g g'\<rbrakk> \<Longrightarrow> retraction_maps X Z (g \<circ> f) (f' \<circ> g')"
  3724   by (clarsimp simp: retraction_maps_def continuous_map_compose) (simp add: continuous_map_def)
  3725 
  3726 lemma retraction_map_compose:
  3727    "\<lbrakk>retraction_map X Y f; retraction_map Y Z g\<rbrakk> \<Longrightarrow> retraction_map X Z (g \<circ> f)"
  3728   by (meson retraction_map_def retraction_maps_compose)
  3729 
  3730 lemma section_map_compose:
  3731    "\<lbrakk>section_map X Y f; section_map Y Z g\<rbrakk> \<Longrightarrow> section_map X Z (g \<circ> f)"
  3732   by (meson retraction_maps_compose section_map_def)
  3733 
  3734 lemma surjective_section_eq_homeomorphic_map:
  3735    "section_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
  3736   by (meson section_and_retraction_eq_homeomorphic_map section_imp_embedding_map surjective_embedding_map)
  3737 
  3738 lemma surjective_retraction_or_section_map:
  3739    "f ` (topspace X) = topspace Y \<Longrightarrow> retraction_map X Y f \<or> section_map X Y f \<longleftrightarrow> retraction_map X Y f"
  3740   using section_and_retraction_eq_homeomorphic_map surjective_section_eq_homeomorphic_map by fastforce
  3741 
  3742 lemma retraction_imp_surjective_map:
  3743    "retraction_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
  3744   by (simp add: retraction_imp_quotient_map quotient_imp_surjective_map)
  3745 
  3746 lemma section_imp_injective_map:
  3747    "\<lbrakk>section_map X Y f; x \<in> topspace X; y \<in> topspace X\<rbrakk> \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
  3748   by (metis (mono_tags, hide_lams) retraction_maps_def section_map_def)
  3749 
  3750 lemma retraction_maps_to_retract_maps:
  3751    "retraction_maps X Y r s
  3752         \<Longrightarrow> retraction_maps X (subtopology X (s ` (topspace Y))) (s \<circ> r) id"
  3753   unfolding retraction_maps_def
  3754   by (auto simp: continuous_map_compose continuous_map_into_subtopology continuous_map_from_subtopology)
  3755 subsection \<open>Continuity\<close>
  3756 
  3757 lemma continuous_on_open:
  3758   "continuous_on S f \<longleftrightarrow>
  3759     (\<forall>T. openin (top_of_set (f ` S)) T \<longrightarrow>
  3760       openin (top_of_set S) (S \<inter> f -` T))"
  3761   unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
  3762   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
  3763 
  3764 lemma continuous_on_closed:
  3765   "continuous_on S f \<longleftrightarrow>
  3766     (\<forall>T. closedin (top_of_set (f ` S)) T \<longrightarrow>
  3767       closedin (top_of_set S) (S \<inter> f -` T))"
  3768   unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
  3769   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
  3770 
  3771 lemma continuous_on_imp_closedin:
  3772   assumes "continuous_on S f" "closedin (top_of_set (f ` S)) T"
  3773   shows "closedin (top_of_set S) (S \<inter> f -` T)"
  3774   using assms continuous_on_closed by blast
  3775 
  3776 subsection%unimportant \<open>Half-global and completely global cases\<close>
  3777 
  3778 lemma continuous_openin_preimage_gen:
  3779   assumes "continuous_on S f"  "open T"
  3780   shows "openin (top_of_set S) (S \<inter> f -` T)"
  3781 proof -
  3782   have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
  3783     by auto
  3784   have "openin (top_of_set (f ` S)) (T \<inter> f ` S)"
  3785     using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
  3786   then show ?thesis
  3787     using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
  3788     using * by auto
  3789 qed
  3790 
  3791 lemma continuous_closedin_preimage:
  3792   assumes "continuous_on S f" and "closed T"
  3793   shows "closedin (top_of_set S) (S \<inter> f -` T)"
  3794 proof -
  3795   have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
  3796     by auto
  3797   have "closedin (top_of_set (f ` S)) (T \<inter> f ` S)"
  3798     using closedin_closed_Int[of T "f ` S", OF assms(2)]
  3799     by (simp add: Int_commute)
  3800   then show ?thesis
  3801     using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
  3802     using * by auto
  3803 qed
  3804 
  3805 lemma continuous_openin_preimage_eq:
  3806    "continuous_on S f \<longleftrightarrow>
  3807     (\<forall>T. open T \<longrightarrow> openin (top_of_set S) (S \<inter> f -` T))"
  3808 apply safe
  3809 apply (simp add: continuous_openin_preimage_gen)
  3810 apply (fastforce simp add: continuous_on_open openin_open)
  3811 done
  3812 
  3813 lemma continuous_closedin_preimage_eq:
  3814    "continuous_on S f \<longleftrightarrow>
  3815     (\<forall>T. closed T \<longrightarrow> closedin (top_of_set S) (S \<inter> f -` T))"
  3816 apply safe
  3817 apply (simp add: continuous_closedin_preimage)
  3818 apply (fastforce simp add: continuous_on_closed closedin_closed)
  3819 done
  3820 
  3821 lemma continuous_open_preimage:
  3822   assumes contf: "continuous_on S f" and "open S" "open T"
  3823   shows "open (S \<inter> f -` T)"
  3824 proof-
  3825   obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
  3826     using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
  3827     unfolding openin_open by auto
  3828   then show ?thesis
  3829     using open_Int[of S U, OF \<open>open S\<close>] by auto
  3830 qed
  3831 
  3832 lemma continuous_closed_preimage:
  3833   assumes contf: "continuous_on S f" and "closed S" "closed T"
  3834   shows "closed (S \<inter> f -` T)"
  3835 proof-
  3836   obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
  3837     using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
  3838     unfolding closedin_closed by auto
  3839   then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
  3840 qed
  3841 
  3842 lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
  3843   by (metis continuous_on_eq_continuous_within open_vimage) 
  3844  
  3845 lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
  3846   by (simp add: closed_vimage continuous_on_eq_continuous_within)
  3847 
  3848 lemma Times_in_interior_subtopology:
  3849   assumes "(x, y) \<in> U" "openin (top_of_set (S \<times> T)) U"
  3850   obtains V W where "openin (top_of_set S) V" "x \<in> V"
  3851                     "openin (top_of_set T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
  3852 proof -
  3853   from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T"
  3854     by (auto simp: openin_open)
  3855   from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>]
  3856   obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E"
  3857     by blast
  3858   show ?thesis
  3859   proof
  3860     show "openin (top_of_set S) (E1 \<inter> S)"
  3861       "openin (top_of_set T) (E2 \<inter> T)"
  3862       using \<open>open E1\<close> \<open>open E2\<close>
  3863       by (auto simp: openin_open)
  3864     show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T"
  3865       using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
  3866     show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
  3867       using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
  3868       by (auto simp: )
  3869   qed
  3870 qed
  3871 
  3872 lemma closedin_Times:
  3873   "closedin (top_of_set S) S' \<Longrightarrow> closedin (top_of_set T) T' \<Longrightarrow>
  3874     closedin (top_of_set (S \<times> T)) (S' \<times> T')"
  3875   unfolding closedin_closed using closed_Times by blast
  3876 
  3877 lemma openin_Times:
  3878   "openin (top_of_set S) S' \<Longrightarrow> openin (top_of_set T) T' \<Longrightarrow>
  3879     openin (top_of_set (S \<times> T)) (S' \<times> T')"
  3880   unfolding openin_open using open_Times by blast
  3881 
  3882 lemma openin_Times_eq:
  3883   fixes S :: "'a::topological_space set" and T :: "'b::topological_space set"
  3884   shows
  3885     "openin (top_of_set (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
  3886       S' = {} \<or> T' = {} \<or> openin (top_of_set S) S' \<and> openin (top_of_set T) T'"
  3887     (is "?lhs = ?rhs")
  3888 proof (cases "S' = {} \<or> T' = {}")
  3889   case True
  3890   then show ?thesis by auto
  3891 next
  3892   case False
  3893   then obtain x y where "x \<in> S'" "y \<in> T'"
  3894     by blast
  3895   show ?thesis
  3896   proof
  3897     assume ?lhs
  3898     have "openin (top_of_set S) S'"
  3899       apply (subst openin_subopen, clarify)
  3900       apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
  3901       using \<open>y \<in> T'\<close>
  3902        apply auto
  3903       done
  3904     moreover have "openin (top_of_set T) T'"
  3905       apply (subst openin_subopen, clarify)
  3906       apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
  3907       using \<open>x \<in> S'\<close>
  3908        apply auto
  3909       done
  3910     ultimately show ?rhs
  3911       by simp
  3912   next
  3913     assume ?rhs
  3914     with False show ?lhs
  3915       by (simp add: openin_Times)
  3916   qed
  3917 qed
  3918 
  3919 lemma Lim_transform_within_openin:
  3920   assumes f: "(f \<longlongrightarrow> l) (at a within T)"
  3921     and "openin (top_of_set T) S" "a \<in> S"
  3922     and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
  3923   shows "(g \<longlongrightarrow> l) (at a within T)"
  3924 proof -
  3925   have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a"
  3926     by (simp add: eventually_at_filter)
  3927   moreover
  3928   from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U"
  3929     by (auto simp: openin_open)
  3930   then have "a \<in> U" using \<open>a \<in> S\<close> by auto
  3931   from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>]
  3932   have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto
  3933   ultimately
  3934   have "\<forall>\<^sub>F x in at a within T. f x = g x"
  3935     by eventually_elim (auto simp: \<open>S = _\<close> eq)
  3936   then show ?thesis using f
  3937     by (rule Lim_transform_eventually)
  3938 qed
  3939 
  3940 lemma continuous_on_open_gen:
  3941   assumes "f ` S \<subseteq> T"
  3942     shows "continuous_on S f \<longleftrightarrow>
  3943              (\<forall>U. openin (top_of_set T) U
  3944                   \<longrightarrow> openin (top_of_set S) (S \<inter> f -` U))"
  3945      (is "?lhs = ?rhs")
  3946 proof
  3947   assume ?lhs
  3948   then show ?rhs
  3949     by (clarsimp simp add: continuous_openin_preimage_eq openin_open)
  3950       (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1)
  3951 next
  3952   assume R [rule_format]: ?rhs
  3953   show ?lhs
  3954   proof (clarsimp simp add: continuous_openin_preimage_eq)
  3955     fix U::"'a set"
  3956     assume "open U"
  3957     then have "openin (top_of_set S) (S \<inter> f -` (U \<inter> T))"
  3958       by (metis R inf_commute openin_open)
  3959     then show "openin (top_of_set S) (S \<inter> f -` U)"
  3960       by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int)
  3961   qed
  3962 qed
  3963 
  3964 lemma continuous_openin_preimage:
  3965   "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (top_of_set T) U\<rbrakk>
  3966         \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` U)"
  3967   by (simp add: continuous_on_open_gen)
  3968 
  3969 lemma continuous_on_closed_gen:
  3970   assumes "f ` S \<subseteq> T"
  3971   shows "continuous_on S f \<longleftrightarrow>
  3972              (\<forall>U. closedin (top_of_set T) U
  3973                   \<longrightarrow> closedin (top_of_set S) (S \<inter> f -` U))"
  3974     (is "?lhs = ?rhs")
  3975 proof -
  3976   have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
  3977     using assms by blast
  3978   show ?thesis
  3979   proof
  3980     assume L: ?lhs
  3981     show ?rhs
  3982     proof clarify
  3983       fix U
  3984       assume "closedin (top_of_set T) U"
  3985       then show "closedin (top_of_set S) (S \<inter> f -` U)"
  3986         using L unfolding continuous_on_open_gen [OF assms]
  3987         by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
  3988     qed
  3989   next
  3990     assume R [rule_format]: ?rhs
  3991     show ?lhs
  3992       unfolding continuous_on_open_gen [OF assms]
  3993       by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
  3994   qed
  3995 qed
  3996 
  3997 lemma continuous_closedin_preimage_gen:
  3998   assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (top_of_set T) U"
  3999     shows "closedin (top_of_set S) (S \<inter> f -` U)"
  4000 using assms continuous_on_closed_gen by blast
  4001 
  4002 lemma continuous_transform_within_openin:
  4003   assumes "continuous (at a within T) f"
  4004     and "openin (top_of_set T) S" "a \<in> S"
  4005     and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  4006   shows "continuous (at a within T) g"
  4007   using assms by (simp add: Lim_transform_within_openin continuous_within)
  4008 
  4009 
  4010 subsection%important \<open>The topology generated by some (open) subsets\<close>
  4011 
  4012 text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
  4013 as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
  4014 and is never a problem in proofs, so I prefer to write it down explicitly.
  4015 
  4016 We do not require \<open>UNIV\<close> to be an open set, as this will not be the case in applications. (We are
  4017 thinking of a topology on a subset of \<open>UNIV\<close>, the remaining part of \<open>UNIV\<close> being irrelevant.)\<close>
  4018 
  4019 inductive generate_topology_on for S where
  4020   Empty: "generate_topology_on S {}"
  4021 | Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
  4022 | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
  4023 | Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
  4024 
  4025 lemma istopology_generate_topology_on:
  4026   "istopology (generate_topology_on S)"
  4027 unfolding istopology_def by (auto intro: generate_topology_on.intros)
  4028 
  4029 text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
  4030 smallest topology containing all the elements of \<open>S\<close>:\<close>
  4031 
  4032 lemma generate_topology_on_coarsest:
  4033   assumes "istopology T"
  4034           "\<And>s. s \<in> S \<Longrightarrow> T s"
  4035           "generate_topology_on S s0"
  4036   shows "T s0"
  4037 using assms(3) apply (induct rule: generate_topology_on.induct)
  4038 using assms(1) assms(2) unfolding istopology_def by auto
  4039 
  4040 abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
  4041   where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
  4042 
  4043 lemma openin_topology_generated_by_iff:
  4044   "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
  4045   using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
  4046 
  4047 lemma openin_topology_generated_by:
  4048   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
  4049 using openin_topology_generated_by_iff by auto
  4050 
  4051 lemma topology_generated_by_topspace:
  4052   "topspace (topology_generated_by S) = (\<Union>S)"
  4053 proof
  4054   {
  4055     fix s assume "openin (topology_generated_by S) s"
  4056     then have "generate_topology_on S s" by (rule openin_topology_generated_by)
  4057     then have "s \<subseteq> (\<Union>S)" by (induct, auto)
  4058   }
  4059   then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
  4060     unfolding topspace_def by auto
  4061 next
  4062   have "generate_topology_on S (\<Union>S)"
  4063     using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
  4064   then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
  4065     unfolding topspace_def using openin_topology_generated_by_iff by auto
  4066 qed
  4067 
  4068 lemma topology_generated_by_Basis:
  4069   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
  4070   by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
  4071 
  4072 lemma generate_topology_on_Inter:
  4073   "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
  4074   by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
  4075 
  4076 subsection\<open>Topology bases and sub-bases\<close>
  4077 
  4078 lemma istopology_base_alt:
  4079    "istopology (arbitrary union_of P) \<longleftrightarrow>
  4080     (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
  4081            \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
  4082   by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)
  4083 
  4084 lemma istopology_base_eq:
  4085    "istopology (arbitrary union_of P) \<longleftrightarrow>
  4086     (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
  4087   by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)
  4088 
  4089 lemma istopology_base:
  4090    "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
  4091   by (simp add: arbitrary_def istopology_base_eq union_of_inc)
  4092 
  4093 lemma openin_topology_base_unique:
  4094    "openin X = arbitrary union_of P \<longleftrightarrow>
  4095         (\<forall>V. P V \<longrightarrow> openin X V) \<and> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V. P V \<and> x \<in> V \<and> V \<subseteq> U))"
  4096    (is "?lhs = ?rhs")
  4097 proof
  4098   assume ?lhs
  4099   then show ?rhs
  4100     by (auto simp: union_of_def arbitrary_def)
  4101 next
  4102   assume R: ?rhs
  4103   then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
  4104     using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
  4105   from R show ?lhs
  4106     by (fastforce simp add: union_of_def arbitrary_def intro: *)
  4107 qed
  4108 
  4109 lemma topology_base_unique:
  4110    "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
  4111      \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>
  4112     \<Longrightarrow> topology(arbitrary union_of P) = X"
  4113   by (metis openin_topology_base_unique openin_inverse [of X])
  4114 
  4115 lemma topology_bases_eq_aux:
  4116    "\<lbrakk>(arbitrary union_of P) S;
  4117      \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
  4118         \<Longrightarrow> (arbitrary union_of Q) S"
  4119   by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)
  4120 
  4121 lemma topology_bases_eq:
  4122    "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
  4123     \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
  4124         \<Longrightarrow> topology (arbitrary union_of P) =
  4125             topology (arbitrary union_of Q)"
  4126   by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)
  4127 
  4128 lemma istopology_subbase:
  4129    "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
  4130   by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)
  4131 
  4132 lemma openin_subbase:
  4133   "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
  4134    \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
  4135   by (simp add: istopology_subbase topology_inverse')
  4136 
  4137 lemma topspace_subbase [simp]:
  4138    "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
  4139 proof
  4140   show "?lhs \<subseteq> U"
  4141     by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
  4142   show "U \<subseteq> ?lhs"
  4143     by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
  4144               openin_subset relative_to_inc subset_UNIV topology_inverse')
  4145 qed
  4146 
  4147 lemma minimal_topology_subbase:
  4148    "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
  4149      openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
  4150     \<Longrightarrow> openin X S"
  4151   apply (simp add: istopology_subbase topology_inverse)
  4152   apply (simp add: union_of_def intersection_of_def relative_to_def)
  4153   apply (blast intro: openin_Int_Inter)
  4154   done
  4155 
  4156 lemma istopology_subbase_UNIV:
  4157    "istopology (arbitrary union_of (finite intersection_of P))"
  4158   by (simp add: istopology_base finite_intersection_of_Int)
  4159 
  4160 
  4161 lemma generate_topology_on_eq:
  4162   "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
  4163 proof (intro ext iffI)
  4164   fix A
  4165   assume "?lhs A"
  4166   then show "?rhs A"
  4167   proof induction
  4168     case (Int a b)
  4169     then show ?case
  4170       by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
  4171   next
  4172     case (UN K)
  4173     then show ?case
  4174       by (simp add: arbitrary_union_of_Union)
  4175   next
  4176     case (Basis s)
  4177     then show ?case
  4178       by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
  4179   qed auto
  4180 next
  4181   fix A
  4182   assume "?rhs A"
  4183   then obtain \<U> where \<U>: "\<And>T. T \<in> \<U> \<Longrightarrow> \<exists>\<F>. finite' \<F> \<and> \<F> \<subseteq> S \<and> \<Inter>\<F> = T" and eq: "A = \<Union>\<U>"
  4184     unfolding union_of_def intersection_of_def by auto
  4185   show "?lhs A"
  4186     unfolding eq
  4187   proof (rule generate_topology_on.UN)
  4188     fix T
  4189     assume "T \<in> \<U>"
  4190     with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
  4191       by blast
  4192     have "generate_topology_on S (\<Inter>\<F>)"
  4193     proof (rule generate_topology_on_Inter)
  4194       show "finite \<F>" "\<F> \<noteq> {}"
  4195         by (auto simp: \<open>finite' \<F>\<close>)
  4196       show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
  4197         by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
  4198     qed
  4199     then show "generate_topology_on S T"
  4200       using \<open>\<Inter>\<F> = T\<close> by blast
  4201   qed
  4202 qed
  4203 
  4204 lemma continuous_on_generated_topo_iff:
  4205   "continuous_map T1 (topology_generated_by S) f \<longleftrightarrow>
  4206       ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
  4207 unfolding continuous_map_alt topology_generated_by_topspace
  4208 proof (auto simp add: topology_generated_by_Basis)
  4209   assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
  4210   fix U assume "openin (topology_generated_by S) U"
  4211   then have "generate_topology_on S U" by (rule openin_topology_generated_by)
  4212   then show "openin T1 (f -` U \<inter> topspace T1)"
  4213   proof (induct)
  4214     fix a b
  4215     assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
  4216     have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
  4217       by auto
  4218     then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
  4219   next
  4220     fix K
  4221     assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
  4222     define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
  4223     have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
  4224     have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
  4225     moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
  4226     ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
  4227   qed (auto simp add: H)
  4228 qed
  4229 
  4230 lemma continuous_on_generated_topo:
  4231   assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
  4232           "f`(topspace T1) \<subseteq> (\<Union> S)"
  4233   shows "continuous_map T1 (topology_generated_by S) f"
  4234   using assms continuous_on_generated_topo_iff by blast
  4235 
  4236 
  4237 subsection%important \<open>Pullback topology\<close>
  4238 
  4239 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
  4240 a special case of this notion, pulling back by the identity. We introduce the general notion as
  4241 we will need it to define the strong operator topology on the space of continuous linear operators,
  4242 by pulling back the product topology on the space of all functions.\<close>
  4243 
  4244 text \<open>\<open>pullback_topology A f T\<close> is the pullback of the topology \<open>T\<close> by the map \<open>f\<close> on
  4245 the set \<open>A\<close>.\<close>
  4246 
  4247 definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
  4248   where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
  4249 
  4250 lemma istopology_pullback_topology:
  4251   "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
  4252   unfolding istopology_def proof (auto)
  4253   fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
  4254   then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
  4255     by (rule bchoice)
  4256   then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
  4257     by blast
  4258   define V where "V = (\<Union>S\<in>K. U S)"
  4259   have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
  4260   then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
  4261 qed
  4262 
  4263 lemma openin_pullback_topology:
  4264   "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
  4265 unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
  4266 
  4267 lemma topspace_pullback_topology:
  4268   "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
  4269 by (auto simp add: topspace_def openin_pullback_topology)
  4270 
  4271 proposition continuous_map_pullback [intro]:
  4272   assumes "continuous_map T1 T2 g"
  4273   shows "continuous_map (pullback_topology A f T1) T2 (g o f)"
  4274 unfolding continuous_map_alt
  4275 proof (auto)
  4276   fix U::"'b set" assume "openin T2 U"
  4277   then have "openin T1 (g-`U \<inter> topspace T1)"
  4278     using assms unfolding continuous_map_alt by auto
  4279   have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
  4280     unfolding topspace_pullback_topology by auto
  4281   also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
  4282     by auto
  4283   also have "openin (pullback_topology A f T1) (...)"
  4284     unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
  4285   finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
  4286     by auto
  4287 next
  4288   fix x assume "x \<in> topspace (pullback_topology A f T1)"
  4289   then have "f x \<in> topspace T1"
  4290     unfolding topspace_pullback_topology by auto
  4291   then show "g (f x) \<in> topspace T2"
  4292     using assms unfolding continuous_map_def by auto
  4293 qed
  4294 
  4295 proposition continuous_map_pullback' [intro]:
  4296   assumes "continuous_map T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
  4297   shows "continuous_map T1 (pullback_topology A f T2) g"
  4298 unfolding continuous_map_alt
  4299 proof (auto)
  4300   fix U assume "openin (pullback_topology A f T2) U"
  4301   then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
  4302     unfolding openin_pullback_topology by auto
  4303   then obtain V where "openin T2 V" "U = f-`V \<inter> A"
  4304     by blast
  4305   then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
  4306     by blast
  4307   also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
  4308     by auto
  4309   also have "... = (f o g)-`V \<inter> topspace T1"
  4310     using assms(2) by auto
  4311   also have "openin T1 (...)"
  4312     using assms(1) \<open>openin T2 V\<close> by auto
  4313   finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
  4314 next
  4315   fix x assume "x \<in> topspace T1"
  4316   have "(f o g) x \<in> topspace T2"
  4317     using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
  4318   then have "g x \<in> f-`(topspace T2)"
  4319     unfolding comp_def by blast
  4320   moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
  4321   ultimately show "g x \<in> topspace (pullback_topology A f T2)"
  4322     unfolding topspace_pullback_topology by blast
  4323 qed
  4324 
  4325 end