Theory HOL-Analysis.Abstract_Topology

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

section ‹Operators involving abstract topology›

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

subsection ‹General notion of a topology as a value›

definition✐‹tag important› istopology :: "('a set ⇒ bool) ⇒ bool" where
  "istopology L ≡ (∀S T. L S ⟶ L T ⟶ L (S ∩ T)) ∧ (∀𝒦. (∀K∈𝒦. L K) ⟶ L (⋃𝒦))"

typedef✐‹tag important› 'a topology = "{L::('a set) ⇒ bool. istopology L}"
  morphisms "openin" "topology"
  unfolding istopology_def by blast

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

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

lemma topology_inverse' [simp]: "istopology U ⟹ openin (topology U) = U"
  using topology_inverse[unfolded mem_Collect_eq] .

lemma topology_inverse_iff: "istopology U ⟷ openin (topology U) = U"
  by (metis istopology_openin topology_inverse')

lemma topology_eq: "T1 = T2 ⟷ (∀S. openin T1 S ⟷ openin T2 S)"
proof
  assume "T1 = T2"
  then show "∀S. openin T1 S ⟷ openin T2 S" by simp
next
  assume H: "∀S. openin T1 S ⟷ 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‹The "universe": the union of all sets in the topology.›
definition "topspace T = ⋃{S. openin T S}"

subsubsection ‹Main properties of open sets›

proposition openin_clauses:
  fixes U :: "'a topology"
  shows
    "openin U {}"
    "⋀S T. openin U S ⟹ openin U T ⟹ openin U (S∩T)"
    "⋀K. (∀S ∈ K. openin U S) ⟹ openin U (⋃K)"
  using openin[of U] unfolding istopology_def by auto

lemma openin_subset: "openin U S ⟹ S ⊆ topspace U"
  unfolding topspace_def by blast

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

lemma openin_Int[intro]: "openin U S ⟹ openin U T ⟹ openin U (S ∩ T)"
  by (rule openin_clauses)

lemma openin_Union[intro]: "(⋀S. S ∈ K ⟹ openin U S) ⟹ openin U (⋃K)"
  using openin_clauses by blast

lemma openin_Un[intro]: "openin U S ⟹ openin U T ⟹ openin U (S ∪ 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 ⟷ (∀x ∈ S. ∃T. openin U T ∧ x ∈ T ∧ T ⊆ S)"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then show ?rhs by auto
next
  assume H: ?rhs
  let ?t = "⋃{T. openin U T ∧ T ⊆ 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"
          "⋀i. i ∈ I ⟹ openin T (U i)"
  shows "openin T ((⋂i ∈ I. U i) ∩ topspace T)"
using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)

lemma openin_INT2 [intro]:
  assumes "finite I" "I ≠ {}"
          "⋀i. i ∈ I ⟹ openin T (U i)"
  shows "openin T (⋂i ∈ I. U i)"
proof -
  have "(⋂i ∈ I. U i) ⊆ topspace T"
    using ‹I ≠ {}› 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 ℱ" "ℱ ≠ {}" "⋀X. X ∈ ℱ ⟹ openin T X" shows "openin T (⋂ℱ)"
  by (metis (full_types) assms openin_INT2 image_ident)

lemma openin_Int_Inter:
  assumes "finite ℱ" "openin T U" "⋀X. X ∈ ℱ ⟹ openin T X" shows "openin T (U ∩ ⋂ℱ)"
  using openin_Inter [of "insert U ℱ"] assms by auto


subsubsection ‹Closed sets›

definition✐‹tag important› closedin :: "'a topology ⇒ 'a set ⇒ bool" where
"closedin U S ⟷ S ⊆ topspace U ∧ openin U (topspace U - S)"

lemma closedin_subset: "closedin U S ⟹ S ⊆ 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 ⟹ closedin U T ⟹ closedin U (S ∪ T)"
  by (auto simp: Diff_Un closedin_def)

lemma Diff_Inter[intro]: "A - ⋂S = ⋃{A - s|s. s∈S}"
  by auto

lemma closedin_Union:
  assumes "finite S" "⋀T. T ∈ S ⟹ closedin U T"
    shows "closedin U (⋃S)"
  using assms by induction auto

lemma closedin_Inter[intro]:
  assumes Ke: "K ≠ {}"
    and Kc: "⋀S. S ∈K ⟹ closedin U S"
  shows "closedin U (⋂K)"
  using Ke Kc unfolding closedin_def Diff_Inter by auto

lemma closedin_INT[intro]:
  assumes "A ≠ {}" "⋀x. x ∈ A ⟹ closedin U (B x)"
  shows "closedin U (⋂x∈A. B x)"
  using assms by blast

lemma closedin_Int[intro]: "closedin U S ⟹ closedin U T ⟹ closedin U (S ∩ T)"
  using closedin_Inter[of "{S,T}" U] by auto

lemma openin_closedin_eq: "openin U S ⟷ S ⊆ topspace U ∧ closedin U (topspace U - S)"
  by (metis Diff_subset closedin_def double_diff equalityD1 openin_subset)

lemma topology_finer_closedin:
  "topspace X = topspace Y ⟹ (∀S. openin Y S ⟶ openin X S) ⟷ (∀S. closedin Y S ⟶ closedin X S)"
  by (metis closedin_def openin_closedin_eq)

lemma openin_closedin: "S ⊆ topspace U ⟹ (openin U S ⟷ 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)"
  by (metis Int_Diff cT closedin_def inf.orderE oS openin_Int openin_subset)

lemma closedin_diff[intro]:
  assumes oS: "closedin U S"
    and cT: "openin U T"
  shows "closedin U (S - T)"
  by (metis Int_Diff cT closedin_Int closedin_subset inf.orderE oS openin_closedin_eq)

lemma all_openin: "(∀U. openin X U ⟶ P U) ⟷ (∀U. closedin X U ⟶ P (topspace X - U))"
  by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)

lemma all_closedin: "(∀U. closedin X U ⟶ P U) ⟷ (∀U. openin X U ⟶ P (topspace X - U))"
  by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)

lemma ex_openin: "(∃U. openin X U ∧ P U) ⟷ (∃U. closedin X U ∧ P (topspace X - U))"
  by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)

lemma ex_closedin: "(∃U. closedin X U ∧ P U) ⟷ (∃U. openin X U ∧ P (topspace X - U))"
  by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)


subsection‹The discrete topology›

definition discrete_topology where "discrete_topology U ≡ topology (λS. S ⊆ U)"

lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S ⟷ S ⊆ U"
proof -
  have "istopology (λS. S ⊆ 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 ⟷ S ⊆ U"
  by (simp add: closedin_def)

lemma discrete_topology_unique:
   "discrete_topology U = X ⟷ topspace X = U ∧ (∀x ∈ U. openin X {x})" (is "?lhs = ?rhs")
proof
  assume R: ?rhs
  then have "openin X S" if "S ⊆ U" for S
    using openin_subopen subsetD that by fastforce
  then show ?lhs
    by (metis R openin_discrete_topology openin_subset topology_eq)
qed auto

lemma discrete_topology_unique_alt:
  "discrete_topology U = X ⟷ topspace X ⊆ U ∧ (∀x ∈ U. openin X {x})"
  using openin_subset
  by (auto simp: discrete_topology_unique)

lemma subtopology_eq_discrete_topology_empty:
   "X = discrete_topology {} ⟷ topspace X = {}"
  using discrete_topology_unique [of "{}" X] by auto

lemma subtopology_eq_discrete_topology_sing:
   "X = discrete_topology {a} ⟷ topspace X = {a}"
  by (metis discrete_topology_unique openin_topspace singletonD)

abbreviation trivial_topology where "trivial_topology ≡ discrete_topology {}"

lemma null_topspace_iff_trivial [simp]: "topspace X = {} ⟷ X = trivial_topology"
  by (simp add: subtopology_eq_discrete_topology_empty)

subsection ‹Subspace topology›

definition✐‹tag important› subtopology :: "'a topology ⇒ 'a set ⇒ 'a topology" 
  where "subtopology U V = topology (λT. ∃S. T = S ∩ V ∧ openin U S)"

lemma istopology_subtopology: "istopology (λT. ∃S. T = S ∩ V ∧ 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 ∩ V" and Sb: "openin U Sb" "B = Sb ∩ V"
      by blast
    have "A ∩ B = (Sa ∩ Sb) ∩ V" "openin U (Sa ∩ Sb)"
      using Sa Sb by blast+
    then have "?L (A ∩ B)" by blast
  }
  moreover
  {
    fix K
    assume K: "K ⊆ Collect ?L"
    have th0: "Collect ?L = (λS. S ∩ V) ` Collect (openin U)"
      by blast
    from K[unfolded th0 subset_image_iff]
    obtain Sk where Sk: "Sk ⊆ Collect (openin U)" "K = (λS. S ∩ V) ` Sk"
      by blast
    have "⋃K = (⋃Sk) ∩ V"
      using Sk by auto
    moreover have "openin U (⋃Sk)"
      using Sk by (auto simp: subset_eq)
    ultimately have "?L (⋃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 ⟷ (∃T. openin U T ∧ S = T ∩ V)"
  unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
  by auto

lemma subset_openin_subtopology:
   "⟦openin X S; S ⊆ T⟧ ⟹ openin (subtopology X T) S"
  by (metis inf.orderE openin_subtopology)

lemma openin_subtopology_Int:
   "openin X S ⟹ openin (subtopology X T) (S ∩ T)"
  using openin_subtopology by auto

lemma openin_subtopology_Int2:
   "openin X T ⟹ openin (subtopology X S) (S ∩ T)"
  using openin_subtopology by auto

lemma openin_subtopology_diff_closed:
   "⟦S ⊆ topspace X; closedin X T⟧ ⟹ 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 ∩ V"
  by (auto simp: topspace_def openin_subtopology)

lemma topspace_subtopology_subset:
   "S ⊆ topspace X ⟹ topspace(subtopology X S) = S"
  by (simp add: inf.absorb_iff2)

lemma closedin_subtopology: "closedin (subtopology U V) S ⟷ (∃T. closedin U T ∧ S = T ∩ V)"
  unfolding closedin_def topspace_subtopology
  by (auto simp: openin_subtopology)

lemma closedin_subtopology_Int_closed:
   "closedin X T ⟹ closedin (subtopology X S) (S ∩ T)"
  using closedin_subtopology inf_commute by blast

lemma closedin_subset_topspace:
   "⟦closedin X S; S ⊆ T⟧ ⟹ closedin (subtopology X T) S"
  using closedin_subtopology by fastforce

lemma closedin_relative_to:
   "(closedin X relative_to S) = closedin (subtopology X S)"
  by (force simp: relative_to_def closedin_subtopology)

lemma openin_subtopology_refl: "openin (subtopology U V) V ⟷ V ⊆ topspace U"
  unfolding openin_subtopology
  by auto (metis IntD1 in_mono openin_subset)

lemma subtopology_trivial_iff: "subtopology X S = trivial_topology ⟷ X = trivial_topology ∨ topspace X ∩ S = {}"
  by (auto simp flip: null_topspace_iff_trivial)

lemma subtopology_subtopology:
   "subtopology (subtopology X S) T = subtopology X (S ∩ T)"
proof -
  have eq: "⋀T'. (∃S'. T' = S' ∩ T ∧ (∃T. openin X T ∧ S' = T ∩ S)) = (∃Sa. T' = Sa ∩ (S ∩ T) ∧ openin X Sa)"
    by (metis inf_assoc)
  have "subtopology (subtopology X S) T = topology (λTa. ∃Sa. Ta = Sa ∩ T ∧ openin (subtopology X S) Sa)"
    by (simp add: subtopology_def)
  also have "… = subtopology X (S ∩ T)"
    by (simp add: openin_subtopology eq) (simp add: subtopology_def)
  finally show ?thesis .
qed

lemma openin_subtopology_alt:
     "openin (subtopology X U) S ⟷ S ∈ (λT. U ∩ T) ` Collect (openin X)"
  by (simp add: image_iff inf_commute openin_subtopology)

lemma closedin_subtopology_alt:
     "closedin (subtopology X U) S ⟷ S ∈ (λT. U ∩ T) ` Collect (closedin X)"
  by (simp add: image_iff inf_commute closedin_subtopology)

lemma subtopology_superset:
  assumes UV: "topspace U ⊆ V"
  shows "subtopology U V = U"
proof -
  { fix S
    have "openin U S" if "openin U T" "S = T ∩ V" for T
      by (metis Int_subset_iff assms inf.orderE openin_subset that)
    then have "(∃T. openin U T ∧ S = T ∩ V) ⟷ openin U S"
      by (metis assms inf.orderE inf_assoc openin_subset)
  }
  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_empty_iff_trivial [simp]: "subtopology X {} = trivial_topology"
  by (simp add: subtopology_eq_discrete_topology_empty)

lemma subtopology_restrict:
   "subtopology X (topspace X ∩ S) = subtopology X S"
  by (metis subtopology_subtopology subtopology_topspace)

lemma openin_subtopology_empty:
  "openin (subtopology U {}) S ⟷ S = {}"
  by (metis Int_empty_right openin_empty openin_subtopology)

lemma closedin_subtopology_empty:
  "closedin (subtopology U {}) S ⟷ S = {}"
  by (metis Int_empty_right closedin_empty closedin_subtopology)

lemma closedin_subtopology_refl [simp]:
  "closedin (subtopology U X) X ⟷ X ⊆ topspace U"
  by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)

lemma closedin_topspace_empty [simp]: "closedin trivial_topology S ⟷ S = {}"
  by (simp add: closedin_def)

lemma openin_topspace_empty [simp]:
   "openin trivial_topology S ⟷ S = {}"
  by (simp add: openin_closedin_eq)

lemma openin_imp_subset:
  "openin (subtopology U S) T ⟹ T ⊆ S"
  by (metis Int_iff openin_subtopology subsetI)

lemma closedin_imp_subset:
  "closedin (subtopology U S) T ⟹ T ⊆ S"
  by (simp add: closedin_def)

lemma openin_open_subtopology:
     "openin X S ⟹ openin (subtopology X S) T ⟷ openin X T ∧ T ⊆ S"
  by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)

lemma closedin_closed_subtopology:
     "closedin X S ⟹ (closedin (subtopology X S) T ⟷ closedin X T ∧ T ⊆ S)"
  by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)

lemma closedin_trans_full:
   "⟦closedin (subtopology X U) S; closedin X U⟧ ⟹ closedin X S"
  using closedin_closed_subtopology by blast

lemma openin_subtopology_Un:
    "⟦openin (subtopology X T) S; openin (subtopology X U) S⟧
     ⟹ openin (subtopology X (T ∪ U)) S"
by (simp add: openin_subtopology) blast

lemma closedin_subtopology_Un:
    "⟦closedin (subtopology X T) S; closedin (subtopology X U) S⟧
     ⟹ closedin (subtopology X (T ∪ U)) S"
by (simp add: closedin_subtopology) blast

lemma openin_trans_full:
   "⟦openin (subtopology X U) S; openin X U⟧ ⟹ openin X S"
  by (simp add: openin_open_subtopology)


subsection ‹The canonical topology from the underlying type class›

abbreviation✐‹tag important› euclidean :: "'a::topological_space topology"
  where "euclidean ≡ topology open"

abbreviation top_of_set :: "'a::topological_space set ⇒ 'a topology"
  where "top_of_set ≡ subtopology (topology open)"

lemma open_openin: "open S ⟷ openin euclidean S"
  by simp

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)

lemma closed_closedin: "closed S ⟷ 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)

lemma euclidean_nontrivial [simp]: "euclidean ≠ trivial_topology"
  by (simp add: subtopology_eq_discrete_topology_empty)


subsubsection‹The most basic facts about the usual topology and metric on R›

abbreviation euclideanreal :: "real topology"
  where "euclideanreal ≡ topology open"

subsection ‹Basic "localization" results are handy for connectedness.›

lemma openin_open: "openin (top_of_set U) S ⟷ (∃T. open T ∧ (S = U ∩ T))"
  by (auto simp: openin_subtopology)

lemma openin_Int_open:
   "⟦openin (top_of_set U) S; open T⟧
        ⟹ openin (top_of_set U) (S ∩ T)"
by (metis open_Int Int_assoc openin_open)

lemma openin_open_Int[intro]: "open S ⟹ openin (top_of_set U) (U ∩ S)"
  by (auto simp: openin_open)

lemma open_openin_trans[trans]:
  "open S ⟹ open T ⟹ T ⊆ S ⟹ openin (top_of_set S) T"
  by (metis Int_absorb1  openin_open_Int)

lemma open_subset: "S ⊆ T ⟹ open S ⟹ openin (top_of_set T) S"
  by (auto simp: openin_open)

lemma closedin_closed: "closedin (top_of_set U) S ⟷ (∃T. closed T ∧ S = U ∩ T)"
  by (simp add: closedin_subtopology Int_ac)

lemma closedin_closed_Int: "closed S ⟹ closedin (top_of_set U) (U ∩ S)"
  by (metis closedin_closed)

lemma closed_subset: "S ⊆ T ⟹ closed S ⟹ closedin (top_of_set T) S"
  by (auto simp: closedin_closed)

lemma closedin_closed_subset:
 "⟦closedin (top_of_set U) V; T ⊆ U; S = V ∩ T⟧
             ⟹ 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 "⟦finite S; S ⊆ T⟧ ⟹ 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} ⟷ a ∈ 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 ⟷
    S ⊆ U ∧ (∀x∈S. ∃e>0. ∀x'∈U. dist x' x < e ⟶ x'∈ S)"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding openin_open open_dist by blast
next
  define T where "T = {x. ∃a∈S. ∃d>0. (∀y∈U. dist y a < d ⟶ y ∈ S) ∧ dist x a < d}"
  have 1: "∀x∈T. ∃e>0. ∀y. dist y x < e ⟶ y ∈ T"
    unfolding T_def
    apply clarsimp
    apply (rule_tac x="d - dist x a" in exI)
    by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq)
  assume ?rhs then have 2: "S = U ∩ 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 ⟷
       ¬(∃E1 E2. openin (top_of_set S) E1 ∧
                 openin (top_of_set S) E2 ∧
                 S ⊆ E1 ∪ E2 ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})"
  unfolding connected_def openin_open disjoint_iff_not_equal by blast

lemma connected_openin_eq:
      "connected S ⟷
       ¬(∃E1 E2. openin (top_of_set S) E1 ∧
                 openin (top_of_set S) E2 ∧
                 E1 ∪ E2 = S ∧ E1 ∩ E2 = {} ∧
                 E1 ≠ {} ∧ E2 ≠ {})"
  unfolding connected_openin
  by (metis (no_types, lifting) Un_subset_iff openin_imp_subset subset_antisym)

lemma connected_closedin:
      "connected S ⟷
       (∄E1 E2.
        closedin (top_of_set S) E1 ∧
        closedin (top_of_set S) E2 ∧
        S ⊆ E1 ∪ E2 ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})"
       (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 ⊆ A ∪ B" "B ∩ S ≠ {}"
      and disj: "A ∩ B ∩ S = {}"
      and cl: "closed A" "closed B"
    have "S - A = B ∩ S"
      using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
    then show "A ∩ S = {}"
      by (metis Int_Diff_Un Int_Diff_disjoint R cl closedin_closed_Int dual_order.refl inf_commute s_sub(2))
  qed
qed

lemma connected_closedin_eq:
      "connected S ⟷
           ¬(∃E1 E2.
                 closedin (top_of_set S) E1 ∧
                 closedin (top_of_set S) E2 ∧
                 E1 ∪ E2 = S ∧ E1 ∩ E2 = {} ∧
                 E1 ≠ {} ∧ E2 ≠ {})"
  unfolding connected_closedin
  by (metis Un_subset_iff closedin_imp_subset subset_antisym)

text ‹These "transitivity" results are handy too›

lemma openin_trans[trans]:
  "openin (top_of_set T) S ⟹ openin (top_of_set U) T ⟹
    openin (top_of_set U) S"
  by (metis openin_Int_open openin_open)

lemma openin_open_trans: "openin (top_of_set T) S ⟹ open T ⟹ open S"
  by (auto simp: openin_open intro: openin_trans)

lemma closedin_trans[trans]:
  "closedin (top_of_set T) S ⟹ closedin (top_of_set U) T ⟹
    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 ⟹ closed T ⟹ closed S"
  by (auto simp: closedin_closed intro: closedin_trans)

lemma openin_subtopology_Int_subset:
   "⟦openin (top_of_set u) (u ∩ S); v ⊆ u⟧ ⟹ openin (top_of_set v) (v ∩ S)"
  by (auto simp: openin_subtopology)

lemma openin_open_eq: "open s ⟹ (openin (top_of_set s) t ⟷ open t ∧ t ⊆ s)"
  using open_subset openin_open_trans openin_subset by fastforce


subsection‹Derived set (set of limit points)›

definition derived_set_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixl ‹derived'_set'_of› 80)
  where "X derived_set_of S ≡
         {x ∈ topspace X.
                (∀T. x ∈ T ∧ openin X T ⟶ (∃y≠x. y ∈ S ∧ y ∈ T))}"

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

lemma in_derived_set_of:
   "x ∈ X derived_set_of S ⟷ x ∈ topspace X ∧ (∀T. x ∈ T ∧ openin X T ⟶ (∃y≠x. y ∈ S ∧ y ∈ T))"
  by (simp add: derived_set_of_def)

lemma derived_set_of_subset_topspace:
   "X derived_set_of S ⊆ topspace X"
  by (auto simp add: derived_set_of_def)

lemma derived_set_of_subtopology:
   "(subtopology X U) derived_set_of S = U ∩ (X derived_set_of (U ∩ S))"
  by (simp add: derived_set_of_def openin_subtopology) blast

lemma derived_set_of_subset_subtopology:
   "(subtopology X S) derived_set_of T ⊆ 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 ⊆ T ⟹ X derived_set_of S ⊆ X derived_set_of T"
  unfolding derived_set_of_def by blast

lemma derived_set_of_Un:
   "X derived_set_of (S ∪ T) = X derived_set_of S ∪ X derived_set_of T" (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    by (clarsimp simp: in_derived_set_of) (metis IntE IntI openin_Int)
  show "?rhs ⊆ ?lhs"
    by (simp add: derived_set_of_mono)
qed

lemma derived_set_of_Union:
   "finite ℱ ⟹ X derived_set_of (⋃ℱ) = (⋃S ∈ ℱ. X derived_set_of S)"
proof (induction ℱ rule: finite_induct)
  case (insert S ℱ)
  then show ?case
    by (simp add: derived_set_of_Un)
qed auto

lemma derived_set_of_topspace:
  "X derived_set_of (topspace X) = {x ∈ topspace X. ¬ openin X {x}}" (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    by (auto simp: in_derived_set_of)
  show "?rhs ⊆ ?lhs"
    by (clarsimp simp: in_derived_set_of) (metis openin_closedin_eq openin_subopen singletonD subset_eq)
qed

lemma discrete_topology_unique_derived_set:
     "discrete_topology U = X ⟷ topspace X = U ∧ 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 ⟷ U ⊆ topspace X ∧ U ∩ X derived_set_of U = {}"
  using discrete_topology_unique_derived_set [of U "subtopology X U"]
  by (auto simp: eq_commute derived_set_of_subtopology)

lemma subtopology_eq_discrete_topology:
   "S ⊆ topspace X ∧ S ∩ X derived_set_of S = {}
        ⟹ subtopology X S = discrete_topology S"
  by (simp add: subtopology_eq_discrete_topology_eq)

lemma subtopology_eq_discrete_topology_gen:
  assumes "S ∩ X derived_set_of S = {}"
  shows "subtopology X S = discrete_topology(topspace X ∩ S)"
proof -
  have "subtopology X S = subtopology X (topspace X ∩ S)"
    by (simp add: subtopology_restrict)
  then show ?thesis
    using assms by (simp add: inf.assoc subtopology_eq_discrete_topology_eq)
qed

lemma subtopology_discrete_topology [simp]: 
  "subtopology (discrete_topology U) S = discrete_topology(U ∩ S)"
proof -
  have "(λT. ∃Sa. T = Sa ∩ S ∧ Sa ⊆ U) = (λSa. Sa ⊆ U ∧ Sa ⊆ 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 ⟹ S ∩ X derived_set_of T ⊆ X derived_set_of (S ∩ T)"
  by (auto simp: derived_set_of_def)

lemma openin_Int_derived_set_of_eq:
  assumes "openin X S"
  shows "S ∩ X derived_set_of T = S ∩ X derived_set_of (S ∩ T)" (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    by (simp add: assms openin_Int_derived_set_of_subset)
  show "?rhs ⊆ ?lhs"
    by (metis derived_set_of_mono inf_commute inf_le1 inf_mono order_refl)
qed


subsection‹ Closure with respect to a topological space›

definition closure_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr ‹closure'_of› 80)
  where "X closure_of S ≡ {x ∈ topspace X. ∀T. x ∈ T ∧ openin X T ⟶ (∃y ∈ S. y ∈ T)}"

lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X ∩ S)"
  unfolding closure_of_def
  using openin_subset by blast

lemma in_closure_of:
   "x ∈ X closure_of S ⟷
    x ∈ topspace X ∧ (∀T. x ∈ T ∧ openin X T ⟶ (∃y. y ∈ S ∧ y ∈ T))"
  by (auto simp: closure_of_def)

lemma closure_of: "X closure_of S = topspace X ∩ (S ∪ 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 ∩ S ∪ 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 ⊆ 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 ∩ (X closure_of (U ∩ 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 ⊆ topspace X"
  by (simp add: closure_of)

lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T ⊆ S"
  by (simp add: closure_of_subtopology)

lemma closure_of_mono: "S ⊆ T ⟹ X closure_of S ⊆ X closure_of T"
  by (fastforce simp add: closure_of_def)

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

lemma closure_of_subtopology_mono:
   "T ⊆ U ⟹ (subtopology X T) closure_of S ⊆ (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 ∪ T) = X closure_of S ∪ 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 ℱ ⟹ X closure_of (⋃ℱ) = (⋃S ∈ ℱ. X closure_of S)"
by (induction ℱ rule: finite_induct) auto

lemma closure_of_subset: "S ⊆ topspace X ⟹ S ⊆ X closure_of S"
  by (auto simp: closure_of_def)

lemma closure_of_subset_Int: "topspace X ∩ S ⊆ X closure_of S"
  by (auto simp: closure_of_def)

lemma closure_of_subset_eq: "S ⊆ topspace X ∧ X closure_of S ⊆ S ⟷ closedin X S"
proof -
  have "openin X (topspace X - S)"
    if "⋀x. ⟦x ∈ topspace X; ∀T. x ∈ T ∧ openin X T ⟶ S ∩ T ≠ {}⟧ ⟹ x ∈ S"
    apply (subst openin_subopen)
    by (metis Diff_iff Diff_mono Diff_triv inf.commute openin_subset order_refl that)
  then show ?thesis
    by (auto simp: closedin_def closure_of_def disjoint_iff_not_equal)
qed

lemma closure_of_eq: "X closure_of S = S ⟷ closedin X S"
  by (metis closure_of_subset closure_of_subset_eq closure_of_subset_topspace subset_antisym)

lemma closedin_contains_derived_set:
   "closedin X S ⟷ X derived_set_of S ⊆ S ∧ S ⊆ topspace X"
proof (intro iffI conjI)
  show "closedin X S ⟹ X derived_set_of S ⊆ S"
    using closure_of_eq derived_set_of_subset_closure_of by fastforce
  show "closedin X S ⟹ S ⊆ topspace X"
    using closedin_subset by blast
  show "X derived_set_of S ⊆ S ∧ S ⊆ topspace X ⟹ 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 ⊆ S ⟷ closedin X (topspace X ∩ S)"
  by (simp add: closedin_contains_derived_set derived_set_of_subset_topspace)

lemma derived_set_subset: "S ⊆ topspace X ⟹ (X derived_set_of S ⊆ S ⟷ closedin X S)"
  by (simp add: closedin_contains_derived_set)

lemma closedin_derived_set:
     "closedin (subtopology X T) S ⟷
      S ⊆ topspace X ∧ S ⊆ T ∧ (∀x. x ∈ X derived_set_of S ∧ x ∈ T ⟶ x ∈ S)"
  by (auto simp: closedin_contains_derived_set derived_set_of_subtopology Int_absorb1)

lemma closedin_Int_closure_of:
     "closedin (subtopology X S) T ⟷ S ∩ X closure_of T = T"
  by (metis Int_left_absorb closure_of_eq closure_of_subtopology)

lemma closure_of_closedin: "closedin X S ⟹ X closure_of S = S"
  by (simp add: closure_of_eq)

lemma closure_of_eq_diff: "X closure_of S = topspace X - ⋃{T. openin X T ∧ 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 ⊆ topspace X" shows "X closure_of S = (closedin X) hull S"
  by (metis assms closedin_closure_of closure_of_eq closure_of_mono closure_of_subset hull_unique)

lemma closure_of_minimal:
   "⟦S ⊆ T; closedin X T⟧ ⟹ (X closure_of S) ⊆ T"
  by (metis closure_of_eq closure_of_mono)

lemma closure_of_minimal_eq:
   "⟦S ⊆ topspace X; closedin X T⟧ ⟹ (X closure_of S) ⊆ T ⟷ S ⊆ T"
  by (meson closure_of_minimal closure_of_subset subset_trans)

lemma closure_of_unique:
   "⟦S ⊆ T; closedin X T;
     ⋀T'. ⟦S ⊆ T'; closedin X T'⟧ ⟹ T ⊆ T'⟧
    ⟹ 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 = {} ⟷ disjnt (topspace X) S"
  unfolding disjnt_def closure_of_restrict [where S=S]
  using closure_of by fastforce

lemma closure_of_eq_empty: "S ⊆ topspace X ⟹ X closure_of S = {} ⟷ S = {}"
  using closure_of_subset by fastforce

lemma openin_Int_closure_of_subset:
  assumes "openin X S"
  shows "S ∩ X closure_of T ⊆ X closure_of (S ∩ T)"
proof -
  have "S ∩ X derived_set_of T = S ∩ X derived_set_of (S ∩ T)"
    by (meson assms openin_Int_derived_set_of_eq)
  moreover have "S ∩ (S ∩ T) = S ∩ 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 ∩ X closure_of T) = X closure_of (S ∩ T)"
proof
  show "X closure_of (S ∩ X closure_of T) ⊆ X closure_of (S ∩ T)"
    by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
next
  show "X closure_of (S ∩ T) ⊆ X closure_of (S ∩ X closure_of T)"
    by (metis Int_subset_iff assms closure_of_alt closure_of_mono inf_mono openin_subset subset_refl sup.coboundedI1)
qed

lemma openin_Int_closure_of_eq:
  assumes "openin X S" shows "S ∩ X closure_of T = S ∩ X closure_of (S ∩ T)"  (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    by (simp add: assms openin_Int_closure_of_subset)
  show "?rhs ⊆ ?lhs"
    by (metis closure_of_mono inf_commute inf_le1 inf_mono order_refl)
qed

lemma openin_Int_closure_of_eq_empty:
  assumes "openin X S" shows "S ∩ X closure_of T = {} ⟷ S ∩ T = {}"  (is "?lhs = ?rhs")
proof
  show "?lhs ⟹ ?rhs"
    unfolding disjoint_iff
    by (meson assms in_closure_of in_mono openin_subset)
  show "?rhs ⟹ ?lhs"
    by (simp add: assms openin_Int_closure_of_eq)
qed

lemma closure_of_openin_Int_superset:
   "openin X S ∧ S ⊆ X closure_of T
        ⟹ X closure_of (S ∩ 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 ⊆ U"
  shows "X closure_of (S ∩ X closure_of T) = X closure_of (S ∩ T)" (is "?lhs = ?rhs")
proof
  obtain S0 where S0: "openin X S0" "S = S0 ∩ U"
    using assms by (auto simp: openin_subtopology)
  then show "?lhs ⊆ ?rhs"
  proof -
    have "S0 ∩ X closure_of T = S0 ∩ X closure_of (S0 ∩ T)"
      by (meson S0(1) openin_Int_closure_of_eq)
    moreover have "S0 ∩ T = S0 ∩ U ∩ T"
      using ‹T ⊆ U› by fastforce
    ultimately have "S ∩ X closure_of T ⊆ X closure_of (S ∩ T)"
      using S0(2) by auto
    then show ?thesis
      by (meson closedin_closure_of closure_of_minimal)
  qed
next
  show "?rhs ⊆ ?lhs"
  proof -
    have "T ∩ S ⊆ T ∪ X derived_set_of T"
      by force
    then show ?thesis
      by (smt (verit, del_insts) Int_iff in_closure_of inf.orderE openin_subset subsetI)
  qed
qed

lemma closure_of_subtopology_open:
     "openin X U ∨ S ⊆ U ⟹ (subtopology X U) closure_of S = U ∩ 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 ∩ S"
  by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)


text‹ Interior with respect to a topological space.                             ›

definition interior_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr ‹interior'_of› 80)
  where "X interior_of S ≡ {x. ∃T. openin X T ∧ x ∈ T ∧ T ⊆ S}"

lemma interior_of_restrict:
   "X interior_of S = X interior_of (topspace X ∩ S)"
  using openin_subset by (auto simp: interior_of_def)

lemma interior_of_eq: "(X interior_of S = S) ⟷ openin X S"
  unfolding interior_of_def  using openin_subopen by blast

lemma interior_of_openin: "openin X S ⟹ 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 ⊆ S"
  by (auto simp: interior_of_def)

lemma interior_of_subset_closure_of: "X interior_of S ⊆ 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 ⊆ X interior_of S ⟷ openin X S"
  by (metis interior_of_eq interior_of_subset subset_antisym)

lemma interior_of_mono: "S ⊆ T ⟹ X interior_of S ⊆ X interior_of T"
  by (auto simp: interior_of_def)

lemma interior_of_maximal: "⟦T ⊆ S; openin X T⟧ ⟹ T ⊆ X interior_of S"
  by (auto simp: interior_of_def)

lemma interior_of_maximal_eq: "openin X T ⟹ T ⊆ X interior_of S ⟷ T ⊆ S"
  by (meson interior_of_maximal interior_of_subset order_trans)

lemma interior_of_unique:
   "⟦T ⊆ S; openin X T; ⋀T'. ⟦T' ⊆ S; openin X T'⟧ ⟹ T' ⊆ T⟧ ⟹ 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 ⊆ topspace X"
  by (simp add: openin_subset)

lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T ⊆ S"
  by (meson openin_imp_subset openin_interior_of)

lemma interior_of_Int: "X interior_of (S ∩ T) = X interior_of S ∩ X interior_of T"  (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    by (simp add: interior_of_mono)
  show "?rhs ⊆ ?lhs"
    by (meson inf_mono interior_of_maximal interior_of_subset openin_Int openin_interior_of)
qed

lemma interior_of_Inter_subset: "X interior_of (⋂ℱ) ⊆ (⋂S ∈ ℱ. X interior_of S)"
  by (simp add: INT_greatest Inf_lower interior_of_mono)

lemma union_interior_of_subset:
   "X interior_of S ∪ X interior_of T ⊆ X interior_of (S ∪ T)"
  by (simp add: interior_of_mono)

lemma interior_of_eq_empty:
   "X interior_of S = {} ⟷ (∀T. openin X T ∧ T ⊆ S ⟶ 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 = {} ⟷ (∀T. openin X T ∧ T ≠ {} ⟶ T - S ≠ {})"
  by (auto simp: interior_of_eq_empty)

lemma interior_of_Union_openin_subsets:
   "⋃{T. openin X T ∧ T ⊆ 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 = {} ⟷ 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 ⟷ 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 ∩ X interior_of S ⊆ (subtopology X U) interior_of S"
  by (auto simp: interior_of_def openin_subtopology)

lemma interior_of_subtopology_subsets:
   "T ⊆ U ⟹ T ∩ (subtopology X U) interior_of S ⊆ (subtopology X T) interior_of S"
  by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)

lemma interior_of_subtopology_mono:
   "⟦S ⊆ T; T ⊆ U⟧ ⟹ (subtopology X U) interior_of S ⊆ (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 ∩ X interior_of S" (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    by (meson assms interior_of_maximal interior_of_subset le_infI openin_interior_of openin_open_subtopology)
  show "?rhs ⊆ ?lhs"
    by (simp add: interior_of_subtopology_subset)
qed

lemma dense_intersects_open:
   "X closure_of S = topspace X ⟷ (∀T. openin X T ∧ T ≠ {} ⟶ S ∩ T ≠ {})"
proof -
  have "X closure_of S = topspace X ⟷ (topspace X - X interior_of (topspace X - S) = topspace X)"
    by (simp add: closure_of_interior_of)
  also have "… ⟷ X interior_of (topspace X - S) = {}"
    by (simp add: closure_of_complement interior_of_eq_empty_complement)
  also have "… ⟷ (∀T. openin X T ∧ T ≠ {} ⟶ S ∩ T ≠ {})"
    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 ∪ 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
        ⟹ (X interior_of (S ∪ T) = {} ⟷
             X interior_of S = {} ∧ 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 ∩ S"
  by (simp add: interior_of_restrict [of _ S] interior_of_eq)


subsection ‹Frontier with respect to topological space ›

definition frontier_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr ‹frontier'_of› 80)
  where "X frontier_of S ≡ X closure_of S - X interior_of S"

lemma frontier_of_closures:
     "X frontier_of S = X closure_of S ∩ 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 ∪ 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 ∩ 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 ⊆ topspace X"
  by (simp add: closedin_frontier_of closedin_subset)

lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T ⊆ S"
  by (metis (no_types) closedin_derived_set closedin_frontier_of)

lemma frontier_of_subtopology_subset:
  "U ∩ (subtopology X U) frontier_of S ⊆ (X frontier_of S)"
proof -
  have "U ∩ X interior_of S - subtopology X U interior_of S = {}"
    by (simp add: interior_of_subtopology_subset)
  moreover have "X closure_of S ∩ 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:
   "⟦S ⊆ T; T ⊆ U⟧ ⟹ (subtopology X T) frontier_of S ⊆ (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 ∧ openin X S ⟷ S ⊆ topspace X ∧ X frontier_of S = {}"
proof (cases "S ⊆ 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 ⊆ topspace X ⟹ (X frontier_of S = {} ⟷ closedin X S ∧ openin X S)"
  by (simp add: clopenin_eq_frontier_of)

lemma frontier_of_openin:
     "openin X S ⟹ 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 ∩ X frontier_of S ≠ {}"
  shows "U ∩ S ≠ {}" "U - S ≠ {}"
proof -
  have "U ∩ (X closure_of S ∩ X closure_of (topspace X - S)) ≠ {}"
    using assms by (simp add: frontier_of_closures)
  then show "U ∩ S ≠ {}"
    using assms openin_Int_closure_of_eq_empty by fastforce
  show "U - S ≠ {}"
  proof -
    have "∃A. X closure_of (A - S) ∩ U ≠ {}"
      using ‹U ∩ (X closure_of S ∩ X closure_of (topspace X - S)) ≠ {}› by blast
    then have "¬ U ⊆ 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 ⟹ (X frontier_of S) ⊆ 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 ⊆ topspace X"
  shows "(X frontier_of S) ⊆ S ⟷ closedin X S"
proof
  show "X frontier_of S ⊆ S ⟹ 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 ⟹ X frontier_of S ⊆ 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 ⊆ topspace X"
  shows "((X frontier_of S) ∩ S = {} ⟷ openin X S)"
proof
  assume "X frontier_of S ∩ 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 ⟹ X frontier_of S ∩ 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 ⊆ (topspace X - X frontier_of S) ⟷ openin X S"
proof (cases "S ⊆ 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 ∩ T) =
      X closure_of (S ∩ T) ∩ (X frontier_of S ∪ X frontier_of T)"
proof -
  have *: "U ⊆ S ∧ U ⊆ T ⟹ U ∩ (S ∩ A ∪ T ∩ B) = U ∩ (A ∪ 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 ∩ T) ⊆ X frontier_of S ∪ X frontier_of T"
  by (simp add: frontier_of_Int)

lemma frontier_of_Int_closedin:
  assumes "closedin X S" "closedin X T" 
  shows "X frontier_of(S ∩ T) = X frontier_of S ∩ T ∪ S ∩ X frontier_of T"  (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    using assms by (force simp add: frontier_of_Int closedin_Int closure_of_closedin)
  show "?rhs ⊆ ?lhs"
    using assms frontier_of_subset_closedin
    by (auto simp add: frontier_of_Int closedin_Int closure_of_closedin)
qed

lemma frontier_of_Un_subset: "X frontier_of(S ∪ T) ⊆ X frontier_of S ∪ X frontier_of T"
  by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)

lemma frontier_of_Union_subset:
   "finite ℱ ⟹ X frontier_of (⋃ℱ) ⊆ (⋃T ∈ ℱ. X frontier_of T)"
proof (induction ℱ rule: finite_induct)
  case (insert A ℱ)
  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) ⊆ X frontier_of S"
  by (simp add: closedin_frontier_of frontier_of_subset_closedin)

lemma frontier_of_subtopology_open:
     "openin X U ⟹ (subtopology X U) frontier_of S = U ∩ 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)

lemma openin_subset_topspace_eq:
  assumes "disjnt S (X frontier_of U)"
  shows "openin (subtopology X U) S ⟷ openin X S ∧ S ⊆ U"
proof
  assume S: "openin (subtopology X U) S"
  show "openin X S ∧ S ⊆ U"
  proof
    show "S ⊆ U"
      using S openin_imp_subset by blast
    have "disjnt S (X frontier_of (topspace X ∩ U))"
      by (metis assms frontier_of_restrict)
    moreover
    have "openin (subtopology X (topspace X ∩ U)) S"
      by (simp add: S subtopology_restrict)
    moreover
    have "openin X S" 
      if dis: "disjnt S (X frontier_of U)" and ope: "openin (subtopology X U) S" and "U ⊆ topspace X" 
      for S U
    proof -
      obtain T where T: "openin X T" "S = T ∩ U"
        using ope by (auto simp: openin_subtopology)
      have "T ∩ U = T ∩ X interior_of U"
        using that T interior_of_subset in_closure_of by (fastforce simp: disjnt_iff frontier_of_def)
      then show ?thesis
        using ‹S = T ∩ U› ‹openin X T› by auto
    qed
  ultimately show "openin X S"
      by blast
  qed 
qed (metis inf.absorb_iff1 openin_subtopology_Int)


subsection‹Locally finite collections›

definition locally_finite_in
  where
 "locally_finite_in X 𝒜 ⟷
        (⋃𝒜 ⊆ topspace X) ∧
        (∀x ∈ topspace X. ∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ 𝒜. U ∩ V ≠ {}})"

lemma finite_imp_locally_finite_in:
   "⟦finite 𝒜; ⋃𝒜 ⊆ topspace X⟧ ⟹ locally_finite_in X 𝒜"
  by (auto simp: locally_finite_in_def)

lemma locally_finite_in_subset:
  assumes "locally_finite_in X 𝒜" "ℬ ⊆ 𝒜"
  shows "locally_finite_in X ℬ"
proof -
  have "finite (𝒜 ∩ {U. U ∩ V ≠ {}}) ⟹ finite (ℬ ∩ {U. U ∩ V ≠ {}})" for V
    by (meson ‹ℬ ⊆ 𝒜› finite_subset inf_le1 inf_le2 le_inf_iff subset_trans)
  then show ?thesis
    using assms unfolding locally_finite_in_def Int_def by fastforce
qed

lemma locally_finite_in_refinement:
  assumes 𝒜: "locally_finite_in X 𝒜" and f: "⋀S. S ∈ 𝒜 ⟹ f S ⊆ S"
  shows "locally_finite_in X (f ` 𝒜)"
proof -
  show ?thesis
    unfolding locally_finite_in_def
  proof safe
    fix x
    assume "x ∈ topspace X"
    then obtain V where "openin X V" "x ∈ V" "finite {U ∈ 𝒜. U ∩ V ≠ {}}"
      using 𝒜 unfolding locally_finite_in_def by blast
    moreover have "{U ∈ 𝒜. f U ∩ V ≠ {}} ⊆ {U ∈ 𝒜. U ∩ V ≠ {}}" for V
      using f by blast
    ultimately have "finite {U ∈ 𝒜. f U ∩ V ≠ {}}"
      using finite_subset by blast
    moreover have "f ` {U ∈ 𝒜. f U ∩ V ≠ {}} = {U ∈ f ` 𝒜. U ∩ V ≠ {}}"
      by blast
    ultimately have "finite {U ∈ f ` 𝒜. U ∩ V ≠ {}}"
      by (metis (no_types, lifting) finite_imageI)
    then show "∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ f ` 𝒜. U ∩ V ≠ {}}"
      using ‹openin X V› ‹x ∈ V› by blast
  next
    show "⋀x xa. ⟦xa ∈ 𝒜; x ∈ f xa⟧ ⟹ x ∈ topspace X"
      by (meson Sup_upper 𝒜 f locally_finite_in_def subset_iff)
  qed
qed

lemma locally_finite_in_subtopology:
  assumes 𝒜: "locally_finite_in X 𝒜" "⋃𝒜 ⊆ S"
  shows "locally_finite_in (subtopology X S) 𝒜"
  unfolding locally_finite_in_def
proof safe
  fix x
  assume x: "x ∈ topspace (subtopology X S)"
  then obtain V where "openin X V" "x ∈ V" and fin: "finite {U ∈ 𝒜. U ∩ V ≠ {}}"
    using 𝒜 unfolding locally_finite_in_def topspace_subtopology by blast
  show "∃V. openin (subtopology X S) V ∧ x ∈ V ∧ finite {U ∈ 𝒜. U ∩ V ≠ {}}"
  proof (intro exI conjI)
    show "openin (subtopology X S) (S ∩ V)"
      by (simp add: ‹openin X V› openin_subtopology_Int2)
    have "{U ∈ 𝒜. U ∩ (S ∩ V) ≠ {}} ⊆ {U ∈ 𝒜. U ∩ V ≠ {}}"
      by auto
    with fin show "finite {U ∈ 𝒜. U ∩ (S ∩ V) ≠ {}}"
      using finite_subset by auto
    show "x ∈ S ∩ V"
      using x ‹x ∈ V› by (simp)
  qed
next
  show "⋀x A. ⟦x ∈ A; A ∈ 𝒜⟧ ⟹ x ∈ topspace (subtopology X S)"
    using assms unfolding locally_finite_in_def topspace_subtopology by blast
qed


lemma closedin_locally_finite_Union:
  assumes clo: "⋀S. S ∈ 𝒜 ⟹ closedin X S" and 𝒜: "locally_finite_in X 𝒜"
  shows "closedin X (⋃𝒜)"
  using 𝒜 unfolding locally_finite_in_def closedin_def
proof clarify
  show "openin X (topspace X - ⋃𝒜)"
  proof (subst openin_subopen, clarify)
    fix x
    assume "x ∈ topspace X" and "x ∉ ⋃𝒜"
    then obtain V where "openin X V" "x ∈ V" and fin: "finite {U ∈ 𝒜. U ∩ V ≠ {}}"
      using 𝒜 unfolding locally_finite_in_def by blast
    let ?T = "V - ⋃{S ∈ 𝒜. S ∩ V ≠ {}}"
    show "∃T. openin X T ∧ x ∈ T ∧ T ⊆ topspace X - ⋃𝒜"
    proof (intro exI conjI)
      show "openin X ?T"
        by (metis (no_types, lifting) fin ‹openin X V› clo closedin_Union mem_Collect_eq openin_diff)
      show "x ∈ ?T"
        using ‹x ∉ ⋃𝒜› ‹x ∈ V› by auto
      show "?T ⊆ topspace X - ⋃𝒜"
        using ‹openin X V› openin_subset by auto
    qed
  qed
qed

lemma locally_finite_in_closure:
  assumes 𝒜: "locally_finite_in X 𝒜"
  shows "locally_finite_in X ((λS. X closure_of S) ` 𝒜)"
  using 𝒜 unfolding locally_finite_in_def
proof (intro conjI; clarsimp)
  fix x A
  assume "x ∈ X closure_of A"
  then show "x ∈ topspace X"
    by (meson in_closure_of)
next
  fix x
  assume "x ∈ topspace X" and "⋃𝒜 ⊆ topspace X"
  then obtain V where V: "openin X V" "x ∈ V" and fin: "finite {U ∈ 𝒜. U ∩ V ≠ {}}"
    using 𝒜 unfolding locally_finite_in_def by blast
  have eq: "{y ∈ f ` 𝒜. Q y} = f ` {x. x ∈ 𝒜 ∧ Q(f x)}" for f and Q :: "'a set ⇒ bool"
    by blast
  have eq2: "{A ∈ 𝒜. X closure_of A ∩ V ≠ {}} = {A ∈ 𝒜. A ∩ V ≠ {}}"
    using openin_Int_closure_of_eq_empty V  by blast
  have "finite {U ∈ (closure_of) X ` 𝒜. U ∩ V ≠ {}}"
    by (simp add: eq eq2 fin)
  with V show "∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ (closure_of) X ` 𝒜. U ∩ V ≠ {}}"
    by blast
qed

lemma closedin_Union_locally_finite_closure:
   "locally_finite_in X 𝒜 ⟹ closedin X (⋃((λS. X closure_of S) ` 𝒜))"
  by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)

lemma closure_of_Union_subset: "⋃((λS. X closure_of S) ` 𝒜) ⊆ X closure_of (⋃𝒜)"
  by (simp add: SUP_le_iff Sup_upper closure_of_mono)

lemma closure_of_locally_finite_Union:
  assumes "locally_finite_in X 𝒜" 
  shows "X closure_of (⋃𝒜) = ⋃((λS. X closure_of S) ` 𝒜)"  
proof (rule closure_of_unique)
  show "⋃ 𝒜 ⊆ ⋃ ((closure_of) X ` 𝒜)"
    using assms by (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
  show "closedin X (⋃ ((closure_of) X ` 𝒜))"
    using assms by (simp add: closedin_Union_locally_finite_closure)
  show "⋀T'. ⟦⋃ 𝒜 ⊆ T'; closedin X T'⟧ ⟹ ⋃ ((closure_of) X ` 𝒜) ⊆ T'"
    by (simp add: Sup_le_iff closure_of_minimal)
qed


subsection✐‹tag important› ‹Continuous maps›

text ‹We will need to deal with continuous maps in terms of topologies and not in terms
of type classes, as defined below.›

definition continuous_map where
  "continuous_map X Y f ≡
     f ∈ topspace X → topspace Y ∧
     (∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U})"

lemma continuous_map:
   "continuous_map X Y f ⟷
        f ` (topspace X) ⊆ topspace Y ∧ (∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U})"
  by (auto simp: continuous_map_def)

lemma continuous_map_image_subset_topspace:
   "continuous_map X Y f ⟹ f ` (topspace X) ⊆ topspace Y"
  by (auto simp: continuous_map_def)

lemma continuous_map_funspace:
   "continuous_map X Y f ⟹ f ∈ topspace X → topspace Y"
  by (auto simp: continuous_map_def)

lemma continuous_map_on_empty [simp]: "continuous_map trivial_topology Y f"
  by (auto simp: continuous_map_def)

lemma continuous_map_on_empty2 [simp]: "continuous_map X trivial_topology f ⟷ X = trivial_topology"
  using continuous_map_image_subset_topspace by fastforce

lemma continuous_map_closedin:
   "continuous_map X Y f ⟷
         f ∈ topspace X → topspace Y ∧
         (∀C. closedin Y C ⟶ closedin X {x ∈ topspace X. f x ∈ C})"
proof -
  have "(∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U}) =
        (∀C. closedin Y C ⟶ closedin X {x ∈ topspace X. f x ∈ C})"
    if "f ∈ topspace X → topspace Y"
  proof -
    have eq: "{x ∈ topspace X. f x ∈ topspace Y ∧ f x ∉ C} = (topspace X - {x ∈ topspace X. f x ∈ C})" for C
      using that by blast
    show ?thesis
    proof (intro iffI allI impI)
      fix C
      assume "∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U}" and "closedin Y C"
      then show "closedin X {x ∈ topspace X. f x ∈ C}"
        by (auto simp add: closedin_def eq)
    next
      fix U
      assume "∀C. closedin Y C ⟶ closedin X {x ∈ topspace X. f x ∈ C}" and "openin Y U"
      then show "openin X {x ∈ topspace X. f x ∈ 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:
   "⟦continuous_map X Y f; openin Y U⟧ ⟹ openin X {x ∈ topspace X. f x ∈ U}"
  by (simp add: continuous_map_def)

lemma closedin_continuous_map_preimage:
   "⟦continuous_map X Y f; closedin Y C⟧ ⟹ closedin X {x ∈ topspace X. f x ∈ 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 ∈ U. f x ∈ V}"
proof -
  have eq: "{x ∈ U. f x ∈ V} = U ∩ {x ∈ topspace X. f x ∈ 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 ∈ U. f x ∈ V}"
proof -
  have eq: "{x ∈ U. f x ∈ V} = U ∩ {x ∈ topspace X. f x ∈ 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) ⊆ Y closure_of f ` S"
proof -
  have *: "f ` (topspace X) ⊆ topspace Y"
    by (meson assms continuous_map)
  have "X closure_of T ⊆ {x ∈ X closure_of T. f x ∈ Y closure_of (f ` T)}"
    if "T ⊆ topspace X" for T
  proof (rule closure_of_minimal)
    show "T ⊆ {x ∈ X closure_of T. f x ∈ Y closure_of f ` T}"
      using closure_of_subset * that  by (fastforce simp: in_closure_of)
  next
    show "closedin X {x ∈ X closure_of T. f x ∈ Y closure_of f ` T}"
      using assms closedin_continuous_map_preimage_gen by fastforce
  qed
  then show ?thesis
    by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq)
qed

lemma continuous_map_subset_aux1: "continuous_map X Y f ⟹
       (∀S. f ` (X closure_of S) ⊆ Y closure_of f ` S)"
  using continuous_map_image_closure_subset by blast

lemma continuous_map_subset_aux2:
  assumes "∀S. S ⊆ topspace X ⟶ f ` (X<