# Theory Abstract_Topology

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

section ‹Operators involving abstract topology›

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

subsection ‹General notion of a topology as a value›

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

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

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

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

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

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

lemma topology_eq: "T1 = T2 ⟷ (∀S. openin T1 S ⟷ openin T2 S)"
proof
assume "T1 = T2"
then show "∀S. openin T1 S ⟷ openin T2 S" by simp
next
assume H: "∀S. openin T1 S ⟷ openin T2 S"
then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
then have "topology (openin T1) = topology (openin T2)" by simp
then show "T1 = T2" unfolding openin_inverse .
qed

text‹The "universe": the union of all sets in the topology.›
definition "topspace T = ⋃{S. openin T S}"

subsubsection ‹Main properties of open sets›

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

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

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

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

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

lemma openin_Un[intro]: "openin U S ⟹ openin U T ⟹ openin U (S ∪ T)"
using openin_Union[of "{S,T}" U] by auto

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

lemma openin_subopen: "openin U S ⟷ (∀x ∈ S. ∃T. openin U T ∧ x ∈ T ∧ T ⊆ S)"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then show ?rhs by auto
next
assume H: ?rhs
let ?t = "⋃{T. openin U T ∧ T ⊆ S}"
have "openin U ?t" by (force simp: openin_Union)
also have "?t = S" using H by auto
finally show "openin U S" .
qed

lemma openin_INT [intro]:
assumes "finite I"
"⋀i. i ∈ I ⟹ openin T (U i)"
shows "openin T ((⋂i ∈ I. U i) ∩ topspace T)"
using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)

lemma openin_INT2 [intro]:
assumes "finite I" "I ≠ {}"
"⋀i. i ∈ I ⟹ openin T (U i)"
shows "openin T (⋂i ∈ I. U i)"
proof -
have "(⋂i ∈ I. U i) ⊆ topspace T"
using ‹I ≠ {}› openin_subset[OF assms(3)] by auto
then show ?thesis
using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
qed

lemma openin_Inter [intro]:
assumes "finite ℱ" "ℱ ≠ {}" "⋀X. X ∈ ℱ ⟹ openin T X" shows "openin T (⋂ℱ)"
by (metis (full_types) assms openin_INT2 image_ident)

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

subsubsection ‹Closed sets›

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

lemma closedin_subset: "closedin U S ⟹ S ⊆ topspace U"
by (metis closedin_def)

lemma closedin_empty[simp]: "closedin U {}"

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

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))"

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
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"

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"

subsection ‹Subspace topology›

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

lemma istopology_subtopology: "istopology (λT. ∃S. T = S ∩ V ∧ openin U S)"
(is "istopology ?L")
proof -
have "?L {}" by blast
{
fix A B
assume A: "?L A" and B: "?L B"
from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa ∩ V" and Sb: "openin U Sb" "B = Sb ∩ V"
by blast
have "A ∩ B = (Sa ∩ Sb) ∩ V" "openin U (Sa ∩ Sb)"
using Sa Sb by blast+
then have "?L (A ∩ B)" by blast
}
moreover
{
fix K
assume K: "K ⊆ Collect ?L"
have th0: "Collect ?L = (λS. S ∩ V) ` Collect (openin U)"
by blast
from K[unfolded th0 subset_image_iff]
obtain Sk where Sk: "Sk ⊆ Collect (openin U)" "K = (λS. S ∩ V) ` Sk"
by blast
have "⋃K = (⋃Sk) ∩ V"
using Sk by auto
moreover have "openin U (⋃Sk)"
using Sk by (auto simp: subset_eq)
ultimately have "?L (⋃K)" by blast
}
ultimately show ?thesis
unfolding subset_eq mem_Collect_eq istopology_def by auto
qed

lemma openin_subtopology: "openin (subtopology U V) S ⟷ (∃T. openin U T ∧ S = T ∩ V)"
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
by auto

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

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

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

lemma openin_subtopology_diff_closed:
"⟦S ⊆ topspace X; closedin X T⟧ ⟹ openin (subtopology X S) (S - T)"
unfolding closedin_def openin_subtopology
by (rule_tac x="topspace X - T" in exI) auto

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

lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U ∩ V"
by (auto simp: topspace_def openin_subtopology)

lemma topspace_subtopology_subset:
"S ⊆ topspace X ⟹ topspace(subtopology X S) = S"

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)"
also have "… = subtopology X (S ∩ T)"
finally show ?thesis .
qed

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

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

lemma subtopology_superset:
assumes UV: "topspace U ⊆ V"
shows "subtopology U V = U"
proof -
{ fix S
have "openin U S" if "openin U T" "S = T ∩ V" for T
by (metis Int_subset_iff assms inf.orderE openin_subset that)
then have "(∃T. openin U T ∧ S = T ∩ V) ⟷ openin U S"
by (metis assms inf.orderE inf_assoc openin_subset)
}
then show ?thesis
unfolding topology_eq openin_subtopology by blast
qed

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

lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"

lemma subtopology_empty_iff_trivial [simp]: "subtopology X {} = trivial_topology"

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 = {}"

lemma openin_topspace_empty [simp]:
"openin trivial_topology S ⟷ S = {}"

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"

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"

lemma closedin_subtopology_Un:
"⟦closedin (subtopology X T) S; closedin (subtopology X U) S⟧
⟹ closedin (subtopology X (T ∪ U)) S"

lemma openin_trans_full:
"⟦openin (subtopology X U) S; openin X U⟧ ⟹ openin X S"

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"

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)"

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"

lemma closedin_singleton [simp]:
fixes a :: "'a::t1_space"
shows "closedin (top_of_set U) {a} ⟷ a ∈ U"
using closedin_subset  by (force intro: closed_subset)

lemma openin_euclidean_subtopology_iff:
fixes S U :: "'a::metric_space set"
shows "openin (top_of_set U) S ⟷
S ⊆ U ∧ (∀x∈S. ∃e>0. ∀x'∈U. dist x' x < e ⟶ x'∈ S)"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding openin_open open_dist by blast
next
define T where "T = {x. ∃a∈S. ∃d>0. (∀y∈U. dist y a < d ⟶ y ∈ S) ∧ dist x a < d}"
have 1: "∀x∈T. ∃e>0. ∀y. dist y x < e ⟶ y ∈ T"
unfolding T_def
apply clarsimp
apply (rule_tac x="d - dist x a" in exI)
by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq)
assume ?rhs then have 2: "S = U ∩ T"
unfolding T_def
by auto (metis dist_self)
from 1 2 show ?lhs
unfolding openin_open open_dist by fast
qed

lemma connected_openin:
"connected S ⟷
¬(∃E1 E2. openin (top_of_set S) E1 ∧
openin (top_of_set S) E2 ∧
S ⊆ E1 ∪ E2 ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})"
unfolding connected_def openin_open disjoint_iff_not_equal by blast

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

lemma connected_closedin:
"connected S ⟷
(∄E1 E2.
closedin (top_of_set S) E1 ∧
closedin (top_of_set S) E2 ∧
S ⊆ E1 ∪ E2 ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (auto simp add: connected_closed closedin_closed)
next
assume R: ?rhs
then show ?lhs
proof (clarsimp simp add: connected_closed closedin_closed)
fix A B
assume s_sub: "S ⊆ A ∪ B" "B ∩ S ≠ {}"
and disj: "A ∩ B ∩ S = {}"
and cl: "closed A" "closed B"
have "S - A = B ∩ S"
using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
then show "A ∩ S = {}"
by (metis Int_Diff_Un Int_Diff_disjoint R cl closedin_closed_Int dual_order.refl inf_commute s_sub(2))
qed
qed

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

text ‹These "transitivity" results are handy too›

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

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

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

lemma closedin_closed_trans: "closedin (top_of_set T) S ⟹ closed T ⟹ closed S"
by (auto simp: closedin_closed intro: closedin_trans)

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

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

subsection‹Derived set (set of limit points)›

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

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

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

lemma derived_set_of_subset_topspace:
"X derived_set_of S ⊆ topspace X"

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"

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"
qed

lemma derived_set_of_Union:
"finite ℱ ⟹ X derived_set_of (⋃ℱ) = (⋃S ∈ ℱ. X derived_set_of S)"
proof (induction ℱ rule: finite_induct)
case (insert S ℱ)
then show ?case
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"

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)"
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
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"
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 {} = {}"

lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"

lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"

lemma closure_of_subset_topspace: "X closure_of S ⊆ topspace X"

lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T ⊆ S"

lemma closure_of_mono: "S ⊆ T ⟹ X closure_of S ⊆ X closure_of T"

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

lemma closure_of_subtopology_mono:
"T ⊆ U ⟹ (subtopology X T) closure_of S ⊆ (subtopology X U) closure_of S"
unfolding closure_of_subtopology
by auto (meson closure_of_mono inf_mono subset_iff)

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

lemma closure_of_Union:
"finite ℱ ⟹ X closure_of (⋃ℱ) = (⋃S ∈ ℱ. X closure_of S)"
by (induction ℱ rule: finite_induct) auto

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

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

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

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

lemma closedin_contains_derived_set:
"closedin X S ⟷ X derived_set_of S ⊆ S ∧ S ⊆ topspace X"
proof (intro iffI conjI)
show "closedin X S ⟹ X derived_set_of S ⊆ S"
using closure_of_eq derived_set_of_subset_closure_of by fastforce
show "closedin X S ⟹ S ⊆ topspace X"
using closedin_subset by blast
show "X derived_set_of S ⊆ S ∧ S ⊆ topspace X ⟹ closedin X S"
by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
qed

lemma derived_set_subset_gen:
"X derived_set_of S ⊆ S ⟷ closedin X (topspace X ∩ S)"

lemma derived_set_subset: "S ⊆ topspace X ⟹ (X derived_set_of S ⊆ S ⟷ closedin X S)"

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"

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"

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"
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"
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"

lemma interior_of_empty [simp]: "X interior_of {} = {}"

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

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"

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"

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"
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)"

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"
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)"
also have "… ⟷ X interior_of (topspace X - S) = {}"
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)"

lemma frontier_of_subset_topspace: "X frontier_of S ⊆ topspace X"

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 = {}"
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
qed

lemma frontier_of_eq_empty:
"S ⊆ topspace X ⟹ (X frontier_of S = {} ⟷ closedin X S ∧ openin X S)"

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)

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 {} = {}"

lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"

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"
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"

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

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

lemma frontier_of_Union_subset:
"finite ℱ ⟹ X frontier_of (⋃ℱ) ⊆ (⋃T ∈ ℱ. X frontier_of T)"
proof (induction ℱ rule: finite_induct)
case (insert A ℱ)
then show ?case
using frontier_of_Un_subset by fastforce
qed simp

lemma frontier_of_frontier_of_subset:
"X frontier_of (X frontier_of S) ⊆ X frontier_of S"

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"
moreover
have "openin X S"
if dis: "disjnt S (X frontier_of U)" and ope: "openin (subtopology X U) S" and "U ⊆ topspace X"
for S U
proof -
obtain T where T: "openin X T" "S = T ∩ U"
using ope by (auto simp: openin_subtopology)
have "T ∩ U = T ∩ X interior_of U"
using that T interior_of_subset in_closure_of by (fastforce simp: disjnt_iff frontier_of_def)
then show ?thesis
using ‹S = T ∩ U› ‹openin X T› by auto
qed
ultimately show "openin X S"
by blast
qed
qed (metis inf.absorb_iff1 openin_subtopology_Int)

subsection‹Locally finite collections›

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

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

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

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

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

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

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

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

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

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

subsection✐‹tag important› ‹Continuous maps›

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

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

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

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

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

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

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

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

lemma openin_continuous_map_preimage:
"⟦continuous_map X Y f; openin Y U⟧ ⟹ openin X {x ∈ topspace X. f x ∈ U}"

lemma closedin_continuous_map_preimage:
"⟦continuous_map X Y f; closedin Y C⟧ ⟹ closedin X {x ∈ topspace X. f x ∈ C}"

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

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

lemma continuous_map_image_closure_subset:
assumes "continuous_map X Y f"
shows "f ` (X closure_of S) ⊆ Y closure_of f ` S"
proof -
have *: "f ` (topspace X) ⊆ topspace Y"
by (meson assms continuous_map)
have "X closure_of T ⊆ {x ∈ X closure_of T. f x ∈ Y closure_of (f ` T)}"
if "T ⊆ topspace X" for T
proof (rule closure_of_minimal)
show "T ⊆ {x ∈ X closure_of T. f x ∈ Y closure_of f ` T}"
using closure_of_subset * that  by (fastforce simp: in_closure_of)
next
show "closedin X {x ∈ X closure_of T. f x ∈ Y closure_of f ` T}"
using assms closedin_continuous_map_preimage_gen by fastforce
qed
then show ?thesis
by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq)
qed

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

lemma continuous_map_subset_aux2:
assumes "∀S. S ⊆ topspace X ⟶ f ` (X closure_of S) ⊆ Y closure_of f ` S"
shows "continuous_map X Y f"
unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
show "f ∈ topspace X → topspace Y"
using assms closure_of_subset_topspace by fastforce
next
fix C
assume "closedin Y C"
then show "closedin X {x ∈ topspace X. f x ∈ C}"
proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
fix x
assume x: "x ∈ X closure_of {x ∈ topspace X. f x ∈ C}"
and "C ⊆ topspace Y" and "Y closure_of C ⊆ C"
show "x ∈ topspace X"
by (meson x in_closure_of)
have "{a ∈ topspace X. f a ∈ C} ⊆ topspace X"
by simp
moreover have "Y closure_of f ` {a ∈ topspace X. f a ∈ C} ⊆ C"
by (simp add: ‹closedin Y C› closure_of_minimal image_subset_iff)
ultimately show "f x ∈ C"
using x assms by blast
qed
qed

lemma continuous_map_eq_image_closure_subset:
"continuous_map X Y f ⟷ (∀S. f ` (X closure_of S) ⊆ Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis

lemma continuous_map_eq_image_closure_subset_alt:
"continuous_map X Y f ⟷ (∀S. S ⊆ topspace X ⟶ f ` (X closure_of S) ⊆ Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis

lemma continuous_map_eq_image_closure_subset_gen:
"continuous_map X Y f ⟷
f ∈ topspace X → topspace Y ∧
(∀S. f ` (X closure_of S) ⊆ Y closure_of f ` S)"
by (meson Pi_iff continuous_map continuous_map_eq_image_closure_subset image_subset_iff)

lemma continuous_map_closure_preimage_subset:
"continuous_map X Y f
⟹ X closure_of {x ∈ topspace X. f x ∈ T}
⊆ {x ∈ topspace X. f x ∈ Y closure_of T}"
unfolding continuous_map_closedin
by (rule closure_of_minimal) (use in_closure_of in ‹fastforce+›)

lemma continuous_map_frontier_frontier_preimage_subset:
assumes "continuous_map X Y f"
shows "X frontier_of {x ∈ topspace X. f x ∈ T} ⊆ {x ∈ topspace X. f x ∈ Y frontier_of T}"
proof -
have eq: "topspace X - {x ∈ topspace X. f x ∈ T} = {x ∈ topspace X. f x ∈ topspace Y - T}"
using assms unfolding continuous_map_def by blast
have "X closure_of {x ∈ topspace X. f x ∈ T} ⊆ {x ∈ topspace X. f x ∈ Y closure_of T}"