Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Abstract_Topology.thy Sprache: Isabelle

Original von: Isabelle^©

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

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

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

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

definition\<^marker>\<open>tag important\<close> istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
  "istopology L \ (\S T. L S \ L T \ L (S \ T)) \ (\\. (\K\\. L K) \ L (\\))"

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

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

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

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

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

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\<open>The "universe": the union of all sets in the topology.\<close>
definition "topspace T = \{S. openin T S}"

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

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 \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
  then show ?thesis
    using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
qed

lemma openin_Inter [intro]:
  assumes "finite \" "\ \ {}" "\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 \<open>Closed sets\<close>

definition\<^marker>\<open>tag important\<close> closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 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)"
proof -
  have "S - T = S \ (topspace U - T)" using openin_subset[of U S] oS cT
    by (auto simp: topspace_def openin_subset)
  then show ?thesis using oS cT
    by (auto simp: closedin_def)
qed

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

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

definition discrete_topology where "discrete_topology U \ 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
  moreover have "x \ topspace X" if "openin X S" and "x \ S" for x S
    using openin_subset that by blast
  ultimately
  show ?lhs
    using R by (auto simp: topology_eq)
qed auto

lemma discrete_topology_unique_alt:
  "discrete_topology U = X \ 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)

subsection \<open>Subspace topology\<close>

definition\<^marker>\<open>tag important\<close> subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> '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 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 openin_subtopology_refl: "openin (subtopology U V) V \ V \ topspace U"
  unfolding openin_subtopology
  by auto (metis IntD1 in_mono openin_subset)

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
    {
      fix T
      assume T: "openin U T" "S = T \ V"
      from T openin_subset[OF T(1)] UV have eq: "S = T"
        by blast
      have "openin U S"
        unfolding eq using T by blast
    }
    moreover
    {
      assume S: "openin U S"
      then have "\T. openin U T \ S = T \ V"
        using openin_subset[OF S] UV by auto
    }
    ultimately have "(\T. openin U T \ S = T \ V) \ openin U S"
      by blast
  }
  then show ?thesis
    unfolding topology_eq openin_subtopology by blast
qed

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

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

lemma subtopology_restrict:
   "subtopology X (topspace X \ 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: "topspace T = {} \ (closedin T S \ S = {})"
  by (simp add: closedin_def)

lemma open_in_topspace_empty:
   "topspace X = {} \ openin X 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 openin_subtopology_Un:
    "\openin (subtopology X T) S; openin (subtopology X U) S\
     \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
by (simp add: openin_subtopology) blast

lemma closedin_subtopology_Un:
    "\closedin (subtopology X T) S; closedin (subtopology X U) S\
     \<Longrightarrow> closedin (subtopology X (T \<union> 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 \<open>The canonical topology from the underlying type class\<close>

abbreviation\<^marker>\<open>tag important\<close> 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 add: istopology_open topology_inverse')

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)

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

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

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

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\
        \<Longrightarrow> openin (top_of_set U) (S \<inter> 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\
             \<Longrightarrow> closedin (top_of_set T) S"
  by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)

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

lemma connected_openin:
      "connected S \
       \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
                 openin (top_of_set S) E2 \<and>
                 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
  unfolding connected_def openin_open disjoint_iff_not_equal by blast

lemma connected_openin_eq:
      "connected S \
       \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
                 openin (top_of_set S) E2 \<and>
                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
  unfolding connected_openin
  by (metis (no_types, lifting) Un_subset_iff openin_imp_subset subset_antisym)

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

lemma connected_closedin_eq:
      "connected S \
           \<not>(\<exists>E1 E2.
                 closedin (top_of_set S) E1 \<and>
                 closedin (top_of_set S) E2 \<and>
                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
  unfolding connected_closedin
  by (metis Un_subset_iff closedin_imp_subset subset_antisym)

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

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\<open>Derived set (set of limit points)\<close>

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

lemma derived_set_of_restrict [simp]:
   "X derived_set_of (topspace X \ 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 = {}
        \<Longrightarrow> subtopology X S = discrete_topology S"
  by (simp add: subtopology_eq_discrete_topology_eq)

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

lemma subtopology_discrete_topology [simp]:
  "subtopology (discrete_topology U) S = discrete_topology(U \ 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\<open> Closure with respect to a topological space\<close>

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 \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
  by (auto simp: closure_of_def)

lemma closure_of: "X closure_of S = topspace X \ (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"
proof (cases "S \ topspace X")
  case True
  then show ?thesis
    by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
next
  case False
  then show ?thesis
    using closure_of closure_of_subset_eq by fastforce
qed

lemma closedin_contains_derived_set:
   "closedin X S \ 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_restrict 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 \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> S)"
  by (auto simp: closedin_contains_derived_set 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"
proof (rule hull_unique [THEN sym])
  show "S \ X closure_of S"
    by (simp add: closure_of_subset assms)
next
  show "closedin X (X closure_of S)"
    by simp
  show "\T. \S \ T; closedin X T\ \ X closure_of S \ T"
    by (metis closure_of_eq closure_of_mono)
qed

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;
     \<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
    \<Longrightarrow> X closure_of S = T"
  by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)

lemma closure_of_eq_empty_gen: "X closure_of S = {} \ 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_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
qed

lemma openin_Int_closure_of_eq:
  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
        \<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
  by (metis closure_of_openin_Int_closure_of inf.orderE)

lemma closure_of_openin_subtopology_Int_closure_of:
  assumes S: "openin (subtopology X U) S" and "T \ 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)
  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 \<open>T \<subseteq> U\<close> 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 (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
  qed
qed

lemma closure_of_subtopology_open:
     "openin X U \ 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\<open> Interior with respect to a topological space.                             \<close>

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"
proof -
  have "\A. U \ X closure_of (U \ A) = U \ X closure_of A"
    using assms openin_Int_closure_of_eq by blast
  then have "topspace X \ U - U \ X closure_of (topspace X \ U - S) = U \ (topspace X - X closure_of (topspace X - S))"
    by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
  then show ?thesis
    unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
    using openin_Int_closure_of_eq [OF assms]
    by (metis assms closure_of_subtopology_open)
qed

lemma dense_intersects_open:
   "X closure_of S = topspace X \ (\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
        \<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
             X interior_of S = {} \<and> X interior_of T = {})"
  by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)

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

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

definition frontier_of :: "'a topology \ '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 \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> 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 \<inter> T) \<inter> (X frontier_of S \<union> 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)

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

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

lemma finite_imp_locally_finite_in:
   "\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 \<open>\<B> \<subseteq> \<A>\<close> 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 \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> 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 \<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 \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
  next
    show "\x xa. \xa \ \; x \ f xa\ \ x \ topspace X"
      by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
  qed
qed

lemma locally_finite_in_subtopology:
  assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
  shows "locally_finite_in (subtopology X S) \"
  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 \<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: \<open>openin X V\<close> 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 \<open>x \<in> V\<close> 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 \<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 \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
      show "x \ ?T"
        using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
      show "?T \ topspace X - \\"
        using \<open>openin X V\<close> openin_subset by auto
    qed
  qed
qed

lemma locally_finite_in_closure:
  assumes \<A>: "locally_finite_in X \<A>"
  shows "locally_finite_in X ((\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 Q
    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 clarify (meson Union_upper closure_of_mono subsetD)

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\<^marker>\<open>tag important\<close> \<open>Continuous maps\<close>

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

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

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

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

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

lemma continuous_map_closedin:
   "continuous_map X Y f \
         (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
proof -
  have "(\U. openin Y U \ openin X {x \ topspace X. f x \ U}) =
        (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
    if "\x. x \ topspace X \ f 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 have "openin X {x \ topspace X. f x \ topspace Y - C}" by blast
      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 have "closedin X {x \ topspace X. f x \ topspace Y - U}" by blast
      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"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.70 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Abstract_Topology.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.70 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©