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›

definitiontag important› istopology :: "('a set  bool)  bool" where
  "istopology L  (S T. L S  L T  L (S  T))  (𝒦. (K𝒦. L K)  L (𝒦))"

typedeftag 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 (ST)"
    "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›

definitiontag 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. sS}"
  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 (xA. 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›

definitiontag 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›

abbreviationtag 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  (xS. 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. aS. d>0. (yU. dist y a < d  y  S)  dist x a < d}"
  have 1: "xT. 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  (yx. 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  (yx. 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


subsectiontag 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 closure_of S)  Y closure_of f ` S"
  shows "continuous_map X Y f"
  unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
  show "f  topspace X  topspace Y"
    using assms closure_of_subset_topspace by fastforce
next
  fix C
  assume "closedin Y C"
  then show "closedin X {x  topspace X. f x  C}"
  proof (clarsimp simp flip: closure_of_subset_eq, <