src/HOL/Analysis/Abstract_Topology.thy

new material about topology, etc.; also fixes for yesterday's

(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light]
*)

section \<open>Operators involving abstract topology\<close>

theory Abstract_Topology
  imports
    Complex_Main
    "HOL-Library.Set_Idioms"
    "HOL-Library.FuncSet"
begin

subsection \<open>General notion of a topology as a value\<close>

definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
"istopology L \<longleftrightarrow>
  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))"

typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
  morphisms "openin" "topology"
  unfolding istopology_def by blast

lemma istopology_openin[intro]: "istopology(openin U)"
  using openin[of U] by blast

lemma istopology_open: "istopology open"
  by (auto simp: istopology_def)

lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
  using topology_inverse[unfolded mem_Collect_eq] .

lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
  using topology_inverse[of U] istopology_openin[of "topology U"] by auto

lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
proof
  assume "T1 = T2"
  then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
next
  assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
  then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
  then have "topology (openin T1) = topology (openin T2)" by simp
  then show "T1 = T2" unfolding openin_inverse .
qed


text\<open>The "universe": the union of all sets in the topology.\<close>
definition "topspace T = \<Union>{S. openin T S}"

subsubsection \<open>Main properties of open sets\<close>

proposition openin_clauses:
  fixes U :: "'a topology"
  shows
    "openin U {}"
    "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
    "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
  using openin[of U] unfolding istopology_def mem_Collect_eq by fast+

lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
  unfolding topspace_def by blast

lemma openin_empty[simp]: "openin U {}"
  by (rule openin_clauses)

lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
  by (rule openin_clauses)

lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)"
  using openin_clauses by blast

lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
  using openin_Union[of "{S,T}" U] by auto

lemma openin_topspace[intro, simp]: "openin U (topspace U)"
  by (force simp: openin_Union topspace_def)

lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
  (is "?lhs \<longleftrightarrow> ?rhs")
proof
  assume ?lhs
  then show ?rhs by auto
next
  assume H: ?rhs
  let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
  have "openin U ?t" by (force simp: openin_Union)
  also have "?t = S" using H by auto
  finally show "openin U S" .
qed

lemma openin_INT [intro]:
  assumes "finite I"
          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
  shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)

lemma openin_INT2 [intro]:
  assumes "finite I" "I \<noteq> {}"
          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
  shows "openin T (\<Inter>i \<in> I. U i)"
proof -
  have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
    using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
  then show ?thesis
    using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
qed

lemma openin_Inter [intro]:
  assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
  by (metis (full_types) assms openin_INT2 image_ident)

lemma openin_Int_Inter:
  assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
  using openin_Inter [of "insert U \<F>"] assms by auto


subsubsection \<open>Closed sets\<close>

definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
"closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"

lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
  by (metis closedin_def)

lemma closedin_empty[simp]: "closedin U {}"
  by (simp add: closedin_def)

lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
  by (simp add: closedin_def)

lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
  by (auto simp: Diff_Un closedin_def)

lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
  by auto

lemma closedin_Union:
  assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T"
    shows "closedin U (\<Union>S)"
  using assms by induction auto

lemma closedin_Inter[intro]:
  assumes Ke: "K \<noteq> {}"
    and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
  shows "closedin U (\<Inter>K)"
  using Ke Kc unfolding closedin_def Diff_Inter by auto

lemma closedin_INT[intro]:
  assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
  shows "closedin U (\<Inter>x\<in>A. B x)"
  apply (rule closedin_Inter)
  using assms
  apply auto
  done

lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
  using closedin_Inter[of "{S,T}" U] by auto

lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
  apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2)
  apply (metis openin_subset subset_eq)
  done

lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
  by (simp add: openin_closedin_eq)

lemma openin_diff[intro]:
  assumes oS: "openin U S"
    and cT: "closedin U T"
  shows "openin U (S - T)"
proof -
  have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
    by (auto simp: topspace_def openin_subset)
  then show ?thesis using oS cT
    by (auto simp: closedin_def)
qed

lemma closedin_diff[intro]:
  assumes oS: "closedin U S"
    and cT: "openin U T"
  shows "closedin U (S - T)"
proof -
  have "S - T = S \<inter> (topspace U - T)"
    using closedin_subset[of U S] oS cT by (auto simp: topspace_def)
  then show ?thesis
    using oS cT by (auto simp: openin_closedin_eq)
qed


subsection\<open>The discrete topology\<close>

definition discrete_topology where "discrete_topology U \<equiv> topology (\<lambda>S. S \<subseteq> U)"

lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
proof -
  have "istopology (\<lambda>S. S \<subseteq> U)"
    by (auto simp: istopology_def)
  then show ?thesis
    by (simp add: discrete_topology_def topology_inverse')
qed

lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U"
  by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)

lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
  by (simp add: closedin_def)

lemma discrete_topology_unique:
   "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
proof
  assume R: ?rhs
  then have "openin X S" if "S \<subseteq> U" for S
    using openin_subopen subsetD that by fastforce
  moreover have "x \<in> topspace X" if "openin X S" and "x \<in> S" for x S
    using openin_subset that by blast
  ultimately
  show ?lhs
    using R by (auto simp: topology_eq)
qed auto

lemma discrete_topology_unique_alt:
  "discrete_topology U = X \<longleftrightarrow> topspace X \<subseteq> U \<and> (\<forall>x \<in> U. openin X {x})"
  using openin_subset
  by (auto simp: discrete_topology_unique)

lemma subtopology_eq_discrete_topology_empty:
   "X = discrete_topology {} \<longleftrightarrow> topspace X = {}"
  using discrete_topology_unique [of "{}" X] by auto

lemma subtopology_eq_discrete_topology_sing:
   "X = discrete_topology {a} \<longleftrightarrow> topspace X = {a}"
  by (metis discrete_topology_unique openin_topspace singletonD)


subsection \<open>Subspace topology\<close>

definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
"subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"

lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
  (is "istopology ?L")
proof -
  have "?L {}" by blast
  {
    fix A B
    assume A: "?L A" and B: "?L B"
    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"
      by blast
    have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
      using Sa Sb by blast+
    then have "?L (A \<inter> B)" by blast
  }
  moreover
  {
    fix K
    assume K: "K \<subseteq> Collect ?L"
    have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
      by blast
    from K[unfolded th0 subset_image_iff]
    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
      by blast
    have "\<Union>K = (\<Union>Sk) \<inter> V"
      using Sk by auto
    moreover have "openin U (\<Union>Sk)"
      using Sk by (auto simp: subset_eq)
    ultimately have "?L (\<Union>K)" by blast
  }
  ultimately show ?thesis
    unfolding subset_eq mem_Collect_eq istopology_def by auto
qed

lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
  unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
  by auto

lemma openin_subtopology_Int:
   "openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
  using openin_subtopology by auto

lemma openin_subtopology_Int2:
   "openin X T \<Longrightarrow> openin (subtopology X S) (S \<inter> T)"
  using openin_subtopology by auto

lemma openin_subtopology_diff_closed:
   "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> openin (subtopology X S) (S - T)"
  unfolding closedin_def openin_subtopology
  by (rule_tac x="topspace X - T" in exI) auto

lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
  by (force simp: relative_to_def openin_subtopology)

lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U \<inter> V"
  by (auto simp: topspace_def openin_subtopology)

lemma topspace_subtopology_subset:
   "S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
  by (simp add: inf.absorb_iff2 topspace_subtopology)

lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
  unfolding closedin_def topspace_subtopology
  by (auto simp: openin_subtopology)

lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
  unfolding openin_subtopology
  by auto (metis IntD1 in_mono openin_subset)

lemma subtopology_subtopology:
   "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
proof -
  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)"
    by (metis inf_assoc)
  have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
    by (simp add: subtopology_def)
  also have "\<dots> = subtopology X (S \<inter> T)"
    by (simp add: openin_subtopology eq) (simp add: subtopology_def)
  finally show ?thesis .
qed

lemma openin_subtopology_alt:
     "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
  by (simp add: image_iff inf_commute openin_subtopology)

lemma closedin_subtopology_alt:
     "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
  by (simp add: image_iff inf_commute closedin_subtopology)

lemma subtopology_superset:
  assumes UV: "topspace U \<subseteq> V"
  shows "subtopology U V = U"
proof -
  {
    fix S
    {
      fix T
      assume T: "openin U T" "S = T \<inter> V"
      from T openin_subset[OF T(1)] UV have eq: "S = T"
        by blast
      have "openin U S"
        unfolding eq using T by blast
    }
    moreover
    {
      assume S: "openin U S"
      then have "\<exists>T. openin U T \<and> S = T \<inter> V"
        using openin_subset[OF S] UV by auto
    }
    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
      by blast
  }
  then show ?thesis
    unfolding topology_eq openin_subtopology by blast
qed

lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
  by (simp add: subtopology_superset)

lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
  by (simp add: subtopology_superset)

lemma subtopology_restrict:
   "subtopology X (topspace X \<inter> S) = subtopology X S"
  by (metis subtopology_subtopology subtopology_topspace)

lemma openin_subtopology_empty:
   "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
by (metis Int_empty_right openin_empty openin_subtopology)

lemma closedin_subtopology_empty:
   "closedin (subtopology U {}) S \<longleftrightarrow> S = {}"
by (metis Int_empty_right closedin_empty closedin_subtopology)

lemma closedin_subtopology_refl [simp]:
   "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)

lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
  by (simp add: closedin_def)

lemma openin_imp_subset:
   "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (metis Int_iff openin_subtopology subsetI)

lemma closedin_imp_subset:
   "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (simp add: closedin_def topspace_subtopology)

lemma openin_open_subtopology:
     "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
  by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)

lemma closedin_closed_subtopology:
     "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
  by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)

lemma openin_subtopology_Un:
    "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
     \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
by (simp add: openin_subtopology) blast

lemma closedin_subtopology_Un:
    "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
     \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
by (simp add: closedin_subtopology) blast

lemma openin_trans_full:
   "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
  by (simp add: openin_open_subtopology)


subsection \<open>The canonical topology from the underlying type class\<close>

abbreviation%important euclidean :: "'a::topological_space topology"
  where "euclidean \<equiv> topology open"

abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
  where "top_of_set \<equiv> subtopology (topology open)"

lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
  apply (rule cong[where x=S and y=S])
  apply (rule topology_inverse[symmetric])
  apply (auto simp: istopology_def)
  done

declare open_openin [symmetric, simp]

lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
  by (force simp: topspace_def)

lemma topspace_euclidean_subtopology[simp]: "topspace (top_of_set S) = S"
  by (simp add: topspace_subtopology)

lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
  by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)

declare closed_closedin [symmetric, simp]

lemma openin_subtopology_self [simp]: "openin (top_of_set S) S"
  by (metis openin_topspace topspace_euclidean_subtopology)

subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>

abbreviation euclideanreal :: "real topology"
  where "euclideanreal \<equiv> topology open"

subsection \<open>Basic "localization" results are handy for connectedness.\<close>

lemma openin_open: "openin (top_of_set U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
  by (auto simp: openin_subtopology)

lemma openin_Int_open:
   "\<lbrakk>openin (top_of_set U) S; open T\<rbrakk>
        \<Longrightarrow> openin (top_of_set U) (S \<inter> T)"
by (metis open_Int Int_assoc openin_open)

lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (top_of_set U) (U \<inter> S)"
  by (auto simp: openin_open)

lemma open_openin_trans[trans]:
  "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (top_of_set S) T"
  by (metis Int_absorb1  openin_open_Int)

lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (top_of_set T) S"
  by (auto simp: openin_open)

lemma closedin_closed: "closedin (top_of_set U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
  by (simp add: closedin_subtopology Int_ac)

lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (top_of_set U) (U \<inter> S)"
  by (metis closedin_closed)

lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (top_of_set T) S"
  by (auto simp: closedin_closed)

lemma closedin_closed_subset:
 "\<lbrakk>closedin (top_of_set U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
             \<Longrightarrow> closedin (top_of_set T) S"
  by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)

lemma finite_imp_closedin:
  fixes S :: "'a::t1_space set"
  shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (top_of_set T) S"
    by (simp add: finite_imp_closed closed_subset)

lemma closedin_singleton [simp]:
  fixes a :: "'a::t1_space"
  shows "closedin (top_of_set U) {a} \<longleftrightarrow> a \<in> U"
using closedin_subset  by (force intro: closed_subset)

lemma openin_euclidean_subtopology_iff:
  fixes S U :: "'a::metric_space set"
  shows "openin (top_of_set U) S \<longleftrightarrow>
    S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
  (is "?lhs \<longleftrightarrow> ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding openin_open open_dist by blast
next
  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}"
  have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
    unfolding T_def
    apply clarsimp
    apply (rule_tac x="d - dist x a" in exI)
    apply (clarsimp simp add: less_diff_eq)
    by (metis dist_commute dist_triangle_lt)
  assume ?rhs then have 2: "S = U \<inter> T"
    unfolding T_def
    by auto (metis dist_self)
  from 1 2 show ?lhs
    unfolding openin_open open_dist by fast
qed

lemma connected_openin:
      "connected S \<longleftrightarrow>
       \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
                 openin (top_of_set S) E2 \<and>
                 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
  apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
  by (simp_all, blast+)  (* SLOW *)

lemma connected_openin_eq:
      "connected S \<longleftrightarrow>
       \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
                 openin (top_of_set S) E2 \<and>
                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
  apply (simp add: connected_openin, safe, blast)
  by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)

lemma connected_closedin:
      "connected S \<longleftrightarrow>
       (\<nexists>E1 E2.
        closedin (top_of_set S) E1 \<and>
        closedin (top_of_set S) E2 \<and>
        S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
       (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs 
    by (auto simp add: connected_closed closedin_closed)
next
  assume R: ?rhs
  then show ?lhs 
  proof (clarsimp simp add: connected_closed closedin_closed)
    fix A B 
    assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
      and disj: "A \<inter> B \<inter> S = {}"
      and cl: "closed A" "closed B"
    have "S \<inter> (A \<union> B) = S"
      using s_sub(1) by auto
    have "S - A = B \<inter> S"
      using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
    then have "S \<inter> A = {}"
      by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
    then show "A \<inter> S = {}"
      by blast
  qed
qed

lemma connected_closedin_eq:
      "connected S \<longleftrightarrow>
           \<not>(\<exists>E1 E2.
                 closedin (top_of_set S) E1 \<and>
                 closedin (top_of_set S) E2 \<and>
                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
  apply (simp add: connected_closedin, safe, blast)
  by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)

text \<open>These "transitivity" results are handy too\<close>

lemma openin_trans[trans]:
  "openin (top_of_set T) S \<Longrightarrow> openin (top_of_set U) T \<Longrightarrow>
    openin (top_of_set U) S"
  by (metis openin_Int_open openin_open)

lemma openin_open_trans: "openin (top_of_set T) S \<Longrightarrow> open T \<Longrightarrow> open S"
  by (auto simp: openin_open intro: openin_trans)

lemma closedin_trans[trans]:
  "closedin (top_of_set T) S \<Longrightarrow> closedin (top_of_set U) T \<Longrightarrow>
    closedin (top_of_set U) S"
  by (auto simp: closedin_closed closed_Inter Int_assoc)

lemma closedin_closed_trans: "closedin (top_of_set T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
  by (auto simp: closedin_closed intro: closedin_trans)

lemma openin_subtopology_Int_subset:
   "\<lbrakk>openin (top_of_set u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (top_of_set v) (v \<inter> S)"
  by (auto simp: openin_subtopology)

lemma openin_open_eq: "open s \<Longrightarrow> (openin (top_of_set s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
  using open_subset openin_open_trans openin_subset by fastforce


subsection\<open>Derived set (set of limit points)\<close>

definition derived_set_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "derived'_set'_of" 80)
  where "X derived_set_of S \<equiv>
         {x \<in> topspace X.
                (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"

lemma derived_set_of_restrict [simp]:
   "X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
  by (simp add: derived_set_of_def) (metis openin_subset subset_iff)

lemma in_derived_set_of:
   "x \<in> X derived_set_of S \<longleftrightarrow> x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))"
  by (simp add: derived_set_of_def)

lemma derived_set_of_subset_topspace:
   "X derived_set_of S \<subseteq> topspace X"
  by (auto simp add: derived_set_of_def)

lemma derived_set_of_subtopology:
   "(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
  by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast

lemma derived_set_of_subset_subtopology:
   "(subtopology X S) derived_set_of T \<subseteq> S"
  by (simp add: derived_set_of_subtopology)

lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}"
  by (auto simp: derived_set_of_def)

lemma derived_set_of_mono:
   "S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
  unfolding derived_set_of_def by blast

lemma derived_set_of_Un:
   "X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
proof
  show "?lhs \<subseteq> ?rhs"
    apply (clarsimp simp: in_derived_set_of)
    by (metis IntE IntI openin_Int)
  show "?rhs \<subseteq> ?lhs"
    by (simp add: derived_set_of_mono)
qed

lemma derived_set_of_Union:
   "finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
proof (induction \<F> rule: finite_induct)
  case (insert S \<F>)
  then show ?case
    by (simp add: derived_set_of_Un)
qed auto

lemma derived_set_of_topspace:
  "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
  apply (auto simp: in_derived_set_of)
  by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)

lemma discrete_topology_unique_derived_set:
     "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
  by (auto simp: discrete_topology_unique derived_set_of_topspace)

lemma subtopology_eq_discrete_topology_eq:
   "subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
  using discrete_topology_unique_derived_set [of U "subtopology X U"]
  by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)

lemma subtopology_eq_discrete_topology:
   "S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
        \<Longrightarrow> subtopology X S = discrete_topology S"
  by (simp add: subtopology_eq_discrete_topology_eq)

lemma subtopology_eq_discrete_topology_gen:
   "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
  by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)

lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
proof -
  have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
    by force
  then show ?thesis
    by (simp add: subtopology_def) (simp add: discrete_topology_def)
qed
lemma openin_Int_derived_set_of_subset:
   "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
  by (auto simp: derived_set_of_def)

lemma openin_Int_derived_set_of_eq:
  "openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
  apply auto
   apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
  by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)


subsection\<open> Closure with respect to a topological space\<close>

definition closure_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "closure'_of" 80)
  where "X closure_of S \<equiv> {x \<in> topspace X. \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y \<in> S. y \<in> T)}"

lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
  unfolding closure_of_def
  apply safe
  apply (meson IntI openin_subset subset_iff)
  by auto

lemma in_closure_of:
   "x \<in> X closure_of S \<longleftrightarrow>
    x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
  by (auto simp: closure_of_def)

lemma closure_of: "X closure_of S = topspace X \<inter> (S \<union> X derived_set_of S)"
  by (fastforce simp: in_closure_of in_derived_set_of)

lemma closure_of_alt: "X closure_of S = topspace X \<inter> S \<union> X derived_set_of S"
  using derived_set_of_subset_topspace [of X S]
  unfolding closure_of_def in_derived_set_of
  by safe (auto simp: in_derived_set_of)

lemma derived_set_of_subset_closure_of:
   "X derived_set_of S \<subseteq> X closure_of S"
  by (fastforce simp: closure_of_def in_derived_set_of)

lemma closure_of_subtopology:
  "(subtopology X U) closure_of S = U \<inter> (X closure_of (U \<inter> S))"
  unfolding closure_of_def topspace_subtopology openin_subtopology
  by safe (metis (full_types) IntI Int_iff inf.commute)+

lemma closure_of_empty [simp]: "X closure_of {} = {}"
  by (simp add: closure_of_alt)

lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"
  by (simp add: closure_of)

lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"
  by (simp add: closure_of)

lemma closure_of_subset_topspace: "X closure_of S \<subseteq> topspace X"
  by (simp add: closure_of)

lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T \<subseteq> S"
  by (simp add: closure_of_subtopology)

lemma closure_of_mono: "S \<subseteq> T \<Longrightarrow> X closure_of S \<subseteq> X closure_of T"
  by (fastforce simp add: closure_of_def)

lemma closure_of_subtopology_subset:
   "(subtopology X U) closure_of S \<subseteq> (X closure_of S)"
  unfolding closure_of_subtopology
  by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2)

lemma closure_of_subtopology_mono:
   "T \<subseteq> U \<Longrightarrow> (subtopology X T) closure_of S \<subseteq> (subtopology X U) closure_of S"
  unfolding closure_of_subtopology
  by auto (meson closure_of_mono inf_mono subset_iff)

lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
  by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_Un inf_sup_distrib1)

lemma closure_of_Union:
   "finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
by (induction \<F> rule: finite_induct) auto

lemma closure_of_subset: "S \<subseteq> topspace X \<Longrightarrow> S \<subseteq> X closure_of S"
  by (auto simp: closure_of_def)

lemma closure_of_subset_Int: "topspace X \<inter> S \<subseteq> X closure_of S"
  by (auto simp: closure_of_def)

lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
proof (cases "S \<subseteq> topspace X")
  case True
  then have "\<forall>x. x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<in>S. y \<in> T)) \<longrightarrow> x \<in> S
             \<Longrightarrow> openin X (topspace X - S)"
    apply (subst openin_subopen, safe)
    by (metis DiffI subset_eq openin_subset [of X])
  then show ?thesis
    by (auto simp: closedin_def closure_of_def)
next
  case False
  then show ?thesis
    by (simp add: closedin_def)
qed

lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
proof (cases "S \<subseteq> topspace X")
  case True
  then show ?thesis
    by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
next
  case False
  then show ?thesis
    using closure_of closure_of_subset_eq by fastforce
qed

lemma closedin_contains_derived_set:
   "closedin X S \<longleftrightarrow> X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X"
proof (intro iffI conjI)
  show "closedin X S \<Longrightarrow> X derived_set_of S \<subseteq> S"
    using closure_of_eq derived_set_of_subset_closure_of by fastforce
  show "closedin X S \<Longrightarrow> S \<subseteq> topspace X"
    using closedin_subset by blast
  show "X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X \<Longrightarrow> closedin X S"
    by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
qed

lemma derived_set_subset_gen:
   "X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X (topspace X \<inter> S)"
  by (simp add: closedin_contains_derived_set derived_set_of_restrict derived_set_of_subset_topspace)

lemma derived_set_subset: "S \<subseteq> topspace X \<Longrightarrow> (X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X S)"
  by (simp add: closedin_contains_derived_set)

lemma closedin_derived_set:
     "closedin (subtopology X T) S \<longleftrightarrow>
      S \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> S)"
  by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)

lemma closedin_Int_closure_of:
     "closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
  by (metis Int_left_absorb closure_of_eq closure_of_subtopology)

lemma closure_of_closedin: "closedin X S \<Longrightarrow> X closure_of S = S"
  by (simp add: closure_of_eq)

lemma closure_of_eq_diff: "X closure_of S = topspace X - \<Union>{T. openin X T \<and> disjnt S T}"
  by (auto simp: closure_of_def disjnt_iff)

lemma closedin_closure_of [simp]: "closedin X (X closure_of S)"
  unfolding closure_of_eq_diff by blast

lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S"
  by (simp add: closure_of_eq)

lemma closure_of_hull:
  assumes "S \<subseteq> topspace X" shows "X closure_of S = (closedin X) hull S"
proof (rule hull_unique [THEN sym])
  show "S \<subseteq> X closure_of S"
    by (simp add: closure_of_subset assms)
next
  show "closedin X (X closure_of S)"
    by simp
  show "\<And>T. \<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> X closure_of S \<subseteq> T"
    by (metis closure_of_eq closure_of_mono)
qed

lemma closure_of_minimal:
   "\<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T"
  by (metis closure_of_eq closure_of_mono)

lemma closure_of_minimal_eq:
   "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T \<longleftrightarrow> S \<subseteq> T"
  by (meson closure_of_minimal closure_of_subset subset_trans)

lemma closure_of_unique:
   "\<lbrakk>S \<subseteq> T; closedin X T;
     \<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
    \<Longrightarrow> X closure_of S = T"
  by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)

lemma closure_of_eq_empty_gen: "X closure_of S = {} \<longleftrightarrow> disjnt (topspace X) S"
  unfolding disjnt_def closure_of_restrict [where S=S]
  using closure_of by fastforce

lemma closure_of_eq_empty: "S \<subseteq> topspace X \<Longrightarrow> X closure_of S = {} \<longleftrightarrow> S = {}"
  using closure_of_subset by fastforce

lemma openin_Int_closure_of_subset:
  assumes "openin X S"
  shows "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
proof -
  have "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
    by (meson assms openin_Int_derived_set_of_eq)
  moreover have "S \<inter> (S \<inter> T) = S \<inter> T"
    by fastforce
  ultimately show ?thesis
    by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1)
qed

lemma closure_of_openin_Int_closure_of:
  assumes "openin X S"
  shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)"
proof
  show "X closure_of (S \<inter> X closure_of T) \<subseteq> X closure_of (S \<inter> T)"
    by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
next
  show "X closure_of (S \<inter> T) \<subseteq> X closure_of (S \<inter> X closure_of T)"
    by (metis Int_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
qed

lemma openin_Int_closure_of_eq:
  "openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
  apply (rule equalityI)
   apply (simp add: openin_Int_closure_of_subset)
  by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)

lemma openin_Int_closure_of_eq_empty:
   "openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
  apply (subst openin_Int_closure_of_eq, auto)
  by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)

lemma closure_of_openin_Int_superset:
   "openin X S \<and> S \<subseteq> X closure_of T
        \<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
  by (metis closure_of_openin_Int_closure_of inf.orderE)

lemma closure_of_openin_subtopology_Int_closure_of:
  assumes S: "openin (subtopology X U) S" and "T \<subseteq> U"
  shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
proof
  obtain S0 where S0: "openin X S0" "S = S0 \<inter> U"
    using assms by (auto simp: openin_subtopology)
  show "?lhs \<subseteq> ?rhs"
  proof -
    have "S0 \<inter> X closure_of T = S0 \<inter> X closure_of (S0 \<inter> T)"
      by (meson S0(1) openin_Int_closure_of_eq)
    moreover have "S0 \<inter> T = S0 \<inter> U \<inter> T"
      using \<open>T \<subseteq> U\<close> by fastforce
    ultimately have "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
      using S0(2) by auto
    then show ?thesis
      by (meson closedin_closure_of closure_of_minimal)
  qed
next
  show "?rhs \<subseteq> ?lhs"
  proof -
    have "T \<inter> S \<subseteq> T \<union> X derived_set_of T"
      by force
    then show ?thesis
      by (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
  qed
qed

lemma closure_of_subtopology_open:
     "openin X U \<or> S \<subseteq> U \<Longrightarrow> (subtopology X U) closure_of S = U \<inter> X closure_of S"
  by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq)

lemma discrete_topology_closure_of:
     "(discrete_topology U) closure_of S = U \<inter> S"
  by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)


text\<open> Interior with respect to a topological space.                             \<close>

definition interior_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "interior'_of" 80)
  where "X interior_of S \<equiv> {x. \<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> S}"

lemma interior_of_restrict:
   "X interior_of S = X interior_of (topspace X \<inter> S)"
  using openin_subset by (auto simp: interior_of_def)

lemma interior_of_eq: "(X interior_of S = S) \<longleftrightarrow> openin X S"
  unfolding interior_of_def  using openin_subopen by blast

lemma interior_of_openin: "openin X S \<Longrightarrow> X interior_of S = S"
  by (simp add: interior_of_eq)

lemma interior_of_empty [simp]: "X interior_of {} = {}"
  by (simp add: interior_of_eq)

lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X"
  by (simp add: interior_of_eq)

lemma openin_interior_of [simp]: "openin X (X interior_of S)"
  unfolding interior_of_def
  using openin_subopen by fastforce

lemma interior_of_interior_of [simp]:
   "X interior_of X interior_of S = X interior_of S"
  by (simp add: interior_of_eq)

lemma interior_of_subset: "X interior_of S \<subseteq> S"
  by (auto simp: interior_of_def)

lemma interior_of_subset_closure_of: "X interior_of S \<subseteq> X closure_of S"
  by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset)

lemma subset_interior_of_eq: "S \<subseteq> X interior_of S \<longleftrightarrow> openin X S"
  by (metis interior_of_eq interior_of_subset subset_antisym)

lemma interior_of_mono: "S \<subseteq> T \<Longrightarrow> X interior_of S \<subseteq> X interior_of T"
  by (auto simp: interior_of_def)

lemma interior_of_maximal: "\<lbrakk>T \<subseteq> S; openin X T\<rbrakk> \<Longrightarrow> T \<subseteq> X interior_of S"
  by (auto simp: interior_of_def)

lemma interior_of_maximal_eq: "openin X T \<Longrightarrow> T \<subseteq> X interior_of S \<longleftrightarrow> T \<subseteq> S"
  by (meson interior_of_maximal interior_of_subset order_trans)

lemma interior_of_unique:
   "\<lbrakk>T \<subseteq> S; openin X T; \<And>T'. \<lbrakk>T' \<subseteq> S; openin X T'\<rbrakk> \<Longrightarrow> T' \<subseteq> T\<rbrakk> \<Longrightarrow> X interior_of S = T"
  by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym)

lemma interior_of_subset_topspace: "X interior_of S \<subseteq> topspace X"
  by (simp add: openin_subset)

lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
  by (meson openin_imp_subset openin_interior_of)

lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
  apply (rule equalityI)
   apply (simp add: interior_of_mono)
  apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
  done

lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
  by (simp add: INT_greatest Inf_lower interior_of_mono)

lemma union_interior_of_subset:
   "X interior_of S \<union> X interior_of T \<subseteq> X interior_of (S \<union> T)"
  by (simp add: interior_of_mono)

lemma interior_of_eq_empty:
   "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<subseteq> S \<longrightarrow> T = {})"
  by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of)

lemma interior_of_eq_empty_alt:
   "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> T - S \<noteq> {})"
  by (auto simp: interior_of_eq_empty)

lemma interior_of_Union_openin_subsets:
   "\<Union>{T. openin X T \<and> T \<subseteq> S} = X interior_of S"
  by (rule interior_of_unique [symmetric]) auto

lemma interior_of_complement:
   "X interior_of (topspace X - S) = topspace X - X closure_of S"
  by (auto simp: interior_of_def closure_of_def)

lemma interior_of_closure_of:
   "X interior_of S = topspace X - X closure_of (topspace X - S)"
  unfolding interior_of_complement [symmetric]
  by (metis Diff_Diff_Int interior_of_restrict)

lemma closure_of_interior_of:
   "X closure_of S = topspace X - X interior_of (topspace X - S)"
  by (simp add: interior_of_complement Diff_Diff_Int closure_of)

lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S"
  unfolding interior_of_def closure_of_def
  by (blast dest: openin_subset)

lemma interior_of_eq_empty_complement:
  "X interior_of S = {} \<longleftrightarrow> X closure_of (topspace X - S) = topspace X"
  using interior_of_subset_topspace [of X S] closure_of_complement by fastforce

lemma closure_of_eq_topspace:
   "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
  using closure_of_subset_topspace [of X S] interior_of_complement by fastforce

lemma interior_of_subtopology_subset:
     "U \<inter> X interior_of S \<subseteq> (subtopology X U) interior_of S"
  by (auto simp: interior_of_def openin_subtopology)

lemma interior_of_subtopology_subsets:
   "T \<subseteq> U \<Longrightarrow> T \<inter> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
  by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)

lemma interior_of_subtopology_mono:
   "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
  by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets)

lemma interior_of_subtopology_open:
  assumes "openin X U"
  shows "(subtopology X U) interior_of S = U \<inter> X interior_of S"
proof -
  have "\<forall>A. U \<inter> X closure_of (U \<inter> A) = U \<inter> X closure_of A"
    using assms openin_Int_closure_of_eq by blast
  then have "topspace X \<inter> U - U \<inter> X closure_of (topspace X \<inter> U - S) = U \<inter> (topspace X - X closure_of (topspace X - S))"
    by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
  then show ?thesis
    unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
    using openin_Int_closure_of_eq [OF assms]
    by (metis assms closure_of_subtopology_open)
qed

lemma dense_intersects_open:
   "X closure_of S = topspace X \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
proof -
  have "X closure_of S = topspace X \<longleftrightarrow> (topspace X - X interior_of (topspace X - S) = topspace X)"
    by (simp add: closure_of_interior_of)
  also have "\<dots> \<longleftrightarrow> X interior_of (topspace X - S) = {}"
    by (simp add: closure_of_complement interior_of_eq_empty_complement)
  also have "\<dots> \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
    unfolding interior_of_eq_empty_alt
    using openin_subset by fastforce
  finally show ?thesis .
qed

lemma interior_of_closedin_union_empty_interior_of:
  assumes "closedin X S" and disj: "X interior_of T = {}"
  shows "X interior_of (S \<union> T) = X interior_of S"
proof -
  have "X closure_of (topspace X - T) = topspace X"
    by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of)
  then show ?thesis
    unfolding interior_of_closure_of
    by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset)
qed

lemma interior_of_union_eq_empty:
   "closedin X S
        \<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
             X interior_of S = {} \<and> X interior_of T = {})"
  by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)

lemma discrete_topology_interior_of [simp]:
    "(discrete_topology U) interior_of S = U \<inter> S"
  by (simp add: interior_of_restrict [of _ S] interior_of_eq)


subsection \<open>Frontier with respect to topological space \<close>

definition frontier_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "frontier'_of" 80)
  where "X frontier_of S \<equiv> X closure_of S - X interior_of S"

lemma frontier_of_closures:
     "X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
  by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)


lemma interior_of_union_frontier_of [simp]:
     "X interior_of S \<union> X frontier_of S = X closure_of S"
  by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)

lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X \<inter> S)"
  by (metis closure_of_restrict frontier_of_def interior_of_restrict)

lemma closedin_frontier_of: "closedin X (X frontier_of S)"
  by (simp add: closedin_Int frontier_of_closures)

lemma frontier_of_subset_topspace: "X frontier_of S \<subseteq> topspace X"
  by (simp add: closedin_frontier_of closedin_subset)

lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T \<subseteq> S"
  by (metis (no_types) closedin_derived_set closedin_frontier_of)

lemma frontier_of_subtopology_subset:
  "U \<inter> (subtopology X U) frontier_of S \<subseteq> (X frontier_of S)"
proof -
  have "U \<inter> X interior_of S - subtopology X U interior_of S = {}"
    by (simp add: interior_of_subtopology_subset)
  moreover have "X closure_of S \<inter> subtopology X U closure_of S = subtopology X U closure_of S"
    by (meson closure_of_subtopology_subset inf.absorb_iff2)
  ultimately show ?thesis
    unfolding frontier_of_def
    by blast
qed

lemma frontier_of_subtopology_mono:
   "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X T) frontier_of S \<subseteq> (subtopology X U) frontier_of S"
    by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono)

lemma clopenin_eq_frontier_of:
   "closedin X S \<and> openin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> X frontier_of S = {}"
proof (cases "S \<subseteq> topspace X")
  case True
  then show ?thesis
    by (metis Diff_eq_empty_iff closure_of_eq closure_of_subset_eq frontier_of_def interior_of_eq interior_of_subset interior_of_union_frontier_of sup_bot_right)
next
  case False
  then show ?thesis
    by (simp add: frontier_of_closures openin_closedin_eq)
qed

lemma frontier_of_eq_empty:
     "S \<subseteq> topspace X \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> closedin X S \<and> openin X S)"
  by (simp add: clopenin_eq_frontier_of)

lemma frontier_of_openin:
     "openin X S \<Longrightarrow> X frontier_of S = X closure_of S - S"
  by (metis (no_types) frontier_of_def interior_of_eq)

lemma frontier_of_openin_straddle_Int:
  assumes "openin X U" "U \<inter> X frontier_of S \<noteq> {}"
  shows "U \<inter> S \<noteq> {}" "U - S \<noteq> {}"
proof -
  have "U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}"
    using assms by (simp add: frontier_of_closures)
  then show "U \<inter> S \<noteq> {}"
    using assms openin_Int_closure_of_eq_empty by fastforce
  show "U - S \<noteq> {}"
  proof -
    have "\<exists>A. X closure_of (A - S) \<inter> U \<noteq> {}"
      using \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> by blast
    then have "\<not> U \<subseteq> S"
      by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty)
    then show ?thesis
      by blast
  qed
qed

lemma frontier_of_subset_closedin: "closedin X S \<Longrightarrow> (X frontier_of S) \<subseteq> S"
  using closure_of_eq frontier_of_def by fastforce

lemma frontier_of_empty [simp]: "X frontier_of {} = {}"
  by (simp add: frontier_of_def)

lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"
  by (simp add: frontier_of_def)

lemma frontier_of_subset_eq:
  assumes "S \<subseteq> topspace X"
  shows "(X frontier_of S) \<subseteq> S \<longleftrightarrow> closedin X S"
proof
  show "X frontier_of S \<subseteq> S \<Longrightarrow> closedin X S"
    by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff)
  show "closedin X S \<Longrightarrow> X frontier_of S \<subseteq> S"
    by (simp add: frontier_of_subset_closedin)
qed

lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S"
  by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute)

lemma frontier_of_disjoint_eq:
  assumes "S \<subseteq> topspace X"
  shows "((X frontier_of S) \<inter> S = {} \<longleftrightarrow> openin X S)"
proof
  assume "X frontier_of S \<inter> S = {}"
  then have "closedin X (topspace X - S)"
    using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce
  then show "openin X S"
    using assms by (simp add: openin_closedin)
next
  show "openin X S \<Longrightarrow> X frontier_of S \<inter> S = {}"
    by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute)
qed

lemma frontier_of_disjoint_eq_alt:
  "S \<subseteq> (topspace X - X frontier_of S) \<longleftrightarrow> openin X S"
proof (cases "S \<subseteq> topspace X")
  case True
  show ?thesis
    using True frontier_of_disjoint_eq by auto
next
  case False
  then show ?thesis
    by (meson Diff_subset openin_subset subset_trans)
qed

lemma frontier_of_Int:
     "X frontier_of (S \<inter> T) =
      X closure_of (S \<inter> T) \<inter> (X frontier_of S \<union> X frontier_of T)"
proof -
  have *: "U \<subseteq> S \<and> U \<subseteq> T \<Longrightarrow> U \<inter> (S \<inter> A \<union> T \<inter> B) = U \<inter> (A \<union> B)" for U S T A B :: "'a set"
    by blast
  show ?thesis
    by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un)
qed

lemma frontier_of_Int_subset: "X frontier_of (S \<inter> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
  by (simp add: frontier_of_Int)

lemma frontier_of_Int_closedin:
  "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> X frontier_of(S \<inter> T) = X frontier_of S \<inter> T \<union> S \<inter> X frontier_of T"
  apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
  using frontier_of_subset_closedin by blast

lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
  by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)

lemma frontier_of_Union_subset:
   "finite \<F> \<Longrightarrow> X frontier_of (\<Union>\<F>) \<subseteq> (\<Union>T \<in> \<F>. X frontier_of T)"
proof (induction \<F> rule: finite_induct)
  case (insert A \<F>)
  then show ?case
    using frontier_of_Un_subset by fastforce
qed simp

lemma frontier_of_frontier_of_subset:
     "X frontier_of (X frontier_of S) \<subseteq> X frontier_of S"
  by (simp add: closedin_frontier_of frontier_of_subset_closedin)

lemma frontier_of_subtopology_open:
     "openin X U \<Longrightarrow> (subtopology X U) frontier_of S = U \<inter> X frontier_of S"
  by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open)

lemma discrete_topology_frontier_of [simp]:
     "(discrete_topology U) frontier_of S = {}"
  by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)


subsection\<open>Locally finite collections\<close>

definition locally_finite_in
  where
 "locally_finite_in X \<A> \<longleftrightarrow>
        (\<Union>\<A> \<subseteq> topspace X) \<and>
        (\<forall>x \<in> topspace X. \<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}})"

lemma finite_imp_locally_finite_in:
   "\<lbrakk>finite \<A>; \<Union>\<A> \<subseteq> topspace X\<rbrakk> \<Longrightarrow> locally_finite_in X \<A>"
  by (auto simp: locally_finite_in_def)

lemma locally_finite_in_subset:
  assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
  shows "locally_finite_in X \<B>"
proof -
  have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
    apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
  then show ?thesis
  using assms unfolding locally_finite_in_def by (fastforce simp add:)
qed

lemma locally_finite_in_refinement:
  assumes \<A>: "locally_finite_in X \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> S"
  shows "locally_finite_in X (f ` \<A>)"
proof -
  show ?thesis
    unfolding locally_finite_in_def
  proof safe
    fix x
    assume "x \<in> topspace X"
    then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
      using \<A> unfolding locally_finite_in_def by blast
    moreover have "{U \<in> \<A>. f U \<inter> V \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}" for V
      using f by blast
    ultimately have "finite {U \<in> \<A>. f U \<inter> V \<noteq> {}}"
      using finite_subset by blast
    moreover have "f ` {U \<in> \<A>. f U \<inter> V \<noteq> {}} = {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
      by blast
    ultimately have "finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
      by (metis (no_types, lifting) finite_imageI)
    then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
      using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
  next
    show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
      by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
  qed
qed

lemma locally_finite_in_subtopology:
  assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
  shows "locally_finite_in (subtopology X S) \<A>"
  unfolding locally_finite_in_def
proof safe
  fix x
  assume x: "x \<in> topspace (subtopology X S)"
  then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
    using \<A> unfolding locally_finite_in_def topspace_subtopology by blast
  show "\<exists>V. openin (subtopology X S) V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
  proof (intro exI conjI)
    show "openin (subtopology X S) (S \<inter> V)"
      by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
    have "{U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}"
      by auto
    with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
      using finite_subset by auto
    show "x \<in> S \<inter> V"
      using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
  qed
next
  show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
    using assms unfolding locally_finite_in_def topspace_subtopology by blast
qed


lemma closedin_locally_finite_Union:
  assumes clo: "\<And>S. S \<in> \<A> \<Longrightarrow> closedin X S" and \<A>: "locally_finite_in X \<A>"
  shows "closedin X (\<Union>\<A>)"
  using \<A> unfolding locally_finite_in_def closedin_def
proof clarify
  show "openin X (topspace X - \<Union>\<A>)"
  proof (subst openin_subopen, clarify)
    fix x
    assume "x \<in> topspace X" and "x \<notin> \<Union>\<A>"
    then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
      using \<A> unfolding locally_finite_in_def by blast
    let ?T = "V - \<Union>{S \<in> \<A>. S \<inter> V \<noteq> {}}"
    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - \<Union>\<A>"
    proof (intro exI conjI)
      show "openin X ?T"
        by (metis (no_types, lifting) fin \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
      show "x \<in> ?T"
        using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
      show "?T \<subseteq> topspace X - \<Union>\<A>"
        using \<open>openin X V\<close> openin_subset by auto
    qed
  qed
qed

lemma locally_finite_in_closure:
  assumes \<A>: "locally_finite_in X \<A>"
  shows "locally_finite_in X ((\<lambda>S. X closure_of S) ` \<A>)"
  using \<A> unfolding locally_finite_in_def
proof (intro conjI; clarsimp)
  fix x A
  assume "x \<in> X closure_of A"
  then show "x \<in> topspace X"
    by (meson in_closure_of)
next
  fix x
  assume "x \<in> topspace X" and "\<Union>\<A> \<subseteq> topspace X"
  then obtain V where V: "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
    using \<A> unfolding locally_finite_in_def by blast
  have eq: "{y \<in> f ` \<A>. Q y} = f ` {x. x \<in> \<A> \<and> Q(f x)}" for f Q
    by blast
  have eq2: "{A \<in> \<A>. X closure_of A \<inter> V \<noteq> {}} = {A \<in> \<A>. A \<inter> V \<noteq> {}}"
    using openin_Int_closure_of_eq_empty V  by blast
  have "finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
    by (simp add: eq eq2 fin)
  with V show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
    by blast
qed

lemma closedin_Union_locally_finite_closure:
   "locally_finite_in X \<A> \<Longrightarrow> closedin X (\<Union>((\<lambda>S. X closure_of S) ` \<A>))"
  by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)

lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
  by clarify (meson Union_upper closure_of_mono subsetD)

lemma closure_of_locally_finite_Union:
   "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
  apply (rule closure_of_unique)
  apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
  apply (simp add: closedin_Union_locally_finite_closure)
  by (simp add: Sup_le_iff closure_of_minimal)


subsection\<open>Continuous maps\<close>

definition continuous_map where
  "continuous_map X Y f \<equiv>
     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
     (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"

lemma continuous_map:
   "continuous_map X Y f \<longleftrightarrow>
        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
  by (auto simp: continuous_map_def)

lemma continuous_map_image_subset_topspace:
   "continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
  by (auto simp: continuous_map_def)

lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
  by (auto simp: continuous_map_def)

lemma continuous_map_closedin:
   "continuous_map X Y f \<longleftrightarrow>
         (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
proof -
  have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
        (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
    if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
  proof -
    have eq: "{x \<in> topspace X. f x \<in> topspace Y \<and> f x \<notin> C} = (topspace X - {x \<in> topspace X. f x \<in> C})" for C
      using that by blast
    show ?thesis
    proof (intro iffI allI impI)
      fix C
      assume "\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}" and "closedin Y C"
      then have "openin X {x \<in> topspace X. f x \<in> topspace Y - C}" by blast
      then show "closedin X {x \<in> topspace X. f x \<in> C}"
        by (auto simp add: closedin_def eq)
    next
      fix U
      assume "\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}" and "openin Y U"
      then have "closedin X {x \<in> topspace X. f x \<in> topspace Y - U}" by blast
      then show "openin X {x \<in> topspace X. f x \<in> U}"
        by (auto simp add: openin_closedin_eq eq)
    qed
  qed
  then show ?thesis
    by (auto simp: continuous_map_def)
qed

lemma openin_continuous_map_preimage:
   "\<lbrakk>continuous_map X Y f; openin Y U\<rbrakk> \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
  by (simp add: continuous_map_def)

lemma closedin_continuous_map_preimage:
   "\<lbrakk>continuous_map X Y f; closedin Y C\<rbrakk> \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}"
  by (simp add: continuous_map_closedin)

lemma openin_continuous_map_preimage_gen:
  assumes "continuous_map X Y f" "openin X U" "openin Y V"
  shows "openin X {x \<in> U. f x \<in> V}"
proof -
  have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
    using assms(2) openin_closedin_eq by fastforce
  show ?thesis
    unfolding eq
    using assms openin_continuous_map_preimage by fastforce
qed

lemma closedin_continuous_map_preimage_gen:
  assumes "continuous_map X Y f" "closedin X U" "closedin Y V"
  shows "closedin X {x \<in> U. f x \<in> V}"
proof -
  have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
    using assms(2) closedin_def by fastforce
  show ?thesis
    unfolding eq
    using assms closedin_continuous_map_preimage by fastforce
qed

lemma continuous_map_image_closure_subset:
  assumes "continuous_map X Y f"
  shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
proof -
  have *: "f ` (topspace X) \<subseteq> topspace Y"
    by (meson assms continuous_map)
  have "X closure_of T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of (f ` T)}" if "T \<subseteq> topspace X" for T
  proof (rule closure_of_minimal)
    show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
      using closure_of_subset * that  by (fastforce simp: in_closure_of)
  next
    show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
      using assms closedin_continuous_map_preimage_gen by fastforce
  qed
  then have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (f ` (topspace X \<inter> S))"
    by blast
  also have "\<dots> \<subseteq> Y closure_of (topspace Y \<inter> f ` S)"
    using * by (blast intro!: closure_of_mono)
  finally have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (topspace Y \<inter> f ` S)" .
  then show ?thesis
    by (metis closure_of_restrict)
qed

lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
       (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  using continuous_map_image_closure_subset by blast

lemma continuous_map_subset_aux2:
  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
  shows "continuous_map X Y f"
  unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
  fix x
  assume "x \<in> topspace X"
  then show "f x \<in> topspace Y"
    using assms closure_of_subset_topspace by fastforce
next
  fix C
  assume "closedin Y C"
  then show "closedin X {x \<in> topspace X. f x \<in> C}"
  proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
    fix x
    assume x: "x \<in> X closure_of {x \<in> topspace X. f x \<in> C}"
      and "C \<subseteq> topspace Y" and "Y closure_of C \<subseteq> C"
    show "x \<in> topspace X"
      by (meson x in_closure_of)
    have "{a \<in> topspace X. f a \<in> C} \<subseteq> topspace X"
      by simp
    moreover have "Y closure_of f ` {a \<in> topspace X. f a \<in> C} \<subseteq> C"
      by (simp add: \<open>closedin Y C\<close> closure_of_minimal image_subset_iff)
    ultimately have "f ` (X closure_of {a \<in> topspace X. f a \<in> C}) \<subseteq> C"
      using assms by blast
    then show "f x \<in> C"
      using x by auto
  qed
qed

lemma continuous_map_eq_image_closure_subset:
     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis

lemma continuous_map_eq_image_closure_subset_alt:
     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis

lemma continuous_map_eq_image_closure_subset_gen:
     "continuous_map X Y f \<longleftrightarrow>
        f ` (topspace X) \<subseteq> topspace Y \<and>
        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
  using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis

lemma continuous_map_closure_preimage_subset:
   "continuous_map X Y f
        \<Longrightarrow> X closure_of {x \<in> topspace X. f x \<in> T}
            \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
  unfolding continuous_map_closedin
  by (rule closure_of_minimal) (use in_closure_of in \<open>fastforce+\<close>)


lemma continuous_map_frontier_frontier_preimage_subset:
  assumes "continuous_map X Y f"
  shows "X frontier_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y frontier_of T}"
proof -
  have eq: "topspace X - {x \<in> topspace X. f x \<in> T} = {x \<in> topspace X. f x \<in> topspace Y - T}"
    using assms unfolding continuous_map_def by blast
  have "X closure_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
    by (simp add: assms continuous_map_closure_preimage_subset)
  moreover
  have "X closure_of (topspace X - {x \<in> topspace X. f x \<in> T}) \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of (topspace Y - T)}"
    using continuous_map_closure_preimage_subset [OF assms] eq by presburger
  ultimately show ?thesis
    by (auto simp: frontier_of_closures)
qed

lemma topology_finer_continuous_id:
  "topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
  unfolding continuous_map_def
  apply auto
  using openin_subopen openin_subset apply fastforce
  using openin_subopen topspace_def by fastforce

lemma continuous_map_const [simp]:
   "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
proof (cases "topspace X = {}")
  case False
  show ?thesis
  proof (cases "C \<in> topspace Y")
    case True
    with openin_subopen show ?thesis
      by (auto simp: continuous_map_def)
  next
    case False
    then show ?thesis
      unfolding continuous_map_def by fastforce
  qed
qed (auto simp: continuous_map_on_empty)

lemma continuous_map_compose:
  assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
  shows "continuous_map X X'' (g \<circ> f)"
  unfolding continuous_map_def
proof (intro conjI ballI allI impI)
  fix x
  assume "x \<in> topspace X"
  then show "(g \<circ> f) x \<in> topspace X''"
    using assms unfolding continuous_map_def by force
next
  fix U
  assume "openin X'' U"
  have eq: "{x \<in> topspace X. (g \<circ> f) x \<in> U} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U}}"
    by auto (meson f continuous_map_def)
  show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
    unfolding eq
    using assms unfolding continuous_map_def
    using \<open>openin X'' U\<close> by blast
qed

lemma continuous_map_eq:
  assumes "continuous_map X X' f" and "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x" shows "continuous_map X X' g"
proof -
  have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
    using assms by auto
  show ?thesis
    using assms by (simp add: continuous_map_def eq)
qed

lemma restrict_continuous_map [simp]:
     "topspace X \<subseteq> S \<Longrightarrow> continuous_map X X' (restrict f S) \<longleftrightarrow> continuous_map X X' f"
  by (auto simp: elim!: continuous_map_eq)

lemma continuous_map_in_subtopology:
  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof -
    have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
      by (meson L continuous_map_image_closure_subset)
    then show ?thesis
      by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset dual_order.trans)
  qed
next
  assume R: ?rhs
  then have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. f x \<in> U \<and> f x \<in> S}" for U
    by auto
  show ?lhs
    using R
    unfolding continuous_map
    by (auto simp: topspace_subtopology openin_subtopology eq)
qed


lemma continuous_map_from_subtopology:
     "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
  by (auto simp: continuous_map topspace_subtopology openin_subtopology)

lemma continuous_map_into_fulltopology:
   "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
  by (auto simp: continuous_map_in_subtopology)

lemma continuous_map_into_subtopology:
   "\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
  by (auto simp: continuous_map_in_subtopology)

lemma continuous_map_from_subtopology_mono:
     "\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
      \<Longrightarrow> continuous_map (subtopology X S) X' f"
  by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)

lemma continuous_map_from_discrete_topology [simp]:
  "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
  by (auto simp: continuous_map_def)

lemma continuous_map_iff_continuous [simp]: "continuous_map (subtopology euclidean S) euclidean g = continuous_on S g"
  by (fastforce simp add: continuous_map openin_subtopology continuous_on_open_invariant)

lemma continuous_map_iff_continuous2 [simp]: "continuous_map euclidean euclidean g = continuous_on UNIV g"
  by (metis continuous_map_iff_continuous subtopology_UNIV)

lemma continuous_map_openin_preimage_eq:
   "continuous_map X Y f \<longleftrightarrow>
        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
  by (auto simp: continuous_map_def vimage_def Int_def)

lemma continuous_map_closedin_preimage_eq:
   "continuous_map X Y f \<longleftrightarrow>
        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
  by (auto simp: continuous_map_closedin vimage_def Int_def)

lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt"
  by (simp add: continuous_at_imp_continuous_on isCont_real_sqrt)

lemma continuous_map_sqrt [continuous_intros]:
   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
  by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)

lemma continuous_map_id [simp]: "continuous_map X X id"
  unfolding continuous_map_def  using openin_subopen topspace_def by fastforce

declare continuous_map_id [unfolded id_def, simp]

lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id"
  by (simp add: continuous_map_from_subtopology)

declare continuous_map_id_subt [unfolded id_def, simp]


subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>

definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  where "open_map X1 X2 f \<equiv> \<forall>U. openin X1 U \<longrightarrow> openin X2 (f ` U)"

definition closed_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"

lemma open_map_imp_subset_topspace:
     "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
  unfolding open_map_def by (simp add: openin_subset)

lemma open_map_imp_subset:
    "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
  by (meson order_trans open_map_imp_subset_topspace subset_image_iff)

lemma topology_finer_open_id:
     "(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
  unfolding open_map_def by auto

lemma open_map_id: "open_map X X id"
  unfolding open_map_def by auto

lemma open_map_eq:
     "\<lbrakk>open_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> open_map X X' g"
  unfolding open_map_def
  by (metis image_cong openin_subset subset_iff)

lemma open_map_inclusion_eq:
  "open_map (subtopology X S) X id \<longleftrightarrow> openin X (topspace X \<inter> S)"
proof -
  have *: "openin X (T \<inter> S)" if "openin X (S \<inter> topspace X)" "openin X T" for T
  proof -
    have "T \<subseteq> topspace X"
      using that by (simp add: openin_subset)
    with that show "openin X (T \<inter> S)"
      by (metis inf.absorb1 inf.left_commute inf_commute openin_Int)
  qed
  show ?thesis
    by (fastforce simp add: open_map_def Int_commute openin_subtopology_alt intro: *)
qed

lemma open_map_inclusion:
     "openin X S \<Longrightarrow> open_map (subtopology X S) X id"
  by (simp add: open_map_inclusion_eq openin_Int)

lemma open_map_compose:
     "\<lbrakk>open_map X X' f; open_map X' X'' g\<rbrakk> \<Longrightarrow> open_map X X'' (g \<circ> f)"
  by (metis (no_types, lifting) image_comp open_map_def)

lemma closed_map_imp_subset_topspace:
     "closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
  by (simp add: closed_map_def closedin_subset)

lemma closed_map_imp_subset:
     "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
  using closed_map_imp_subset_topspace by blast

lemma topology_finer_closed_id:
    "(\<forall>S. closedin X S \<longrightarrow> closedin X' S) \<longleftrightarrow> closed_map X X' id"
  by (simp add: closed_map_def)

lemma closed_map_id: "closed_map X X id"
  by (simp add: closed_map_def)

lemma closed_map_eq:
   "\<lbrakk>closed_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> closed_map X X' g"
  unfolding closed_map_def
  by (metis image_cong closedin_subset subset_iff)

lemma closed_map_compose:
    "\<lbrakk>closed_map X X' f; closed_map X' X'' g\<rbrakk> \<Longrightarrow> closed_map X X'' (g \<circ> f)"
  by (metis (no_types, lifting) closed_map_def image_comp)

lemma closed_map_inclusion_eq:
   "closed_map (subtopology X S) X id \<longleftrightarrow>
        closedin X (topspace X \<inter> S)"
proof -
  have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
  proof -
    have "T \<subseteq> topspace X"
      using that by (simp add: closedin_subset)
    with that show "closedin X (T \<inter> S)"
      by (metis inf.absorb1 inf.left_commute inf_commute closedin_Int)
  qed
  show ?thesis
    by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *)
qed

lemma closed_map_inclusion: "closedin X S \<Longrightarrow> closed_map (subtopology X S) X id"
  by (simp add: closed_map_inclusion_eq closedin_Int)

lemma open_map_into_subtopology:
    "\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
  unfolding open_map_def openin_subtopology
  using openin_subset by fastforce

lemma closed_map_into_subtopology:
    "\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
  unfolding closed_map_def closedin_subtopology
  using closedin_subset by fastforce

lemma open_map_into_discrete_topology:
    "open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
  unfolding open_map_def openin_discrete_topology using openin_subset by blast

lemma closed_map_into_discrete_topology:
    "closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
  unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast

lemma bijective_open_imp_closed_map:
     "\<lbrakk>open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> closed_map X X' f"
  unfolding open_map_def closed_map_def closedin_def
  by auto (metis Diff_subset inj_on_image_set_diff)

lemma bijective_closed_imp_open_map:
     "\<lbrakk>closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> open_map X X' f"
  unfolding closed_map_def open_map_def openin_closedin_eq
  by auto (metis Diff_subset inj_on_image_set_diff)

lemma open_map_from_subtopology:
     "\<lbrakk>open_map X X' f; openin X U\<rbrakk> \<Longrightarrow> open_map (subtopology X U) X' f"
  unfolding open_map_def openin_subtopology_alt by blast

lemma closed_map_from_subtopology:
     "\<lbrakk>closed_map X X' f; closedin X U\<rbrakk> \<Longrightarrow> closed_map (subtopology X U) X' f"
  unfolding closed_map_def closedin_subtopology_alt by blast

lemma open_map_restriction:
     "\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
      \<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
  unfolding open_map_def openin_subtopology_alt
  apply clarify
  apply (rename_tac T)
  apply (rule_tac x="f ` T" in image_eqI)
  using openin_closedin_eq by force+

lemma closed_map_restriction:
     "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
      \<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
  unfolding closed_map_def closedin_subtopology_alt
  apply clarify
  apply (rename_tac T)
  apply (rule_tac x="f ` T" in image_eqI)
  using closedin_def by force+

subsection\<open>Quotient maps\<close>
                                      
definition quotient_map where
 "quotient_map X X' f \<longleftrightarrow>
        f ` (topspace X) = topspace X' \<and>
        (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (openin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> openin X' U))"

lemma quotient_map_eq:
  assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
  shows "quotient_map X X' g"
proof -
  have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
    using assms by auto
  show ?thesis
  using assms
  unfolding quotient_map_def
  by (metis (mono_tags, lifting) eq image_cong)
qed

lemma quotient_map_compose:
  assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
  shows "quotient_map X X'' (g \<circ> f)"
  unfolding quotient_map_def
proof (intro conjI allI impI)
  show "(g \<circ> f) ` topspace X = topspace X''"
    using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def)
next
  fix U''
  assume "U'' \<subseteq> topspace X''"
  define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}"
  have "U' \<subseteq> topspace X'"
    by (auto simp add: U'_def)
  then have U': "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
    using assms unfolding quotient_map_def by simp
  have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''} = {x \<in> topspace X. (g \<circ> f) x \<in> U''}"
    using f quotient_map_def by fastforce
  have "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X {x \<in> topspace X. f x \<in> U'}"
    using assms  by (simp add: quotient_map_def U'_def eq)
  also have "\<dots> = openin X'' U''"
    using U'_def \<open>U'' \<subseteq> topspace X''\<close> U' g quotient_map_def by fastforce
  finally show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X'' U''" .
qed

lemma quotient_map_from_composition:
  assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \<circ> f)"
  shows  "quotient_map X' X'' g"
  unfolding quotient_map_def
proof (intro conjI allI impI)
  show "g ` topspace X' = topspace X''"
    using assms unfolding continuous_map_def quotient_map_def by fastforce
next
  fix U'' :: "'c set"
  assume U'': "U'' \<subseteq> topspace X''"
  have eq: "{x \<in> topspace X. g (f x) \<in> U''} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U''}}"
    using continuous_map_def f by fastforce
  show "openin X' {x \<in> topspace X'. g x \<in> U''} = openin X'' U''"
    using assms unfolding continuous_map_def quotient_map_def
    by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq)
qed

lemma quotient_imp_continuous_map:
    "quotient_map X X' f \<Longrightarrow> continuous_map X X' f"
  by (simp add: continuous_map openin_subset quotient_map_def)

lemma quotient_imp_surjective_map:
    "quotient_map X X' f \<Longrightarrow> f ` (topspace X) = topspace X'"
  by (simp add: quotient_map_def)

lemma quotient_map_closedin:
  "quotient_map X X' f \<longleftrightarrow>
        f ` (topspace X) = topspace X' \<and>
        (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (closedin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> closedin X' U))"
proof -
  have eq: "(topspace X - {x \<in> topspace X. f x \<in> U'}) = {x \<in> topspace X. f x \<in> topspace X' \<and> f x \<notin> U'}"
    if "f ` topspace X = topspace X'" "U' \<subseteq> topspace X'" for U'
      using that by auto
  have "(\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U) =
          (\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U)"
    if "f ` topspace X = topspace X'"
  proof (rule iffI; intro allI impI subsetI)
    fix U'
    assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
      and U': "U' \<subseteq> topspace X'"
    show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
      using U'  by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
  next
    fix U' :: "'b set"
    assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
      and U': "U' \<subseteq> topspace X'"
    show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
      using U'  by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
  qed
  then show ?thesis
    unfolding quotient_map_def by force
qed

lemma continuous_open_imp_quotient_map:
  assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
  shows "quotient_map X X' f"
proof -
  { fix U
    assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
    then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
      using om unfolding open_map_def by blast
    then have "openin X' U"
      using U feq by (subst openin_subopen) force
  }
  moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
    using that assms unfolding continuous_map_def by blast
  ultimately show ?thesis
    unfolding quotient_map_def using assms by blast
qed

lemma continuous_closed_imp_quotient_map:
  assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'"
  shows "quotient_map X X' f"
proof -
  have "f ` {x \<in> topspace X. f x \<in> U} = U" if "U \<subseteq> topspace X'" for U
    using that feq by auto
  with assms show ?thesis
    unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto
qed

lemma continuous_open_quotient_map:
   "\<lbrakk>continuous_map X X' f; open_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
  by (meson continuous_open_imp_quotient_map quotient_map_def)

lemma continuous_closed_quotient_map:
     "\<lbrakk>continuous_map X X' f; closed_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
  by (meson continuous_closed_imp_quotient_map quotient_map_def)

lemma injective_quotient_map:
  assumes "inj_on f (topspace X)"
  shows "quotient_map X X' f \<longleftrightarrow>
         continuous_map X X' f \<and> open_map X X' f \<and> closed_map X X' f \<and> f ` (topspace X) = topspace X'"
         (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  have "open_map X X' f"
  proof (clarsimp simp add: open_map_def)
    fix U
    assume "openin X U"
    then have "U \<subseteq> topspace X"
      by (simp add: openin_subset)
    moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
      using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
    ultimately show "openin X' (f ` U)"
      using L unfolding quotient_map_def
      by (metis (no_types, lifting) Collect_cong \<open>openin X U\<close> image_mono)
  qed
  moreover have "closed_map X X' f"
  proof (clarsimp simp add: closed_map_def)
    fix U
    assume "closedin X U"
    then have "U \<subseteq> topspace X"
      by (simp add: closedin_subset)
    moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
      using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
    ultimately show "closedin X' (f ` U)"
      using L unfolding quotient_map_closedin
      by (metis (no_types, lifting) Collect_cong \<open>closedin X U\<close> image_mono)
  qed
  ultimately show ?rhs
    using L by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
next
  assume ?rhs
  then show ?lhs
    by (simp add: continuous_closed_imp_quotient_map)
qed

lemma continuous_compose_quotient_map:
  assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
  shows "continuous_map X' X'' g"
  unfolding quotient_map_def continuous_map_def
proof (intro conjI ballI allI impI)
  show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
    using assms unfolding quotient_map_def
    by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
next
  fix U'' :: "'c set"
  assume U'': "openin X'' U''"
  have "f ` topspace X = topspace X'"
    by (simp add: f quotient_imp_surjective_map)
  then have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U} = {x \<in> topspace X. g (f x) \<in> U}" for U
    by auto
  have "openin X {x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''}"
    unfolding eq using U'' g openin_continuous_map_preimage by fastforce
  then have *: "openin X {x \<in> topspace X. f x \<in> {x \<in> topspace X'. g x \<in> U''}}"
    by auto
  show "openin X' {x \<in> topspace X'. g x \<in> U''}"
    using f unfolding quotient_map_def
    by (metis (no_types) Collect_subset *)
qed

lemma continuous_compose_quotient_map_eq:
   "quotient_map X X' f \<Longrightarrow> continuous_map X X'' (g \<circ> f) \<longleftrightarrow> continuous_map X' X'' g"
  using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast

lemma quotient_map_compose_eq:
   "quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
  apply safe
  apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
  by (simp add: quotient_map_compose)

lemma quotient_map_restriction:
  assumes quo: "quotient_map X Y f" and U: "{x \<in> topspace X. f x \<in> V} = U" and disj: "openin Y V \<or> closedin Y V"
 shows "quotient_map (subtopology X U) (subtopology Y V) f"
  using disj
proof
  assume V: "openin Y V"
  with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
    by (auto simp: openin_subset)
  have fim: "f ` topspace X = topspace Y"
     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
    using quo unfolding quotient_map_def by auto
  have "openin X U"
    using U V Y sub(2) by blast
  show ?thesis
    unfolding quotient_map_def
  proof (intro conjI allI impI)
    show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
      using sub U fim by (auto simp: topspace_subtopology)
  next
    fix Y' :: "'b set"
    assume "Y' \<subseteq> topspace (subtopology Y V)"
    then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
      by (simp_all add: topspace_subtopology)
    then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
      using U by blast
    then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
      using U V Y \<open>openin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
      by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
  qed
next
  assume V: "closedin Y V"
  with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
    by (auto simp: closedin_subset)
  have fim: "f ` topspace X = topspace Y"
     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U} = closedin Y U"
    using quo unfolding quotient_map_closedin by auto
  have "closedin X U"
    using U V Y sub(2) by blast
  show ?thesis
    unfolding quotient_map_closedin
  proof (intro conjI allI impI)
    show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
      using sub U fim by (auto simp: topspace_subtopology)
  next
    fix Y' :: "'b set"
    assume "Y' \<subseteq> topspace (subtopology Y V)"
    then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
      by (simp_all add: topspace_subtopology)
    then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
      using U by blast
    then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
      using U V Y \<open>closedin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
      by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
  qed
qed

lemma quotient_map_saturated_open:
     "quotient_map X Y f \<longleftrightarrow>
        continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
        (\<forall>U. openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> openin Y (f ` U))"
     (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have fim: "f ` topspace X = topspace Y"
    and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin Y U = openin X {x \<in> topspace X. f x \<in> U}"
    unfolding quotient_map_def by auto
  show ?rhs
  proof (intro conjI allI impI)
    show "continuous_map X Y f"
      by (simp add: L quotient_imp_continuous_map)
    show "f ` topspace X = topspace Y"
      by (simp add: fim)
  next
    fix U :: "'a set"
    assume U: "openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
    then have sub:  "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
      using fim openin_subset by fastforce+
    show "openin Y (f ` U)"
      by (simp add: sub Y eq U)
  qed
next
  assume ?rhs
  then have YX: "\<And>U. openin Y U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
       and fim: "f ` topspace X = topspace Y"
       and XY: "\<And>U. \<lbrakk>openin X U; {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U\<rbrakk> \<Longrightarrow> openin Y (f ` U)"
    by (auto simp: quotient_map_def continuous_map_def)
  show ?lhs
  proof (simp add: quotient_map_def fim, intro allI impI iffI)
    fix U :: "'b set"
    assume "U \<subseteq> topspace Y" and X: "openin X {x \<in> topspace X. f x \<in> U}"
    have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
      using \<open>U \<subseteq> topspace Y\<close> fim by auto
    show "openin Y U"
      using XY [OF X] by (simp add: feq)
  next
    fix U :: "'b set"
    assume "U \<subseteq> topspace Y" and Y: "openin Y U"
    show "openin X {x \<in> topspace X. f x \<in> U}"
      by (metis YX [OF Y])
  qed
qed

subsection\<open> Separated Sets\<close>

definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
  where "separatedin X S T \<equiv>
           S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
           S \<inter> X closure_of T = {} \<and> T \<inter> X closure_of S = {}"

lemma separatedin_empty [simp]:
     "separatedin X S {} \<longleftrightarrow> S \<subseteq> topspace X"
     "separatedin X {} S \<longleftrightarrow> S \<subseteq> topspace X"
  by (simp_all add: separatedin_def)

lemma separatedin_refl [simp]:
     "separatedin X S S \<longleftrightarrow> S = {}"
proof -
  have "\<And>x. \<lbrakk>separatedin X S S; x \<in> S\<rbrakk> \<Longrightarrow> False"
    by (metis all_not_in_conv closure_of_subset inf.orderE separatedin_def)
  then show ?thesis
    by auto
qed

lemma separatedin_sym:
     "separatedin X S T \<longleftrightarrow> separatedin X T S"
  by (auto simp: separatedin_def)

lemma separatedin_imp_disjoint:
     "separatedin X S T \<Longrightarrow> disjnt S T"
  by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def)

lemma separatedin_mono:
   "\<lbrakk>separatedin X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separatedin X S' T'"
  unfolding separatedin_def
  using closure_of_mono by blast

lemma separatedin_open_sets:
     "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
  unfolding disjnt_def separatedin_def
  by (auto simp: openin_Int_closure_of_eq_empty openin_subset)

lemma separatedin_closed_sets:
     "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
  by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)

lemma separatedin_subtopology:
     "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
  apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
  apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
  done

lemma separatedin_discrete_topology:
     "separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
  by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology)

lemma separated_eq_distinguishable:
   "separatedin X {x} {y} \<longleftrightarrow>
        x \<in> topspace X \<and> y \<in> topspace X \<and>
        (\<exists>U. openin X U \<and> x \<in> U \<and> (y \<notin> U)) \<and>
        (\<exists>v. openin X v \<and> y \<in> v \<and> (x \<notin> v))"
  by (force simp: separatedin_def closure_of_def)

lemma separatedin_Un [simp]:
   "separatedin X S (T \<union> U) \<longleftrightarrow> separatedin X S T \<and> separatedin X S U"
   "separatedin X (S \<union> T) U \<longleftrightarrow> separatedin X S U \<and> separatedin X T U"
  by (auto simp: separatedin_def)

lemma separatedin_Union:
  "finite \<F> \<Longrightarrow> separatedin X S (\<Union>\<F>) \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<forall>T \<in> \<F>. separatedin X S T)"
  "finite \<F> \<Longrightarrow> separatedin X (\<Union>\<F>) S \<longleftrightarrow> (\<forall>T \<in> \<F>. separatedin X S T) \<and> S \<subseteq> topspace X"
  by (auto simp: separatedin_def closure_of_Union)

lemma separatedin_openin_diff:
   "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
  unfolding separatedin_def
  apply (intro conjI)
  apply (meson Diff_subset openin_subset subset_trans)+
  using openin_Int_closure_of_eq_empty by fastforce+

lemma separatedin_closedin_diff:
     "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
  apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
  apply (meson Diff_subset closedin_subset subset_trans)
  done

lemma separation_closedin_Un_gen:
     "separatedin X S T \<longleftrightarrow>
        S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
        closedin (subtopology X (S \<union> T)) S \<and>
        closedin (subtopology X (S \<union> T)) T"
  apply (simp add: separatedin_def closedin_Int_closure_of disjnt_iff)
  using closure_of_subset apply blast
  done

lemma separation_openin_Un_gen:
     "separatedin X S T \<longleftrightarrow>
        S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
        openin (subtopology X (S \<union> T)) S \<and>
        openin (subtopology X (S \<union> T)) T"
  unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
  by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)


subsection\<open>Homeomorphisms\<close>
text\<open>(1-way and 2-way versions may be useful in places)\<close>

definition homeomorphic_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  where
 "homeomorphic_map X Y f \<equiv> quotient_map X Y f \<and> inj_on f (topspace X)"

definition homeomorphic_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
  where
 "homeomorphic_maps X Y f g \<equiv>
    continuous_map X Y f \<and> continuous_map Y X g \<and>
     (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"


lemma homeomorphic_map_eq:
   "\<lbrakk>homeomorphic_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> homeomorphic_map X Y g"
  by (meson homeomorphic_map_def inj_on_cong quotient_map_eq)

lemma homeomorphic_maps_eq:
     "\<lbrakk>homeomorphic_maps X Y f g;
       \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
      \<Longrightarrow> homeomorphic_maps X Y f' g'"
  apply (simp add: homeomorphic_maps_def)
  by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)

lemma homeomorphic_maps_sym:
     "homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
  by (auto simp: homeomorphic_maps_def)

lemma homeomorphic_maps_id:
     "homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have "topspace X = topspace Y"
    by (auto simp: homeomorphic_maps_def continuous_map_def)
  with L show ?rhs
    unfolding homeomorphic_maps_def
    by (metis topology_finer_continuous_id topology_eq)
next
  assume ?rhs
  then show ?lhs
    unfolding homeomorphic_maps_def by auto
qed

lemma homeomorphic_map_id [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
       (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have eq: "topspace X = topspace Y"
    by (auto simp: homeomorphic_map_def continuous_map_def quotient_map_def)
  then have "\<And>S. openin X S \<longrightarrow> openin Y S"
    by (meson L homeomorphic_map_def injective_quotient_map topology_finer_open_id)
  then show ?rhs
    using L unfolding homeomorphic_map_def
    by (metis eq quotient_imp_continuous_map topology_eq topology_finer_continuous_id)
next
  assume ?rhs
  then show ?lhs
    unfolding homeomorphic_map_def
    by (simp add: closed_map_id continuous_closed_imp_quotient_map)
qed

lemma homeomorphic_maps_i [simp]:"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
  by (metis (full_types) eq_id_iff homeomorphic_maps_id)

lemma homeomorphic_map_i [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
  by (metis (no_types) eq_id_iff homeomorphic_map_id)

lemma homeomorphic_map_compose:
  assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g"
  shows "homeomorphic_map X X'' (g \<circ> f)"
proof -
  have "inj_on g (f ` topspace X)"
    by (metis (no_types) assms homeomorphic_map_def quotient_imp_surjective_map)
  then show ?thesis
    using assms by (meson comp_inj_on homeomorphic_map_def quotient_map_compose_eq)
qed

lemma homeomorphic_maps_compose:
   "homeomorphic_maps X Y f h \<and>
        homeomorphic_maps Y X'' g k
        \<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
  unfolding homeomorphic_maps_def
  by (auto simp: continuous_map_compose; simp add: continuous_map_def)

lemma homeomorphic_eq_everything_map:
   "homeomorphic_map X Y f \<longleftrightarrow>
        continuous_map X Y f \<and> open_map X Y f \<and> closed_map X Y f \<and>
        f ` (topspace X) = topspace Y \<and> inj_on f (topspace X)"
  unfolding homeomorphic_map_def
  by (force simp: injective_quotient_map intro: injective_quotient_map)

lemma homeomorphic_imp_continuous_map:
     "homeomorphic_map X Y f \<Longrightarrow> continuous_map X Y f"
  by (simp add: homeomorphic_eq_everything_map)

lemma homeomorphic_imp_open_map:
   "homeomorphic_map X Y f \<Longrightarrow> open_map X Y f"
  by (simp add: homeomorphic_eq_everything_map)

lemma homeomorphic_imp_closed_map:
   "homeomorphic_map X Y f \<Longrightarrow> closed_map X Y f"
  by (simp add: homeomorphic_eq_everything_map)

lemma homeomorphic_imp_surjective_map:
   "homeomorphic_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
  by (simp add: homeomorphic_eq_everything_map)

lemma homeomorphic_imp_injective_map:
    "homeomorphic_map X Y f \<Longrightarrow> inj_on f (topspace X)"
  by (simp add: homeomorphic_eq_everything_map)

lemma bijective_open_imp_homeomorphic_map:
   "\<lbrakk>continuous_map X Y f; open_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
        \<Longrightarrow> homeomorphic_map X Y f"
  by (simp add: homeomorphic_map_def continuous_open_imp_quotient_map)

lemma bijective_closed_imp_homeomorphic_map:
   "\<lbrakk>continuous_map X Y f; closed_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
        \<Longrightarrow> homeomorphic_map X Y f"
  by (simp add: continuous_closed_quotient_map homeomorphic_map_def)

lemma open_eq_continuous_inverse_map:
  assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
    and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
  shows "open_map X Y f \<longleftrightarrow> continuous_map Y X g"
proof -
  have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "openin X U" for U
    using openin_subset [OF that] by (force simp: X Y image_iff)
  show ?thesis
    by (auto simp: Y open_map_def continuous_map_def eq)
qed

lemma closed_eq_continuous_inverse_map:
  assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
    and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
  shows "closed_map X Y f \<longleftrightarrow> continuous_map Y X g"
proof -
  have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "closedin X U" for U
    using closedin_subset [OF that] by (force simp: X Y image_iff)
  show ?thesis
    by (auto simp: Y closed_map_def continuous_map_closedin eq)
qed

lemma homeomorphic_maps_map:
  "homeomorphic_maps X Y f g \<longleftrightarrow>
        homeomorphic_map X Y f \<and> homeomorphic_map Y X g \<and>
        (\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have L: "continuous_map X Y f" "continuous_map Y X g" "\<forall>x\<in>topspace X. g (f x) = x" "\<forall>x'\<in>topspace Y. f (g x') = x'"
    by (auto simp: homeomorphic_maps_def)
  show ?rhs
  proof (intro conjI bijective_open_imp_homeomorphic_map L)
    show "open_map X Y f"
      using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
    show "open_map Y X g"
      using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
    show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
      using L by (force simp: continuous_map_closedin)+
    show "inj_on f (topspace X)" "inj_on g (topspace Y)"
      using L unfolding inj_on_def by metis+
  qed
next
  assume ?rhs
  then show ?lhs
    by (auto simp: homeomorphic_maps_def homeomorphic_imp_continuous_map)
qed

lemma homeomorphic_maps_imp_map:
    "homeomorphic_maps X Y f g \<Longrightarrow> homeomorphic_map X Y f"
  using homeomorphic_maps_map by blast

lemma homeomorphic_map_maps:
     "homeomorphic_map X Y f \<longleftrightarrow> (\<exists>g. homeomorphic_maps X Y f g)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have L: "continuous_map X Y f" "open_map X Y f" "closed_map X Y f"
    "f ` (topspace X) = topspace Y" "inj_on f (topspace X)"
    by (auto simp: homeomorphic_eq_everything_map)
  have X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> inv_into (topspace X) f (f x) = x"
    using L by auto
  have Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> inv_into (topspace X) f y \<in> topspace X \<and> f (inv_into (topspace X) f y) = y"
    by (simp add: L f_inv_into_f inv_into_into)
  have "homeomorphic_maps X Y f (inv_into (topspace X) f)"
    unfolding homeomorphic_maps_def
  proof (intro conjI L)
    show "continuous_map Y X (inv_into (topspace X) f)"
      by (simp add: L X Y flip: open_eq_continuous_inverse_map [where f=f])
  next
    show "\<forall>x\<in>topspace X. inv_into (topspace X) f (f x) = x"
         "\<forall>y\<in>topspace Y. f (inv_into (topspace X) f y) = y"
      using X Y by auto
  qed
  then show ?rhs
    by metis
next
  assume ?rhs
  then show ?lhs
    using homeomorphic_maps_map by blast
qed

lemma homeomorphic_maps_involution:
   "\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_maps X X f f"
  by (auto simp: homeomorphic_maps_def)

lemma homeomorphic_map_involution:
   "\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_map X X f"
  using homeomorphic_maps_involution homeomorphic_maps_map by blast

lemma homeomorphic_map_openness:
  assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  shows "openin Y (f ` U) \<longleftrightarrow> openin X U"
proof -
  obtain g where "homeomorphic_maps X Y f g"
    using assms by (auto simp: homeomorphic_map_maps)
  then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
    by (auto simp: homeomorphic_maps_map)
  then have "openin X U \<Longrightarrow> openin Y (f ` U)"
    using hom homeomorphic_imp_open_map open_map_def by blast
  show "openin Y (f ` U) = openin X U"
  proof
    assume L: "openin Y (f ` U)"
    have "U = g ` (f ` U)"
      using U gf by force
    then show "openin X U"
      by (metis L homeomorphic_imp_open_map open_map_def g)
  next
    assume "openin X U"
    then show "openin Y (f ` U)"
      using hom homeomorphic_imp_open_map open_map_def by blast
  qed
qed


lemma homeomorphic_map_closedness:
  assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  shows "closedin Y (f ` U) \<longleftrightarrow> closedin X U"
proof -
  obtain g where "homeomorphic_maps X Y f g"
    using assms by (auto simp: homeomorphic_map_maps)
  then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
    by (auto simp: homeomorphic_maps_map)
  then have "closedin X U \<Longrightarrow> closedin Y (f ` U)"
    using hom homeomorphic_imp_closed_map closed_map_def by blast
  show "closedin Y (f ` U) = closedin X U"
  proof
    assume L: "closedin Y (f ` U)"
    have "U = g ` (f ` U)"
      using U gf by force
    then show "closedin X U"
      by (metis L homeomorphic_imp_closed_map closed_map_def g)
  next
    assume "closedin X U"
    then show "closedin Y (f ` U)"
      using hom homeomorphic_imp_closed_map closed_map_def by blast
  qed
qed

lemma homeomorphic_map_openness_eq:
     "homeomorphic_map X Y f \<Longrightarrow> openin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> openin Y (f ` U)"
  by (meson homeomorphic_map_openness openin_closedin_eq)

lemma homeomorphic_map_closedness_eq:
    "homeomorphic_map X Y f \<Longrightarrow> closedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> closedin Y (f ` U)"
  by (meson closedin_subset homeomorphic_map_closedness)

lemma all_openin_homeomorphic_image:
  assumes "homeomorphic_map X Y f"
  shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (meson assms homeomorphic_map_openness_eq)
next
  assume ?rhs
  then show ?lhs
    by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff)
qed

lemma all_closedin_homeomorphic_image:
  assumes "homeomorphic_map X Y f"
  shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))"  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (meson assms homeomorphic_map_closedness_eq)
next
  assume ?rhs
  then show ?lhs
    by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff)
qed


lemma homeomorphic_map_derived_set_of:
  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
proof -
  have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
    using hom by (auto simp: homeomorphic_eq_everything_map)
  have iff: "(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) =
            (\<forall>T. T \<subseteq> topspace Y \<longrightarrow> f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))"
    if "x \<in> topspace X" for x
  proof -
    have 1: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
      by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
    have 2: "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)" (is "?lhs = ?rhs")
      if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
    proof
      show "?lhs \<Longrightarrow> ?rhs"
        by (meson "1" imageI inj inj_on_eq_iff inj_on_subset that)
      show "?rhs \<Longrightarrow> ?lhs"
        using S inj inj_onD that by fastforce
    qed
    show ?thesis
      apply (simp flip: fim add: all_subset_image)
      apply (simp flip: imp_conjL)
      by (intro all_cong1 imp_cong 1 2)
  qed
  have *: "\<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x \<longleftrightarrow> Q(f x)\<rbrakk> \<Longrightarrow> {y. y \<in> T \<and> Q y} = f ` {x \<in> S. P x}" for T S P Q
    by auto
  show ?thesis
    unfolding derived_set_of_def
    apply (rule *)
    using fim apply blast
    using iff openin_subset by force
qed


lemma homeomorphic_map_closure_of:
  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  shows "Y closure_of (f ` S) = f ` (X closure_of S)"
  unfolding closure_of
  using homeomorphic_imp_surjective_map [OF hom] S
  by (auto simp: in_derived_set_of homeomorphic_map_derived_set_of [OF assms])

lemma homeomorphic_map_interior_of:
  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  shows "Y interior_of (f ` S) = f ` (X interior_of S)"
proof -
  { fix y
    assume "y \<in> topspace Y" and "y \<notin> Y closure_of (topspace Y - f ` S)"
    then have "y \<in> f ` (topspace X - X closure_of (topspace X - S))"
      using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom]
      by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) }
  moreover
  { fix x
    assume "x \<in> topspace X"
    then have "f x \<in> topspace Y"
      using hom homeomorphic_imp_surjective_map by blast }
  moreover
  { fix x
    assume "x \<in> topspace X" and "x \<notin> X closure_of (topspace X - S)" and "f x \<in> Y closure_of (topspace Y - f ` S)"
    then have "False"
      using homeomorphic_map_closure_of [OF hom] hom
      unfolding homeomorphic_eq_everything_map
      by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
  ultimately  show ?thesis
    by (auto simp: interior_of_closure_of)
qed

lemma homeomorphic_map_frontier_of:
  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  shows "Y frontier_of (f ` S) = f ` (X frontier_of S)"
  unfolding frontier_of_def
proof (intro equalityI subsetI DiffI)
  fix y
  assume "y \<in> Y closure_of f ` S - Y interior_of f ` S"
  then show "y \<in> f ` (X closure_of S - X interior_of S)"
    using S hom homeomorphic_map_closure_of homeomorphic_map_interior_of by fastforce
next
  fix y
  assume "y \<in> f ` (X closure_of S - X interior_of S)"
  then show "y \<in> Y closure_of f ` S"
    using S hom homeomorphic_map_closure_of by fastforce
next
  fix x
  assume "x \<in> f ` (X closure_of S - X interior_of S)"
  then obtain y where y: "x = f y" "y \<in> X closure_of S" "y \<notin> X interior_of S"
    by blast
  then have "y \<in> topspace X"
    by (simp add: in_closure_of)
  then have "f y \<notin> f ` (X interior_of S)"
    by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
  then show "x \<notin> Y interior_of f ` S"
    using S hom homeomorphic_map_interior_of y(1) by blast
qed

lemma homeomorphic_maps_subtopologies:
   "\<lbrakk>homeomorphic_maps X Y f g;  f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
        \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
  unfolding homeomorphic_maps_def
  by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)

lemma homeomorphic_maps_subtopologies_alt:
     "\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
      \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
  unfolding homeomorphic_maps_def
  by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)

lemma homeomorphic_map_subtopologies:
   "\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
        \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
  by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies)

lemma homeomorphic_map_subtopologies_alt:
   "\<lbrakk>homeomorphic_map X Y f;
     \<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S\<rbrakk>
    \<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
  unfolding homeomorphic_map_maps
  apply (erule ex_forward)
  apply (rule homeomorphic_maps_subtopologies)
  apply (auto simp: homeomorphic_maps_def continuous_map_def)
  by (metis IntI image_iff)


subsection\<open>Relation of homeomorphism between topological spaces\<close>

definition homeomorphic_space (infixr "homeomorphic'_space" 50)
  where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"

lemma homeomorphic_space_refl: "X homeomorphic_space X"
  by (meson homeomorphic_maps_id homeomorphic_space_def)

lemma homeomorphic_space_sym:
   "X homeomorphic_space Y \<longleftrightarrow> Y homeomorphic_space X"
  unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym)

lemma homeomorphic_space_trans:
     "\<lbrakk>X1 homeomorphic_space X2; X2 homeomorphic_space X3\<rbrakk> \<Longrightarrow> X1 homeomorphic_space X3"
  unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose)

lemma homeomorphic_space:
     "X homeomorphic_space Y \<longleftrightarrow> (\<exists>f. homeomorphic_map X Y f)"
  by (simp add: homeomorphic_map_maps homeomorphic_space_def)

lemma homeomorphic_maps_imp_homeomorphic_space:
     "homeomorphic_maps X Y f g \<Longrightarrow> X homeomorphic_space Y"
  unfolding homeomorphic_space_def by metis

lemma homeomorphic_map_imp_homeomorphic_space:
     "homeomorphic_map X Y f \<Longrightarrow> X homeomorphic_space Y"
  unfolding homeomorphic_map_maps
  using homeomorphic_space_def by blast

lemma homeomorphic_empty_space:
     "X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
  by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty)

lemma homeomorphic_empty_space_eq:
  assumes "topspace X = {}"
    shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
proof -
  have "\<forall>f t. continuous_map X (t::'b topology) f"
    using assms continuous_map_on_empty by blast
  then show ?thesis
    by (metis (no_types) assms continuous_map_on_empty empty_iff homeomorphic_empty_space homeomorphic_maps_def homeomorphic_space_def)
qed

subsection\<open>Connected topological spaces\<close>

definition connected_space :: "'a topology \<Rightarrow> bool" where
  "connected_space X \<equiv>
        \<not>(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
                  topspace X \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"

definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
  "connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"

lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
  by (simp add: connectedin_def)

lemma connectedin_topspace:
     "connectedin X (topspace X) \<longleftrightarrow> connected_space X"
  by (simp add: connectedin_def)

lemma connected_space_subtopology:
     "connectedin X S \<Longrightarrow> connected_space (subtopology X S)"
  by (simp add: connectedin_def)

lemma connectedin_subtopology:
     "connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> S"
  by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2)

lemma connected_space_eq:
     "connected_space X \<longleftrightarrow>
      (\<nexists>E1 E2. openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
  unfolding connected_space_def
  by (metis openin_Un openin_subset subset_antisym)

lemma connected_space_closedin:
     "connected_space X \<longleftrightarrow>
      (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and> topspace X \<subseteq> E1 \<union> E2 \<and>
               E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have L: "\<And>E1 E2. \<lbrakk>openin X E1; E1 \<inter> E2 = {}; topspace X \<subseteq> E1 \<union> E2; openin X E2\<rbrakk> \<Longrightarrow> E1 = {} \<or> E2 = {}"
    by (simp add: connected_space_def)
  show ?rhs
    unfolding connected_space_def
  proof clarify
    fix E1 E2
    assume "closedin X E1" and "closedin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
      and "E1 \<noteq> {}" and "E2 \<noteq> {}"
    have "E1 \<union> E2 = topspace X"
      by (meson Un_subset_iff \<open>closedin X E1\<close> \<open>closedin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> closedin_def subset_antisym)
    then have "topspace X - E2 = E1"
      using \<open>E1 \<inter> E2 = {}\<close> by fastforce
    then have "topspace X = E1"
      using \<open>E1 \<noteq> {}\<close> L \<open>closedin X E1\<close> \<open>closedin X E2\<close> by blast
    then show "False"
      using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
  qed
next
  assume R: ?rhs
  show ?lhs
    unfolding connected_space_def
  proof clarify
    fix E1 E2
    assume "openin X E1" and "openin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
      and "E1 \<noteq> {}" and "E2 \<noteq> {}"
    have "E1 \<union> E2 = topspace X"
      by (meson Un_subset_iff \<open>openin X E1\<close> \<open>openin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> openin_closedin_eq subset_antisym)
    then have "topspace X - E2 = E1"
      using \<open>E1 \<inter> E2 = {}\<close> by fastforce
    then have "topspace X = E1"
      using \<open>E1 \<noteq> {}\<close> R \<open>openin X E1\<close> \<open>openin X E2\<close> by blast
    then show "False"
      using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
  qed
qed

lemma connected_space_closedin_eq:
     "connected_space X \<longleftrightarrow>
       (\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
                E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
  apply (simp add: connected_space_closedin)
  apply (intro all_cong)
  using closedin_subset apply blast
  done

lemma connected_space_clopen_in:
     "connected_space X \<longleftrightarrow>
        (\<forall>T. openin X T \<and> closedin X T \<longrightarrow> T = {} \<or> T = topspace X)"
proof -
  have eq: "openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> P
        \<longleftrightarrow> E2 = topspace X - E1 \<and> openin X E1 \<and> openin X E2 \<and> P" for E1 E2 P
    using openin_subset by blast
  show ?thesis
    unfolding connected_space_eq eq closedin_def
    by (auto simp: openin_closedin_eq)
qed

lemma connectedin:
     "connectedin X S \<longleftrightarrow>
        S \<subseteq> topspace X \<and>
         (\<nexists>E1 E2.
             openin X E1 \<and> openin X E2 \<and>
             S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
proof -
  have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
             R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
    by auto
  show ?thesis
    unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology Not_eq_iff *
    apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
    apply (blast elim: dest!: openin_subset)+
    done
qed

lemma connectedin_iff_connected [simp]: "connectedin euclidean S \<longleftrightarrow> connected S"
  by (simp add: connected_def connectedin)

lemma connectedin_closedin:
   "connectedin X S \<longleftrightarrow>
        S \<subseteq> topspace X \<and>
        \<not>(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
                  S \<subseteq> (E1 \<union> E2) \<and>
                  (E1 \<inter> E2 \<inter> S = {}) \<and>
                  \<not>(E1 \<inter> S = {}) \<and> \<not>(E2 \<inter> S = {}))"
proof -
  have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
             R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
    by auto
  show ?thesis
    unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology Not_eq_iff *
    apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
    apply (blast elim: dest!: openin_subset)+
    done
qed

lemma connectedin_empty [simp]: "connectedin X {}"
  by (simp add: connectedin)

lemma connected_space_topspace_empty:
     "topspace X = {} \<Longrightarrow> connected_space X"
  using connectedin_topspace by fastforce

lemma connectedin_sing [simp]: "connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
  by (simp add: connectedin)

lemma connectedin_absolute [simp]:
  "connectedin (subtopology X S) S \<longleftrightarrow> connectedin X S"
  apply (simp only: connectedin_def topspace_subtopology subtopology_subtopology)
  apply (intro conj_cong imp_cong arg_cong [where f=Not] all_cong1 ex_cong1 refl)
  by auto

lemma connectedin_Union:
  assumes \<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> connectedin X S" and ne: "\<Inter>\<U> \<noteq> {}"
  shows "connectedin X (\<Union>\<U>)"
proof -
  have "\<Union>\<U> \<subseteq> topspace X"
    using \<U> by (simp add: Union_least connectedin_def)
  moreover have False
    if "openin X E1" "openin X E2" and cover: "\<Union>\<U> \<subseteq> E1 \<union> E2" and disj: "E1 \<inter> E2 \<inter> \<Union>\<U> = {}"
       and overlap1: "E1 \<inter> \<Union>\<U> \<noteq> {}" and overlap2: "E2 \<inter> \<Union>\<U> \<noteq> {}"
      for E1 E2
  proof -
    have disjS: "E1 \<inter> E2 \<inter> S = {}" if "S \<in> \<U>" for S
      using Diff_triv that disj by auto
    have coverS: "S \<subseteq> E1 \<union> E2" if "S \<in> \<U>" for S
      using that cover by blast
    have "\<U> \<noteq> {}"
      using overlap1 by blast
    obtain a where a: "\<And>U. U \<in> \<U> \<Longrightarrow> a \<in> U"
      using ne by force
    with \<open>\<U> \<noteq> {}\<close> have "a \<in> \<Union>\<U>"
      by blast
    then consider "a \<in> E1" | "a \<in> E2"
      using \<open>\<Union>\<U> \<subseteq> E1 \<union> E2\<close> by auto
    then show False
    proof cases
      case 1
      then obtain b S where "b \<in> E2" "b \<in> S" "S \<in> \<U>"
        using overlap2 by blast
      then show ?thesis
        using "1" \<open>openin X E1\<close> \<open>openin X E2\<close> disjS coverS a [OF \<open>S \<in> \<U>\<close>]  \<U>[OF \<open>S \<in> \<U>\<close>]
        unfolding connectedin
        by (meson disjoint_iff_not_equal)
    next
      case 2
      then obtain b S where "b \<in> E1" "b \<in> S" "S \<in> \<U>"
        using overlap1 by blast
      then show ?thesis
        using "2" \<open>openin X E1\<close> \<open>openin X E2\<close> disjS coverS a [OF \<open>S \<in> \<U>\<close>]  \<U>[OF \<open>S \<in> \<U>\<close>]
        unfolding connectedin
        by (meson disjoint_iff_not_equal)
    qed
  qed
  ultimately show ?thesis
    unfolding connectedin by blast
qed

lemma connectedin_Un:
     "\<lbrakk>connectedin X S; connectedin X T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
  using connectedin_Union [of "{S,T}"] by auto

lemma connected_space_subconnected:
  "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. connectedin X S \<and> x \<in> S \<and> y \<in> S)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    using connectedin_topspace by blast
next
  assume R [rule_format]: ?rhs
  have False if "openin X U" "openin X V" and disj: "U \<inter> V = {}" and cover: "topspace X \<subseteq> U \<union> V"
    and "U \<noteq> {}" "V \<noteq> {}" for U V
  proof -
    obtain u v where "u \<in> U" "v \<in> V"
      using \<open>U \<noteq> {}\<close> \<open>V \<noteq> {}\<close> by auto
    then obtain T where "u \<in> T" "v \<in> T" and T: "connectedin X T"
      using R [of u v] that
      by (meson \<open>openin X U\<close> \<open>openin X V\<close> subsetD openin_subset)
    then show False
      using that unfolding connectedin
      by (metis IntI \<open>u \<in> U\<close> \<open>v \<in> V\<close> empty_iff inf_bot_left subset_trans)
  qed
  then show ?lhs
    by (auto simp: connected_space_def)
qed

lemma connectedin_intermediate_closure_of:
  assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
  shows "connectedin X T"
proof -
  have S: "S \<subseteq> topspace X"and T: "T \<subseteq> topspace X"
    using assms by (meson closure_of_subset_topspace dual_order.trans)+
  show ?thesis
  using assms
  apply (simp add: connectedin closure_of_subset_topspace S T)
  apply (elim all_forward imp_forward2 asm_rl)
  apply (blast dest: openin_Int_closure_of_eq_empty [of X _ S])+
  done
qed

lemma connectedin_closure_of:
     "connectedin X S \<Longrightarrow> connectedin X (X closure_of S)"
  by (meson closure_of_subset connectedin_def connectedin_intermediate_closure_of subset_refl)

lemma connectedin_separation:
  "connectedin X S \<longleftrightarrow>
        S \<subseteq> topspace X \<and>
        (\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> C1 \<inter> X closure_of C2 = {} \<and> C2 \<inter> X closure_of C1 = {})" (is "?lhs = ?rhs")
  unfolding connectedin_def connected_space_closedin_eq closedin_Int_closure_of topspace_subtopology
  apply (intro conj_cong refl arg_cong [where f=Not])
  apply (intro ex_cong1 iffI, blast)
  using closure_of_subset_Int by force

lemma connectedin_eq_not_separated:
   "connectedin X S \<longleftrightarrow>
         S \<subseteq> topspace X \<and>
         (\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
  apply (simp add: separatedin_def connectedin_separation)
  apply (intro conj_cong all_cong1 refl, blast)
  done

lemma connectedin_eq_not_separated_subset:
  "connectedin X S \<longleftrightarrow>
      S \<subseteq> topspace X \<and> (\<nexists>C1 C2. S \<subseteq> C1 \<union> C2 \<and> S \<inter> C1 \<noteq> {} \<and> S \<inter> C2 \<noteq> {} \<and> separatedin X C1 C2)"
proof -
  have *: "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
    if "\<And>C1 C2. C1 \<union> C2 = S \<longrightarrow> C1 = {} \<or> C2 = {} \<or> \<not> separatedin X C1 C2"
  proof (intro allI)
    fix C1 C2
    show "S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
      using that [of "S \<inter> C1" "S \<inter> C2"]
      by (auto simp: separatedin_mono)
  qed
  show ?thesis
    apply (simp add: connectedin_eq_not_separated)
    apply (intro conj_cong refl iffI *)
    apply (blast elim!: all_forward)+
    done
qed

lemma connected_space_eq_not_separated:
     "connected_space X \<longleftrightarrow>
      (\<nexists>C1 C2. C1 \<union> C2 = topspace X \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
  by (simp add: connectedin_eq_not_separated flip: connectedin_topspace)

lemma connected_space_eq_not_separated_subset:
  "connected_space X \<longleftrightarrow>
    (\<nexists>C1 C2. topspace X \<subseteq> C1 \<union> C2 \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
  apply (simp add: connected_space_eq_not_separated)
  apply (intro all_cong1)
  by (metis Un_absorb dual_order.antisym separatedin_def subset_refl sup_mono)

lemma connectedin_subset_separated_union:
     "\<lbrakk>connectedin X C; separatedin X S T; C \<subseteq> S \<union> T\<rbrakk> \<Longrightarrow> C \<subseteq> S \<or> C \<subseteq> T"
  unfolding connectedin_eq_not_separated_subset  by blast

lemma connectedin_nonseparated_union:
   "\<lbrakk>connectedin X S; connectedin X T; \<not>separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
  apply (simp add: connectedin_eq_not_separated_subset, auto)
    apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
  apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
  by (meson disjoint_iff_not_equal)

lemma connected_space_closures:
     "connected_space X \<longleftrightarrow>
        (\<nexists>e1 e2. e1 \<union> e2 = topspace X \<and> X closure_of e1 \<inter> X closure_of e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding connected_space_closedin_eq
    by (metis Un_upper1 Un_upper2 closedin_closure_of closure_of_Un closure_of_eq_empty closure_of_topspace)
next
  assume ?rhs
  then show ?lhs
    unfolding connected_space_closedin_eq
    by (metis closure_of_eq)
qed

lemma connectedin_inter_frontier_of:
  assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
  shows "S \<inter> X frontier_of T \<noteq> {}"
proof -
  have "S \<subseteq> topspace X" and *:
    "\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
    using \<open>connectedin X S\<close> by (auto simp: connectedin)
  have "S - (topspace X \<inter> T) \<noteq> {}"
    using assms(3) by blast
  moreover
  have "S \<inter> topspace X \<inter> T \<noteq> {}"
    using assms(1) assms(2) connectedin by fastforce
  moreover
  have False if "S \<inter> T \<noteq> {}" "S - T \<noteq> {}" "T \<subseteq> topspace X" "S \<inter> X frontier_of T = {}" for T
  proof -
    have null: "S \<inter> (X closure_of T - X interior_of T) = {}"
      using that unfolding frontier_of_def by blast
    have 1: "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
      by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty)
    have 2: "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
      using that \<open>S \<subseteq> topspace X\<close> null by auto
    have 3: "S \<inter> X interior_of T \<noteq> {}"
      using closure_of_subset that(1) that(3) null by fastforce
    show ?thesis
      using null \<open>S \<subseteq> topspace X\<close> that * [of "X interior_of T" "topspace X - X closure_of T"]
      apply (clarsimp simp add: openin_diff 1 2)
      apply (simp add: Int_commute Diff_Int_distrib 3)
      by (metis Int_absorb2 contra_subsetD interior_of_subset)
  qed
  ultimately show ?thesis
    by (metis Int_lower1 frontier_of_restrict inf_assoc)
qed

lemma connectedin_continuous_map_image:
  assumes f: "continuous_map X Y f" and "connectedin X S"
  shows "connectedin Y (f ` S)"
proof -
  have "S \<subseteq> topspace X" and *:
    "\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
    using \<open>connectedin X S\<close> by (auto simp: connectedin)
  show ?thesis
    unfolding connectedin connected_space_def
  proof (intro conjI notI; clarify)
    show "f x \<in> topspace Y" if  "x \<in> S" for x
      using \<open>S \<subseteq> topspace X\<close> continuous_map_image_subset_topspace f that by blast
  next
    fix U V
    let ?U = "{x \<in> topspace X. f x \<in> U}"
    let ?V = "{x \<in> topspace X. f x \<in> V}"
    assume UV: "openin Y U" "openin Y V" "f ` S \<subseteq> U \<union> V" "U \<inter> V \<inter> f ` S = {}" "U \<inter> f ` S \<noteq> {}" "V \<inter> f ` S \<noteq> {}"
    then have 1: "?U \<inter> ?V \<inter> S = {}"
      by auto
    have 2: "openin X ?U" "openin X ?V"
      using \<open>openin Y U\<close> \<open>openin Y V\<close> continuous_map f by fastforce+
    show "False"
      using  * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
      by (auto simp: 1 2)
  qed
qed

lemma homeomorphic_connected_space:
     "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
  unfolding homeomorphic_space_def homeomorphic_maps_def
  apply safe
  apply (metis connectedin_continuous_map_image connected_space_subconnected continuous_map_image_subset_topspace image_eqI image_subset_iff)
  by (metis (no_types, hide_lams) connectedin_continuous_map_image connectedin_topspace continuous_map_def continuous_map_image_subset_topspace imageI set_eq_subset subsetI)

lemma homeomorphic_map_connectedness:
  assumes f: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  shows "connectedin Y (f ` U) \<longleftrightarrow> connectedin X U"
proof -
  have 1: "f ` U \<subseteq> topspace Y \<longleftrightarrow> U \<subseteq> topspace X"
    using U f homeomorphic_imp_surjective_map by blast
  moreover have "connected_space (subtopology Y (f ` U)) \<longleftrightarrow> connected_space (subtopology X U)"
  proof (rule homeomorphic_connected_space)
    have "f ` U \<subseteq> topspace Y"
      by (simp add: U 1)
    then have "topspace Y \<inter> f ` U = f ` U"
      by (simp add: subset_antisym)
    then show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
      by (metis (no_types) Int_subset_iff U f homeomorphic_map_imp_homeomorphic_space homeomorphic_map_subtopologies homeomorphic_space_sym subset_antisym subset_refl)
  qed
  ultimately show ?thesis
    by (auto simp: connectedin_def)
qed

lemma homeomorphic_map_connectedness_eq:
   "homeomorphic_map X Y f
        \<Longrightarrow> connectedin X U \<longleftrightarrow>
             U \<subseteq> topspace X \<and> connectedin Y (f ` U)"
  using homeomorphic_map_connectedness connectedin_subset_topspace by metis

lemma connectedin_discrete_topology:
   "connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
proof (cases "S \<subseteq> U")
  case True
  show ?thesis
  proof (cases "S = {}")
    case False
    moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
      apply safe
      using False connectedin_inter_frontier_of insert_Diff apply fastforce
      using True by auto
    ultimately show ?thesis
      by auto
  qed simp
next
  case False
  then show ?thesis
    by (simp add: connectedin_def)
qed

lemma connected_space_discrete_topology:
     "connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
  by (metis connectedin_discrete_topology connectedin_topspace order_refl topspace_discrete_topology)


subsection\<open>Compact sets\<close>

definition compactin where
 "compactin X S \<longleftrightarrow>
     S \<subseteq> topspace X \<and>
     (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
          \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>))"

definition compact_space where
   "compact_space X \<equiv> compactin X (topspace X)"

lemma compact_space_alt:
   "compact_space X \<longleftrightarrow>
        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
            \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>))"
  by (simp add: compact_space_def compactin_def)

lemma compact_space:
   "compact_space X \<longleftrightarrow>
        (\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
            \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> \<Union>\<F> = topspace X))"
  unfolding compact_space_alt
  using openin_subset by fastforce

lemma compactin_euclidean_iff [simp]: "compactin euclidean S \<longleftrightarrow> compact S"
  by (simp add: compact_eq_Heine_Borel compactin_def) meson

lemma compactin_absolute [simp]:
   "compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
proof -
  have eq: "(\<forall>U \<in> \<U>. \<exists>Y. openin X Y \<and> U = Y \<inter> S) \<longleftrightarrow> \<U> \<subseteq> (\<lambda>Y. Y \<inter> S) ` {y. openin X y}" for \<U>
    by auto
  show ?thesis
    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
qed

lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
  unfolding compact_space_def topspace_subtopology
  by (metis compactin_absolute compactin_def inf.absorb2)

lemma compact_space_subtopology: "compactin X S \<Longrightarrow> compact_space (subtopology X S)"
  by (simp add: compactin_subspace)

lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
apply (simp add: compactin_subspace topspace_subtopology)
  by (metis inf.orderE inf_commute subtopology_subtopology)


lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
  by (simp add: compactin_subspace)

lemma compactin_contractive:
   "\<lbrakk>compactin X' S; topspace X' = topspace X;
     \<And>U. openin X U \<Longrightarrow> openin X' U\<rbrakk> \<Longrightarrow> compactin X S"
  by (simp add: compactin_def)

lemma finite_imp_compactin:
   "\<lbrakk>S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> compactin X S"
  by (metis compactin_subspace compact_space finite_UnionD inf.absorb_iff2 order_refl topspace_subtopology)

lemma compactin_empty [iff]: "compactin X {}"
  by (simp add: finite_imp_compactin)

lemma compact_space_topspace_empty:
   "topspace X = {} \<Longrightarrow> compact_space X"
  by (simp add: compact_space_def)

lemma finite_imp_compactin_eq:
   "finite S \<Longrightarrow> (compactin X S \<longleftrightarrow> S \<subseteq> topspace X)"
  using compactin_subset_topspace finite_imp_compactin by blast

lemma compactin_sing [simp]: "compactin X {a} \<longleftrightarrow> a \<in> topspace X"
  by (simp add: finite_imp_compactin_eq)

lemma closed_compactin:
  assumes XK: "compactin X K" and "C \<subseteq> K" and XC: "closedin X C"
  shows "compactin X C"
  unfolding compactin_def
proof (intro conjI allI impI)
  show "C \<subseteq> topspace X"
    by (simp add: XC closedin_subset)
next
  fix \<U> :: "'a set set"
  assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
  have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
    using XC \<U> by blast
  moreover have "K \<subseteq> \<Union>(insert (topspace X - C) \<U>)"
    using \<U> XK compactin_subset_topspace by fastforce
  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
    using assms unfolding compactin_def by metis
  moreover have "openin X (topspace X - C)"
    using XC by auto
  ultimately show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> C \<subseteq> \<Union>\<F>"
    using \<open>C \<subseteq> K\<close>
    by (rule_tac x="\<F> - {topspace X - C}" in exI) auto
qed

lemma closedin_compact_space:
   "\<lbrakk>compact_space X; closedin X S\<rbrakk> \<Longrightarrow> compactin X S"
  by (simp add: closed_compactin closedin_subset compact_space_def)

lemma compact_Int_closedin:
  assumes "compactin X S" "closedin X T" shows "compactin X (S \<inter> T)"
proof -
  have "compactin (subtopology X S) (S \<inter> T)"
    by (metis assms closedin_compact_space closedin_subtopology compactin_subspace inf_commute)
  then show ?thesis
    by (simp add: compactin_subtopology)
qed

lemma closed_Int_compactin: "\<lbrakk>closedin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
  by (metis compact_Int_closedin inf_commute)

lemma compactin_Un:
  assumes S: "compactin X S" and T: "compactin X T" shows "compactin X (S \<union> T)"
  unfolding compactin_def
proof (intro conjI allI impI)
  show "S \<union> T \<subseteq> topspace X"
    using assms by (auto simp: compactin_def)
next
  fix \<U> :: "'a set set"
  assume \<U>: "Ball \<U> (openin X) \<and> S \<union> T \<subseteq> \<Union>\<U>"
  with S obtain \<F> where \<V>: "finite \<F>" "\<F> \<subseteq> \<U>" "S \<subseteq> \<Union>\<F>"
    unfolding compactin_def by (meson sup.bounded_iff)
  obtain \<W> where "finite \<W>" "\<W> \<subseteq> \<U>" "T \<subseteq> \<Union>\<W>"
    using \<U> T
    unfolding compactin_def by (meson sup.bounded_iff)
  with \<V> show "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> S \<union> T \<subseteq> \<Union>\<V>"
    by (rule_tac x="\<F> \<union> \<W>" in exI) auto
qed

lemma compactin_Union:
   "\<lbrakk>finite \<F>; \<And>S. S \<in> \<F> \<Longrightarrow> compactin X S\<rbrakk> \<Longrightarrow> compactin X (\<Union>\<F>)"
by (induction rule: finite_induct) (simp_all add: compactin_Un)

lemma compactin_subtopology_imp_compact:
  assumes "compactin (subtopology X S) K" shows "compactin X K"
  using assms
proof (clarsimp simp add: compactin_def topspace_subtopology)
  fix \<U>
  define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
  assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
  then have "\<forall>V \<in> \<V>. openin (subtopology X S) V" "K \<subseteq> \<Union>\<V>"
    unfolding \<V>_def by (auto simp: openin_subtopology)
  moreover
  assume "\<forall>\<U>. (\<forall>x\<in>\<U>. openin (subtopology X S) x) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
    by meson
  then have \<F>: "\<exists>U. U \<in> \<U> \<and> V = U \<inter> S" if "V \<in> \<F>" for V
    unfolding \<V>_def using that by blast
  let ?\<F> = "(\<lambda>F. @U. U \<in> \<U> \<and> F = U \<inter> S) ` \<F>"
  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
  proof (intro exI conjI)
    show "finite ?\<F>"
      using \<open>finite \<F>\<close> by blast
    show "?\<F> \<subseteq> \<U>"
      using someI_ex [OF \<F>] by blast
    show "K \<subseteq> \<Union>?\<F>"
    proof clarsimp
      fix x
      assume "x \<in> K"
      then show "\<exists>V \<in> \<F>. x \<in> (SOME U. U \<in> \<U> \<and> V = U \<inter> S)"
        using \<open>K \<subseteq> \<Union>\<F>\<close> someI_ex [OF \<F>]
        by (metis (no_types, lifting) IntD1 Union_iff subsetCE)
    qed
  qed
qed

lemma compact_imp_compactin_subtopology:
  assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
  using assms
proof (clarsimp simp add: compactin_def topspace_subtopology)
  fix \<U> :: "'a set set"
  define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
  assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
  then have "\<forall>V \<in> \<V>. openin X V" "K \<subseteq> \<Union>\<V>"
    unfolding \<V>_def by (fastforce simp: subset_eq openin_subtopology)+
  moreover
  assume "\<forall>\<U>. (\<forall>U\<in>\<U>. openin X U) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
    by meson
  let ?\<F> = "(\<lambda>F. F \<inter> S) ` \<F>"
  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
  proof (intro exI conjI)
    show "finite ?\<F>"
      using \<open>finite \<F>\<close> by blast
    show "?\<F> \<subseteq> \<U>"
      using \<V>_def \<open>\<F> \<subseteq> \<V>\<close> by blast
    show "K \<subseteq> \<Union>?\<F>"
      using \<open>K \<subseteq> \<Union>\<F>\<close> assms(2) by auto
  qed
qed


proposition compact_space_fip:
   "compact_space X \<longleftrightarrow>
    (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
   (is "_ = ?rhs")
proof (cases "topspace X = {}")
  case True
  then show ?thesis
    apply (clarsimp simp add: compact_space_def closedin_topspace_empty)
    by (metis finite.emptyI finite_insert infinite_super insertI1 subsetI)
next
  case False
  show ?thesis
  proof safe
    fix \<U> :: "'a set set"
    assume * [rule_format]: "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
    define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
    assume clo: "\<forall>C\<in>\<U>. closedin X C" and [simp]: "\<Inter>\<U> = {}"
    then have "\<forall>V \<in> \<V>. openin X V" "topspace X \<subseteq> \<Union>\<V>"
      by (auto simp: \<V>_def)
    moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
    ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
      by (auto simp: exists_finite_subset_image \<V>_def)
    moreover have "\<F> \<noteq> {}"
      using \<F> \<open>topspace X \<noteq> {}\<close> by blast
    ultimately show "False"
      using * [of \<F>]
      by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
  next
    assume R [rule_format]: ?rhs
    show "compact_space X"
      unfolding compact_space_alt
    proof clarify
      fix \<U> :: "'a set set"
      define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
      assume "\<forall>C\<in>\<U>. openin X C" and "topspace X \<subseteq> \<Union>\<U>"
      with \<open>topspace X \<noteq> {}\<close> have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
        by (auto simp: \<V>_def)
      show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>"
      proof (rule ccontr; simp)
        assume "\<forall>\<F>\<subseteq>\<U>. finite \<F> \<longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>"
        then have "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<V> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
          by (simp add: \<V>_def all_finite_subset_image)
        with \<open>topspace X \<subseteq> \<Union>\<U>\<close> show False
          using R [of \<V>] * by (simp add: \<V>_def)
      qed
    qed
  qed
qed

corollary compactin_fip:
  "compactin X S \<longleftrightarrow>
    S \<subseteq> topspace X \<and>
    (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
proof (cases "S = {}")
  case False
  show ?thesis
  proof (cases "S \<subseteq> topspace X")
    case True
    then have "compactin X S \<longleftrightarrow>
          (\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
           (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
      by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
    also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {})"
      by (simp add: all_subset_image)
    also have "\<dots> = (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
    proof -
      have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
                ((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"  for \<U>
        by simp (use \<open>S \<noteq> {}\<close> in blast)
      show ?thesis
        apply (simp only: imp_conjL [symmetric] all_finite_subset_image eq)
        apply (simp add: subset_eq)
        done
    qed
    finally show ?thesis
      using True by simp
  qed (simp add: compactin_subspace)
qed force

corollary compact_space_imp_nest:
  fixes C :: "nat \<Rightarrow> 'a set"
  assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
    and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
  shows "(\<Inter>n. C n) \<noteq> {}"
proof -
  let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
  have "closedin X A" if "A \<in> ?\<U>" for A
    using that clo by auto
  moreover have "(\<Inter>n\<in>K. \<Inter>m \<le> n. C m) \<noteq> {}" if "finite K" for K
  proof -
    obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
      using Max.coboundedI \<open>finite K\<close> by blast
    with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
    by blast
  with ne [of n] show ?thesis
    by blast
  qed
  ultimately show ?thesis
    using \<open>compact_space X\<close> [unfolded compact_space_fip, rule_format, of ?\<U>]
    by (simp add: all_finite_subset_image INT_extend_simps UN_atMost_UNIV del: INT_simps)
qed

lemma compactin_discrete_topology:
   "compactin (discrete_topology X) S \<longleftrightarrow> S \<subseteq> X \<and> finite S" (is "?lhs = ?rhs")
proof (intro iffI conjI)
  assume L: ?lhs
  then show "S \<subseteq> X"
    by (auto simp: compactin_def)
  have *: "\<And>\<U>. Ball \<U> (openin (discrete_topology X)) \<and> S \<subseteq> \<Union>\<U> \<Longrightarrow>
        (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>)"
    using L by (auto simp: compactin_def)
  show "finite S"
    using * [of "(\<lambda>x. {x}) ` X"] \<open>S \<subseteq> X\<close>
    by clarsimp (metis UN_singleton finite_subset_image infinite_super)
next
  assume ?rhs
  then show ?lhs
    by (simp add: finite_imp_compactin)
qed

lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
  by (simp add: compactin_discrete_topology compact_space_def)

lemma compact_space_imp_Bolzano_Weierstrass:
  assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
  shows "X derived_set_of S \<noteq> {}"
proof
  assume X: "X derived_set_of S = {}"
  then have "closedin X S"
    by (simp add: closedin_contains_derived_set assms)
  then have "compactin X S"
    by (rule closedin_compact_space [OF \<open>compact_space X\<close>])
  with X show False
    by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
qed

lemma compactin_imp_Bolzano_Weierstrass:
   "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
  using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
  by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)

lemma compact_closure_of_imp_Bolzano_Weierstrass:
   "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
  using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce

lemma discrete_compactin_eq_finite:
   "S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
  apply (rule iffI)
  using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
  by (simp add: finite_imp_compactin_eq)

lemma discrete_compact_space_eq_finite:
   "X derived_set_of (topspace X) = {} \<Longrightarrow> (compact_space X \<longleftrightarrow> finite(topspace X))"
  by (metis compact_space_discrete_topology discrete_topology_unique_derived_set)

lemma image_compactin:
  assumes cpt: "compactin X S" and cont: "continuous_map X Y f"
  shows "compactin Y (f ` S)"
  unfolding compactin_def
proof (intro conjI allI impI)
  show "f ` S \<subseteq> topspace Y"
    using compactin_subset_topspace cont continuous_map_image_subset_topspace cpt by blast
next
  fix \<U> :: "'b set set"
  assume \<U>: "Ball \<U> (openin Y) \<and> f ` S \<subseteq> \<Union>\<U>"
  define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
  have "S \<subseteq> topspace X"
    and *: "\<And>\<U>. \<lbrakk>\<forall>U\<in>\<U>. openin X U; S \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow> \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
    using cpt by (auto simp: compactin_def)
  obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<V>" "S \<subseteq> \<Union>\<F>"
  proof -
    have 1: "\<forall>U\<in>\<V>. openin X U"
      unfolding \<V>_def using \<U> cont[unfolded continuous_map] by blast
    have 2: "S \<subseteq> \<Union>\<V>"
      unfolding \<V>_def using compactin_subset_topspace cpt \<U> by fastforce
    show thesis
      using * [OF 1 2] that by metis
  qed
  have "\<forall>v \<in> \<V>. \<exists>U. U \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U}"
    using \<V>_def by blast
  then obtain U where U: "\<forall>v \<in> \<V>. U v \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U v}"
    by metis
  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> f ` S \<subseteq> \<Union>\<F>"
  proof (intro conjI exI)
    show "finite (U ` \<F>)"
      by (simp add: \<open>finite \<F>\<close>)
  next
    show "U ` \<F> \<subseteq> \<U>"
      using \<open>\<F> \<subseteq> \<V>\<close> U by auto
  next
    show "f ` S \<subseteq> \<Union> (U ` \<F>)"
      using \<F>(2-3) U UnionE subset_eq U by fastforce
  qed
qed


lemma homeomorphic_compact_space:
  assumes "X homeomorphic_space Y"
  shows "compact_space X \<longleftrightarrow> compact_space Y"
    using homeomorphic_space_sym
    by (metis assms compact_space_def homeomorphic_eq_everything_map homeomorphic_space image_compactin)

lemma homeomorphic_map_compactness:
  assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
  shows "compactin Y (f ` U) \<longleftrightarrow> compactin X U"
proof -
  have "f ` U \<subseteq> topspace Y"
    using hom U homeomorphic_imp_surjective_map by blast
  moreover have "homeomorphic_map (subtopology X U) (subtopology Y (f ` U)) f"
    using U hom homeomorphic_imp_surjective_map by (blast intro: homeomorphic_map_subtopologies)
  then have "compact_space (subtopology Y (f ` U)) = compact_space (subtopology X U)"
    using homeomorphic_compact_space homeomorphic_map_imp_homeomorphic_space by blast
  ultimately show ?thesis
    by (simp add: compactin_subspace U)
qed

lemma homeomorphic_map_compactness_eq:
   "homeomorphic_map X Y f
        \<Longrightarrow> compactin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> compactin Y (f ` U)"
  by (meson compactin_subset_topspace homeomorphic_map_compactness)


subsection\<open>Embedding maps\<close>

definition embedding_map
  where "embedding_map X Y f \<equiv> homeomorphic_map X (subtopology Y (f ` (topspace X))) f"

lemma embedding_map_eq:
   "\<lbrakk>embedding_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> embedding_map X Y g"
  unfolding embedding_map_def
  by (metis homeomorphic_map_eq image_cong)

lemma embedding_map_compose:
  assumes "embedding_map X X' f" "embedding_map X' X'' g"
  shows "embedding_map X X'' (g \<circ> f)"
proof -
  have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g"
    using assms by (auto simp: embedding_map_def)
  then obtain C where "g ` topspace X' \<inter> C = (g \<circ> f) ` topspace X"
    by (metis (no_types) Int_absorb1 continuous_map_image_subset_topspace continuous_map_in_subtopology homeomorphic_eq_everything_map image_comp image_mono)
  then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \<circ> f) ` topspace X)) g"
    by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
  then show ?thesis
  unfolding embedding_map_def
  using hm(1) homeomorphic_map_compose by blast
qed

lemma surjective_embedding_map:
   "embedding_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
  by (force simp: embedding_map_def homeomorphic_eq_everything_map)

lemma embedding_map_in_subtopology:
   "embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
  apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
    apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
  apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
  done

lemma injective_open_imp_embedding_map:
   "\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
  unfolding embedding_map_def
  apply (rule bijective_open_imp_homeomorphic_map)
  using continuous_map_in_subtopology apply blast
    apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
  done

lemma injective_closed_imp_embedding_map:
  "\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
  unfolding embedding_map_def
  apply (rule bijective_closed_imp_homeomorphic_map)
     apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
  apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
  done

lemma embedding_map_imp_homeomorphic_space:
   "embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
  unfolding embedding_map_def
  using homeomorphic_space by blast


subsection\<open>Retraction and section maps\<close>

definition retraction_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
  where "retraction_maps X Y f g \<equiv>
           continuous_map X Y f \<and> continuous_map Y X g \<and> (\<forall>x \<in> topspace Y. f(g x) = x)"

definition section_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  where "section_map X Y f \<equiv> \<exists>g. retraction_maps Y X g f"

definition retraction_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  where "retraction_map X Y f \<equiv> \<exists>g. retraction_maps X Y f g"

lemma retraction_maps_eq:
   "\<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>
        \<Longrightarrow> retraction_maps X Y f' g'"
  unfolding retraction_maps_def by (metis (no_types, lifting) continuous_map_def continuous_map_eq)

lemma section_map_eq:
   "\<lbrakk>section_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> section_map X Y g"
  unfolding section_map_def using retraction_maps_eq by blast

lemma retraction_map_eq:
   "\<lbrakk>retraction_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> retraction_map X Y g"
  unfolding retraction_map_def using retraction_maps_eq by blast

lemma homeomorphic_imp_retraction_maps:
   "homeomorphic_maps X Y f g \<Longrightarrow> retraction_maps X Y f g"
  by (simp add: homeomorphic_maps_def retraction_maps_def)

lemma section_and_retraction_eq_homeomorphic_map:
   "section_map X Y f \<and> retraction_map X Y f \<longleftrightarrow> homeomorphic_map X Y f"
  apply (auto simp: section_map_def retraction_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def)
  by (metis (full_types) continuous_map_image_subset_topspace image_subset_iff)

lemma section_imp_embedding_map:
   "section_map X Y f \<Longrightarrow> embedding_map X Y f"
  unfolding section_map_def embedding_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def
  by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology topspace_subtopology)

lemma retraction_imp_quotient_map:
  assumes "retraction_map X Y f"
  shows "quotient_map X Y f"
  unfolding quotient_map_def
proof (intro conjI subsetI allI impI)
  show "f ` topspace X = topspace Y"
    using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def)
next
  fix U
  assume U: "U \<subseteq> topspace Y"
  have "openin Y U"
    if "\<forall>x\<in>topspace Y. g x \<in> topspace X" "\<forall>x\<in>topspace Y. f (g x) = x"
       "openin Y {x \<in> topspace Y. g x \<in> {x \<in> topspace X. f x \<in> U}}" for g
    using openin_subopen U that by fastforce
  then show "openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
    using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def)
qed

lemma retraction_maps_compose:
   "\<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')"
  by (clarsimp simp: retraction_maps_def continuous_map_compose) (simp add: continuous_map_def)

lemma retraction_map_compose:
   "\<lbrakk>retraction_map X Y f; retraction_map Y Z g\<rbrakk> \<Longrightarrow> retraction_map X Z (g \<circ> f)"
  by (meson retraction_map_def retraction_maps_compose)

lemma section_map_compose:
   "\<lbrakk>section_map X Y f; section_map Y Z g\<rbrakk> \<Longrightarrow> section_map X Z (g \<circ> f)"
  by (meson retraction_maps_compose section_map_def)

lemma surjective_section_eq_homeomorphic_map:
   "section_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
  by (meson section_and_retraction_eq_homeomorphic_map section_imp_embedding_map surjective_embedding_map)

lemma surjective_retraction_or_section_map:
   "f ` (topspace X) = topspace Y \<Longrightarrow> retraction_map X Y f \<or> section_map X Y f \<longleftrightarrow> retraction_map X Y f"
  using section_and_retraction_eq_homeomorphic_map surjective_section_eq_homeomorphic_map by fastforce

lemma retraction_imp_surjective_map:
   "retraction_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
  by (simp add: retraction_imp_quotient_map quotient_imp_surjective_map)

lemma section_imp_injective_map:
   "\<lbrakk>section_map X Y f; x \<in> topspace X; y \<in> topspace X\<rbrakk> \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
  by (metis (mono_tags, hide_lams) retraction_maps_def section_map_def)

lemma retraction_maps_to_retract_maps:
   "retraction_maps X Y r s
        \<Longrightarrow> retraction_maps X (subtopology X (s ` (topspace Y))) (s \<circ> r) id"
  unfolding retraction_maps_def
  by (auto simp: continuous_map_compose continuous_map_into_subtopology continuous_map_from_subtopology)
subsection \<open>Continuity\<close>

lemma continuous_on_open:
  "continuous_on S f \<longleftrightarrow>
    (\<forall>T. openin (top_of_set (f ` S)) T \<longrightarrow>
      openin (top_of_set S) (S \<inter> f -` T))"
  unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)

lemma continuous_on_closed:
  "continuous_on S f \<longleftrightarrow>
    (\<forall>T. closedin (top_of_set (f ` S)) T \<longrightarrow>
      closedin (top_of_set S) (S \<inter> f -` T))"
  unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)

lemma continuous_on_imp_closedin:
  assumes "continuous_on S f" "closedin (top_of_set (f ` S)) T"
  shows "closedin (top_of_set S) (S \<inter> f -` T)"
  using assms continuous_on_closed by blast

subsection%unimportant \<open>Half-global and completely global cases\<close>

lemma continuous_openin_preimage_gen:
  assumes "continuous_on S f"  "open T"
  shows "openin (top_of_set S) (S \<inter> f -` T)"
proof -
  have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
    by auto
  have "openin (top_of_set (f ` S)) (T \<inter> f ` S)"
    using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
  then show ?thesis
    using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
    using * by auto
qed

lemma continuous_closedin_preimage:
  assumes "continuous_on S f" and "closed T"
  shows "closedin (top_of_set S) (S \<inter> f -` T)"
proof -
  have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
    by auto
  have "closedin (top_of_set (f ` S)) (T \<inter> f ` S)"
    using closedin_closed_Int[of T "f ` S", OF assms(2)]
    by (simp add: Int_commute)
  then show ?thesis
    using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
    using * by auto
qed

lemma continuous_openin_preimage_eq:
   "continuous_on S f \<longleftrightarrow>
    (\<forall>T. open T \<longrightarrow> openin (top_of_set S) (S \<inter> f -` T))"
apply safe
apply (simp add: continuous_openin_preimage_gen)
apply (fastforce simp add: continuous_on_open openin_open)
done

lemma continuous_closedin_preimage_eq:
   "continuous_on S f \<longleftrightarrow>
    (\<forall>T. closed T \<longrightarrow> closedin (top_of_set S) (S \<inter> f -` T))"
apply safe
apply (simp add: continuous_closedin_preimage)
apply (fastforce simp add: continuous_on_closed closedin_closed)
done

lemma continuous_open_preimage:
  assumes contf: "continuous_on S f" and "open S" "open T"
  shows "open (S \<inter> f -` T)"
proof-
  obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
    using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
    unfolding openin_open by auto
  then show ?thesis
    using open_Int[of S U, OF \<open>open S\<close>] by auto
qed

lemma continuous_closed_preimage:
  assumes contf: "continuous_on S f" and "closed S" "closed T"
  shows "closed (S \<inter> f -` T)"
proof-
  obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
    using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
    unfolding closedin_closed by auto
  then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
qed

lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
  by (metis continuous_on_eq_continuous_within open_vimage) 
 
lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
  by (simp add: closed_vimage continuous_on_eq_continuous_within)

lemma Times_in_interior_subtopology:
  assumes "(x, y) \<in> U" "openin (top_of_set (S \<times> T)) U"
  obtains V W where "openin (top_of_set S) V" "x \<in> V"
                    "openin (top_of_set T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
proof -
  from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T"
    by (auto simp: openin_open)
  from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>]
  obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E"
    by blast
  show ?thesis
  proof
    show "openin (top_of_set S) (E1 \<inter> S)"
      "openin (top_of_set T) (E2 \<inter> T)"
      using \<open>open E1\<close> \<open>open E2\<close>
      by (auto simp: openin_open)
    show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T"
      using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
    show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
      using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
      by (auto simp: )
  qed
qed

lemma closedin_Times:
  "closedin (top_of_set S) S' \<Longrightarrow> closedin (top_of_set T) T' \<Longrightarrow>
    closedin (top_of_set (S \<times> T)) (S' \<times> T')"
  unfolding closedin_closed using closed_Times by blast

lemma openin_Times:
  "openin (top_of_set S) S' \<Longrightarrow> openin (top_of_set T) T' \<Longrightarrow>
    openin (top_of_set (S \<times> T)) (S' \<times> T')"
  unfolding openin_open using open_Times by blast

lemma openin_Times_eq:
  fixes S :: "'a::topological_space set" and T :: "'b::topological_space set"
  shows
    "openin (top_of_set (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
      S' = {} \<or> T' = {} \<or> openin (top_of_set S) S' \<and> openin (top_of_set T) T'"
    (is "?lhs = ?rhs")
proof (cases "S' = {} \<or> T' = {}")
  case True
  then show ?thesis by auto
next
  case False
  then obtain x y where "x \<in> S'" "y \<in> T'"
    by blast
  show ?thesis
  proof
    assume ?lhs
    have "openin (top_of_set S) S'"
      apply (subst openin_subopen, clarify)
      apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
      using \<open>y \<in> T'\<close>
       apply auto
      done
    moreover have "openin (top_of_set T) T'"
      apply (subst openin_subopen, clarify)
      apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
      using \<open>x \<in> S'\<close>
       apply auto
      done
    ultimately show ?rhs
      by simp
  next
    assume ?rhs
    with False show ?lhs
      by (simp add: openin_Times)
  qed
qed

lemma Lim_transform_within_openin:
  assumes f: "(f \<longlongrightarrow> l) (at a within T)"
    and "openin (top_of_set T) S" "a \<in> S"
    and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
  shows "(g \<longlongrightarrow> l) (at a within T)"
proof -
  have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a"
    by (simp add: eventually_at_filter)
  moreover
  from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U"
    by (auto simp: openin_open)
  then have "a \<in> U" using \<open>a \<in> S\<close> by auto
  from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>]
  have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto
  ultimately
  have "\<forall>\<^sub>F x in at a within T. f x = g x"
    by eventually_elim (auto simp: \<open>S = _\<close> eq)
  then show ?thesis using f
    by (rule Lim_transform_eventually)
qed

lemma continuous_on_open_gen:
  assumes "f ` S \<subseteq> T"
    shows "continuous_on S f \<longleftrightarrow>
             (\<forall>U. openin (top_of_set T) U
                  \<longrightarrow> openin (top_of_set S) (S \<inter> f -` U))"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (clarsimp simp add: continuous_openin_preimage_eq openin_open)
      (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1)
next
  assume R [rule_format]: ?rhs
  show ?lhs
  proof (clarsimp simp add: continuous_openin_preimage_eq)
    fix U::"'a set"
    assume "open U"
    then have "openin (top_of_set S) (S \<inter> f -` (U \<inter> T))"
      by (metis R inf_commute openin_open)
    then show "openin (top_of_set S) (S \<inter> f -` U)"
      by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int)
  qed
qed

lemma continuous_openin_preimage:
  "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (top_of_set T) U\<rbrakk>
        \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` U)"
  by (simp add: continuous_on_open_gen)

lemma continuous_on_closed_gen:
  assumes "f ` S \<subseteq> T"
  shows "continuous_on S f \<longleftrightarrow>
             (\<forall>U. closedin (top_of_set T) U
                  \<longrightarrow> closedin (top_of_set S) (S \<inter> f -` U))"
    (is "?lhs = ?rhs")
proof -
  have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
    using assms by blast
  show ?thesis
  proof
    assume L: ?lhs
    show ?rhs
    proof clarify
      fix U
      assume "closedin (top_of_set T) U"
      then show "closedin (top_of_set S) (S \<inter> f -` U)"
        using L unfolding continuous_on_open_gen [OF assms]
        by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
    qed
  next
    assume R [rule_format]: ?rhs
    show ?lhs
      unfolding continuous_on_open_gen [OF assms]
      by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
  qed
qed

lemma continuous_closedin_preimage_gen:
  assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (top_of_set T) U"
    shows "closedin (top_of_set S) (S \<inter> f -` U)"
using assms continuous_on_closed_gen by blast

lemma continuous_transform_within_openin:
  assumes "continuous (at a within T) f"
    and "openin (top_of_set T) S" "a \<in> S"
    and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  shows "continuous (at a within T) g"
  using assms by (simp add: Lim_transform_within_openin continuous_within)


subsection%important \<open>The topology generated by some (open) subsets\<close>

text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
and is never a problem in proofs, so I prefer to write it down explicitly.

We do not require \<open>UNIV\<close> to be an open set, as this will not be the case in applications. (We are
thinking of a topology on a subset of \<open>UNIV\<close>, the remaining part of \<open>UNIV\<close> being irrelevant.)\<close>

inductive generate_topology_on for S where
  Empty: "generate_topology_on S {}"
| Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
| Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"

lemma istopology_generate_topology_on:
  "istopology (generate_topology_on S)"
unfolding istopology_def by (auto intro: generate_topology_on.intros)

text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
smallest topology containing all the elements of \<open>S\<close>:\<close>

lemma generate_topology_on_coarsest:
  assumes "istopology T"
          "\<And>s. s \<in> S \<Longrightarrow> T s"
          "generate_topology_on S s0"
  shows "T s0"
using assms(3) apply (induct rule: generate_topology_on.induct)
using assms(1) assms(2) unfolding istopology_def by auto

abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
  where "topology_generated_by S \<equiv> topology (generate_topology_on S)"

lemma openin_topology_generated_by_iff:
  "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
  using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp

lemma openin_topology_generated_by:
  "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
using openin_topology_generated_by_iff by auto

lemma topology_generated_by_topspace:
  "topspace (topology_generated_by S) = (\<Union>S)"
proof
  {
    fix s assume "openin (topology_generated_by S) s"
    then have "generate_topology_on S s" by (rule openin_topology_generated_by)
    then have "s \<subseteq> (\<Union>S)" by (induct, auto)
  }
  then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
    unfolding topspace_def by auto
next
  have "generate_topology_on S (\<Union>S)"
    using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
  then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
    unfolding topspace_def using openin_topology_generated_by_iff by auto
qed

lemma topology_generated_by_Basis:
  "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
  by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)

lemma generate_topology_on_Inter:
  "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
  by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)

subsection\<open>Topology bases and sub-bases\<close>

lemma istopology_base_alt:
   "istopology (arbitrary union_of P) \<longleftrightarrow>
    (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
           \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
  by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)

lemma istopology_base_eq:
   "istopology (arbitrary union_of P) \<longleftrightarrow>
    (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
  by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)

lemma istopology_base:
   "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
  by (simp add: arbitrary_def istopology_base_eq union_of_inc)

lemma openin_topology_base_unique:
   "openin X = arbitrary union_of P \<longleftrightarrow>
        (\<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))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: union_of_def arbitrary_def)
next
  assume R: ?rhs
  then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
    using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
  from R show ?lhs
    by (fastforce simp add: union_of_def arbitrary_def intro: *)
qed

lemma topology_base_unique:
   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
     \<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>
    \<Longrightarrow> topology(arbitrary union_of P) = X"
  by (metis openin_topology_base_unique openin_inverse [of X])

lemma topology_bases_eq_aux:
   "\<lbrakk>(arbitrary union_of P) S;
     \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
        \<Longrightarrow> (arbitrary union_of Q) S"
  by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)

lemma topology_bases_eq:
   "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
    \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
        \<Longrightarrow> topology (arbitrary union_of P) =
            topology (arbitrary union_of Q)"
  by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)

lemma istopology_subbase:
   "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
  by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)

lemma openin_subbase:
  "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
   \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
  by (simp add: istopology_subbase topology_inverse')

lemma topspace_subbase [simp]:
   "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
proof
  show "?lhs \<subseteq> U"
    by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
  show "U \<subseteq> ?lhs"
    by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
              openin_subset relative_to_inc subset_UNIV topology_inverse')
qed

lemma minimal_topology_subbase:
   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
     openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
    \<Longrightarrow> openin X S"
  apply (simp add: istopology_subbase topology_inverse)
  apply (simp add: union_of_def intersection_of_def relative_to_def)
  apply (blast intro: openin_Int_Inter)
  done

lemma istopology_subbase_UNIV:
   "istopology (arbitrary union_of (finite intersection_of P))"
  by (simp add: istopology_base finite_intersection_of_Int)


lemma generate_topology_on_eq:
  "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
proof (intro ext iffI)
  fix A
  assume "?lhs A"
  then show "?rhs A"
  proof induction
    case (Int a b)
    then show ?case
      by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
  next
    case (UN K)
    then show ?case
      by (simp add: arbitrary_union_of_Union)
  next
    case (Basis s)
    then show ?case
      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
  qed auto
next
  fix A
  assume "?rhs A"
  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>"
    unfolding union_of_def intersection_of_def by auto
  show "?lhs A"
    unfolding eq
  proof (rule generate_topology_on.UN)
    fix T
    assume "T \<in> \<U>"
    with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
      by blast
    have "generate_topology_on S (\<Inter>\<F>)"
    proof (rule generate_topology_on_Inter)
      show "finite \<F>" "\<F> \<noteq> {}"
        by (auto simp: \<open>finite' \<F>\<close>)
      show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
        by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
    qed
    then show "generate_topology_on S T"
      using \<open>\<Inter>\<F> = T\<close> by blast
  qed
qed

subsubsection%important \<open>Continuity\<close>

text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
of type classes, as defined below.\<close>

definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"

lemma continuous_on_continuous_on_topo:
  "continuous_on s f \<longleftrightarrow> continuous_on_topo (top_of_set s) euclidean f"
  by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq)

lemma continuous_on_topo_UNIV:
  "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto

lemma continuous_on_topo_open [intro]:
  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
  unfolding continuous_on_topo_def by auto

lemma continuous_on_topo_topspace [intro]:
  "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
unfolding continuous_on_topo_def by auto

lemma continuous_on_generated_topo_iff:
  "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
      ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
unfolding continuous_on_topo_def topology_generated_by_topspace
proof (auto simp add: topology_generated_by_Basis)
  assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
  fix U assume "openin (topology_generated_by S) U"
  then have "generate_topology_on S U" by (rule openin_topology_generated_by)
  then show "openin T1 (f -` U \<inter> topspace T1)"
  proof (induct)
    fix a b
    assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
    have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
      by auto
    then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
  next
    fix K
    assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
    define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
    have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
    have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
    moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
    ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
  qed (auto simp add: H)
qed

lemma continuous_on_generated_topo:
  assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
          "f`(topspace T1) \<subseteq> (\<Union> S)"
  shows "continuous_on_topo T1 (topology_generated_by S) f"
  using assms continuous_on_generated_topo_iff by blast

proposition continuous_on_topo_compose:
  assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
  shows "continuous_on_topo T1 T3 (g o f)"
  using assms unfolding continuous_on_topo_def
proof (auto)
  fix U :: "'c set"
  assume H: "openin T3 U"
  have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
    using H assms by blast
  moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
    using H assms continuous_on_topo_topspace by fastforce
  ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
    by simp
qed (blast)

lemma continuous_on_topo_preimage_topspace [intro]:
  assumes "continuous_on_topo T1 T2 f"
  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
using assms unfolding continuous_on_topo_def by auto


subsubsection%important \<open>Pullback topology\<close>

text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
a special case of this notion, pulling back by the identity. We introduce the general notion as
we will need it to define the strong operator topology on the space of continuous linear operators,
by pulling back the product topology on the space of all functions.\<close>

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
the set \<open>A\<close>.\<close>

definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
  where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"

lemma istopology_pullback_topology:
  "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
  unfolding istopology_def proof (auto)
  fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
  then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
    by (rule bchoice)
  then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
    by blast
  define V where "V = (\<Union>S\<in>K. U S)"
  have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
  then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
qed

lemma openin_pullback_topology:
  "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto

lemma topspace_pullback_topology:
  "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
by (auto simp add: topspace_def openin_pullback_topology)

proposition continuous_on_topo_pullback [intro]:
  assumes "continuous_on_topo T1 T2 g"
  shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
unfolding continuous_on_topo_def
proof (auto)
  fix U::"'b set" assume "openin T2 U"
  then have "openin T1 (g-`U \<inter> topspace T1)"
    using assms unfolding continuous_on_topo_def by auto
  have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
    unfolding topspace_pullback_topology by auto
  also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
    by auto
  also have "openin (pullback_topology A f T1) (...)"
    unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
  finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
    by auto
next
  fix x assume "x \<in> topspace (pullback_topology A f T1)"
  then have "f x \<in> topspace T1"
    unfolding topspace_pullback_topology by auto
  then show "g (f x) \<in> topspace T2"
    using assms unfolding continuous_on_topo_def by auto
qed

proposition continuous_on_topo_pullback' [intro]:
  assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
  shows "continuous_on_topo T1 (pullback_topology A f T2) g"
unfolding continuous_on_topo_def
proof (auto)
  fix U assume "openin (pullback_topology A f T2) U"
  then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
    unfolding openin_pullback_topology by auto
  then obtain V where "openin T2 V" "U = f-`V \<inter> A"
    by blast
  then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
    by blast
  also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
    by auto
  also have "... = (f o g)-`V \<inter> topspace T1"
    using assms(2) by auto
  also have "openin T1 (...)"
    using assms(1) \<open>openin T2 V\<close> by auto
  finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
next
  fix x assume "x \<in> topspace T1"
  have "(f o g) x \<in> topspace T2"
    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
  then have "g x \<in> f-`(topspace T2)"
    unfolding comp_def by blast
  moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
  ultimately show "g x \<in> topspace (pullback_topology A f T2)"
    unfolding topspace_pullback_topology by blast
qed

end