Quelle  Abstract_Topology.thy   Sprache: Isabelle

(*  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 "\S T Sa Sb. \openin U Sa; openin U Sb\ \ \S. Sa \ V \ (Sb \ V) = S \ V \ openin U S"
    by (metis Int_assoc inf.absorb2 inf_sup_ord(2) openin_Int)
  moreover 
  have "\S. \ \ = S \ V \ openin U S"
    if K: "\K\\. \S. K = S \ V \ openin U S" for K
  proof -
    obtain f where f: "\K\\. K = f K \ V \ openin U (f K)"
      using K by metis
    with f show ?thesis
      by blast
  qed
  ultimately show ?thesis
 unfolding istopology_def by force
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"
  unfolding topology_eq openin_subtopology
proof (intro strip)
  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 show "(\T. openin U T \ S = T \ V) \ openin U S"
    by (metis assms inf.orderE inf_assoc openin_subset)
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
    subgoal for x a d
      apply (rule_tac x="d - dist x a" in exI)
      by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq)
    done
  assume ?rhs then have 2: "S = U \ T"
    unfolding T_def by fastforce
  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 F rule: finite_induct)
  case (insert S F)
  then show ?case
    by (simp add: derived_set_of_Un)
qed auto

lemma derived_set_of_topspace:
  "X derived_set_of (topspace X) = {x \ 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 F 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 F rule: finite_induct)
  case (insert A F)
  then show ?case
    using frontier_of_Un_subset by fastforce
qed simp

lemma frontier_of_frontier_of_subset:
     "X frontier_of (X frontier_of S) \ 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 \ \
        (∪A ⊆ topspace X) ∧
        (∀x ∈ topspace X. ∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ A. 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 ‹B ⊆ A› 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 A: "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 (intro conjI strip)
    fix x
    assume "x \ topspace X"
    then obtain V where "openin X V" "x \ V" "finite {U \ \. U \ V \ {}}"
      using A 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 "\ (f ` \) \ topspace X"
      using A f by (force simp: locally_finite_in_def image_iff)
  qed
qed

lemma locally_finite_in_subtopology:
  assumes A: "locally_finite_in X \" "\\ \ S"
  shows "locally_finite_in (subtopology X S) \"
  unfolding locally_finite_in_def
proof (intro conjI strip)
  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 A 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 "\ \ \ 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 A: "locally_finite_in X \"
  shows "closedin X (\\)"
  using A 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 A 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 ∉ ∪A› ‹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 A: "locally_finite_in X \"
  shows "locally_finite_in X ((\S. X closure_of S) ` \)"
  using A 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 A 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 -
--> --------------------

--> maximum size reached

--> --------------------