(* Author: L C Paulson, University of Cambridge [ported from HOL Light] *) section ‹Operators involving abstract topology› theory Abstract_Topology imports Complex_Main "HOL-Library.Set_Idioms" "HOL-Library.FuncSet" begin subsection ‹General notion of a topology as a value› definition✐‹tag important› istopology :: "('a set ⇒ bool) ⇒ bool" where "istopology L ≡ (∀S T. L S ⟶ L T ⟶ L (S ∩ T)) ∧ (∀𝒦. (∀K∈𝒦. L K) ⟶ L (⋃𝒦))" typedef✐‹tag important› 'a topology = "{L::('a set) ⇒ bool. istopology L}" morphisms "openin" "topology" unfolding istopology_def by blast lemma istopology_openin[iff]: "istopology(openin U)" using openin[of U] by blast lemma istopology_open[iff]: "istopology open" by (auto simp: istopology_def) lemma topology_inverse' [simp]: "istopology U ⟹ openin (topology U) = U" using topology_inverse[unfolded mem_Collect_eq] . lemma topology_inverse_iff: "istopology U ⟷ openin (topology U) = U" by (metis istopology_openin topology_inverse') lemma topology_eq: "T1 = T2 ⟷ (∀S. openin T1 S ⟷ openin T2 S)" proof assume "T1 = T2" then show "∀S. openin T1 S ⟷ openin T2 S" by simp next assume H: "∀S. openin T1 S ⟷ openin T2 S" then have "openin T1 = openin T2" by (simp add: fun_eq_iff) then have "topology (openin T1) = topology (openin T2)" by simp then show "T1 = T2" unfolding openin_inverse . qed text‹The "universe": the union of all sets in the topology.› definition "topspace T = ⋃{S. openin T S}" subsubsection ‹Main properties of open sets› proposition openin_clauses: fixes U :: "'a topology" shows "openin U {}" "⋀S T. openin U S ⟹ openin U T ⟹ openin U (S∩T)" "⋀K. (∀S ∈ K. openin U S) ⟹ openin U (⋃K)" using openin[of U] unfolding istopology_def by auto lemma openin_subset: "openin U S ⟹ S ⊆ topspace U" unfolding topspace_def by blast lemma openin_empty[simp]: "openin U {}" by (rule openin_clauses) lemma openin_Int[intro]: "openin U S ⟹ openin U T ⟹ openin U (S ∩ T)" by (rule openin_clauses) lemma openin_Union[intro]: "(⋀S. S ∈ K ⟹ openin U S) ⟹ openin U (⋃K)" using openin_clauses by blast lemma openin_Un[intro]: "openin U S ⟹ openin U T ⟹ openin U (S ∪ T)" using openin_Union[of "{S,T}" U] by auto lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (force simp: openin_Union topspace_def) lemma openin_subopen: "openin U S ⟷ (∀x ∈ S. ∃T. openin U T ∧ x ∈ T ∧ T ⊆ S)" (is "?lhs ⟷ ?rhs") proof assume ?lhs then show ?rhs by auto next assume H: ?rhs let ?t = "⋃{T. openin U T ∧ T ⊆ S}" have "openin U ?t" by (force simp: openin_Union) also have "?t = S" using H by auto finally show "openin U S" . qed lemma openin_INT [intro]: assumes "finite I" "⋀i. i ∈ I ⟹ openin T (U i)" shows "openin T ((⋂i ∈ I. U i) ∩ topspace T)" using assms by (induct, auto simp: inf_sup_aci(2) openin_Int) lemma openin_INT2 [intro]: assumes "finite I" "I ≠ {}" "⋀i. i ∈ I ⟹ openin T (U i)" shows "openin T (⋂i ∈ I. U i)" proof - have "(⋂i ∈ I. U i) ⊆ topspace T" using ‹I ≠ {}› openin_subset[OF assms(3)] by auto then show ?thesis using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute) qed lemma openin_Inter [intro]: assumes "finite ℱ" "ℱ ≠ {}" "⋀X. X ∈ ℱ ⟹ openin T X" shows "openin T (⋂ℱ)" by (metis (full_types) assms openin_INT2 image_ident) lemma openin_Int_Inter: assumes "finite ℱ" "openin T U" "⋀X. X ∈ ℱ ⟹ openin T X" shows "openin T (U ∩ ⋂ℱ)" using openin_Inter [of "insert U ℱ"] assms by auto subsubsection ‹Closed sets› definition✐‹tag important› closedin :: "'a topology ⇒ 'a set ⇒ bool" where "closedin U S ⟷ S ⊆ topspace U ∧ openin U (topspace U - S)" lemma closedin_subset: "closedin U S ⟹ S ⊆ topspace U" by (metis closedin_def) lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" by (simp add: closedin_def) lemma closedin_Un[intro]: "closedin U S ⟹ closedin U T ⟹ closedin U (S ∪ T)" by (auto simp: Diff_Un closedin_def) lemma Diff_Inter[intro]: "A - ⋂S = ⋃{A - s|s. s∈S}" by auto lemma closedin_Union: assumes "finite S" "⋀T. T ∈ S ⟹ closedin U T" shows "closedin U (⋃S)" using assms by induction auto lemma closedin_Inter[intro]: assumes Ke: "K ≠ {}" and Kc: "⋀S. S ∈K ⟹ closedin U S" shows "closedin U (⋂K)" using Ke Kc unfolding closedin_def Diff_Inter by auto lemma closedin_INT[intro]: assumes "A ≠ {}" "⋀x. x ∈ A ⟹ closedin U (B x)" shows "closedin U (⋂x∈A. B x)" using assms by blast lemma closedin_Int[intro]: "closedin U S ⟹ closedin U T ⟹ closedin U (S ∩ T)" using closedin_Inter[of "{S,T}" U] by auto lemma openin_closedin_eq: "openin U S ⟷ S ⊆ topspace U ∧ closedin U (topspace U - S)" by (metis Diff_subset closedin_def double_diff equalityD1 openin_subset) lemma topology_finer_closedin: "topspace X = topspace Y ⟹ (∀S. openin Y S ⟶ openin X S) ⟷ (∀S. closedin Y S ⟶ closedin X S)" by (metis closedin_def openin_closedin_eq) lemma openin_closedin: "S ⊆ topspace U ⟹ (openin U S ⟷ closedin U (topspace U - S))" by (simp add: openin_closedin_eq) lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)" by (metis Int_Diff cT closedin_def inf.orderE oS openin_Int openin_subset) lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)" by (metis Int_Diff cT closedin_Int closedin_subset inf.orderE oS openin_closedin_eq) lemma all_openin: "(∀U. openin X U ⟶ P U) ⟷ (∀U. closedin X U ⟶ P (topspace X - U))" by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq) lemma all_closedin: "(∀U. closedin X U ⟶ P U) ⟷ (∀U. openin X U ⟶ P (topspace X - U))" by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq) lemma ex_openin: "(∃U. openin X U ∧ P U) ⟷ (∃U. closedin X U ∧ P (topspace X - U))" by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq) lemma ex_closedin: "(∃U. closedin X U ∧ P U) ⟷ (∃U. openin X U ∧ P (topspace X - U))" by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq) subsection‹The discrete topology› definition discrete_topology where "discrete_topology U ≡ topology (λS. S ⊆ U)" lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S ⟷ S ⊆ U" proof - have "istopology (λS. S ⊆ U)" by (auto simp: istopology_def) then show ?thesis by (simp add: discrete_topology_def topology_inverse') qed lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U" by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym) lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S ⟷ S ⊆ U" by (simp add: closedin_def) lemma discrete_topology_unique: "discrete_topology U = X ⟷ topspace X = U ∧ (∀x ∈ U. openin X {x})" (is "?lhs = ?rhs") proof assume R: ?rhs then have "openin X S" if "S ⊆ U" for S using openin_subopen subsetD that by fastforce then show ?lhs by (metis R openin_discrete_topology openin_subset topology_eq) qed auto lemma discrete_topology_unique_alt: "discrete_topology U = X ⟷ topspace X ⊆ U ∧ (∀x ∈ U. openin X {x})" using openin_subset by (auto simp: discrete_topology_unique) lemma subtopology_eq_discrete_topology_empty: "X = discrete_topology {} ⟷ topspace X = {}" using discrete_topology_unique [of "{}" X] by auto lemma subtopology_eq_discrete_topology_sing: "X = discrete_topology {a} ⟷ topspace X = {a}" by (metis discrete_topology_unique openin_topspace singletonD) abbreviation trivial_topology where "trivial_topology ≡ discrete_topology {}" lemma null_topspace_iff_trivial [simp]: "topspace X = {} ⟷ X = trivial_topology" by (simp add: subtopology_eq_discrete_topology_empty) subsection ‹Subspace topology› definition✐‹tag important› subtopology :: "'a topology ⇒ 'a set ⇒ 'a topology" where "subtopology U V = topology (λT. ∃S. T = S ∩ V ∧ openin U S)" lemma istopology_subtopology: "istopology (λT. ∃S. T = S ∩ V ∧ openin U S)" (is "istopology ?L") proof - have "?L {}" by blast { fix A B assume A: "?L A" and B: "?L B" from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa ∩ V" and Sb: "openin U Sb" "B = Sb ∩ V" by blast have "A ∩ B = (Sa ∩ Sb) ∩ V" "openin U (Sa ∩ Sb)" using Sa Sb by blast+ then have "?L (A ∩ B)" by blast } moreover { fix K assume K: "K ⊆ Collect ?L" have th0: "Collect ?L = (λS. S ∩ V) ` Collect (openin U)" by blast from K[unfolded th0 subset_image_iff] obtain Sk where Sk: "Sk ⊆ Collect (openin U)" "K = (λS. S ∩ V) ` Sk" by blast have "⋃K = (⋃Sk) ∩ V" using Sk by auto moreover have "openin U (⋃Sk)" using Sk by (auto simp: subset_eq) ultimately have "?L (⋃K)" by blast } ultimately show ?thesis unfolding subset_eq mem_Collect_eq istopology_def by auto qed lemma openin_subtopology: "openin (subtopology U V) S ⟷ (∃T. openin U T ∧ S = T ∩ V)" unfolding subtopology_def topology_inverse'[OF istopology_subtopology] by auto lemma subset_openin_subtopology: "⟦openin X S; S ⊆ T⟧ ⟹ openin (subtopology X T) S" by (metis inf.orderE openin_subtopology) lemma openin_subtopology_Int: "openin X S ⟹ openin (subtopology X T) (S ∩ T)" using openin_subtopology by auto lemma openin_subtopology_Int2: "openin X T ⟹ openin (subtopology X S) (S ∩ T)" using openin_subtopology by auto lemma openin_subtopology_diff_closed: "⟦S ⊆ topspace X; closedin X T⟧ ⟹ openin (subtopology X S) (S - T)" unfolding closedin_def openin_subtopology by (rule_tac x="topspace X - T" in exI) auto lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)" by (force simp: relative_to_def openin_subtopology) lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U ∩ V" by (auto simp: topspace_def openin_subtopology) lemma topspace_subtopology_subset: "S ⊆ topspace X ⟹ topspace(subtopology X S) = S" by (simp add: inf.absorb_iff2) lemma closedin_subtopology: "closedin (subtopology U V) S ⟷ (∃T. closedin U T ∧ S = T ∩ V)" unfolding closedin_def topspace_subtopology by (auto simp: openin_subtopology) lemma closedin_subtopology_Int_closed: "closedin X T ⟹ closedin (subtopology X S) (S ∩ T)" using closedin_subtopology inf_commute by blast lemma closedin_subset_topspace: "⟦closedin X S; S ⊆ T⟧ ⟹ closedin (subtopology X T) S" using closedin_subtopology by fastforce lemma closedin_relative_to: "(closedin X relative_to S) = closedin (subtopology X S)" by (force simp: relative_to_def closedin_subtopology) lemma openin_subtopology_refl: "openin (subtopology U V) V ⟷ V ⊆ topspace U" unfolding openin_subtopology by auto (metis IntD1 in_mono openin_subset) lemma subtopology_trivial_iff: "subtopology X S = trivial_topology ⟷ X = trivial_topology ∨ topspace X ∩ S = {}" by (auto simp flip: null_topspace_iff_trivial) lemma subtopology_subtopology: "subtopology (subtopology X S) T = subtopology X (S ∩ T)" proof - have eq: "⋀T'. (∃S'. T' = S' ∩ T ∧ (∃T. openin X T ∧ S' = T ∩ S)) = (∃Sa. T' = Sa ∩ (S ∩ T) ∧ openin X Sa)" by (metis inf_assoc) have "subtopology (subtopology X S) T = topology (λTa. ∃Sa. Ta = Sa ∩ T ∧ openin (subtopology X S) Sa)" by (simp add: subtopology_def) also have "… = subtopology X (S ∩ T)" by (simp add: openin_subtopology eq) (simp add: subtopology_def) finally show ?thesis . qed lemma openin_subtopology_alt: "openin (subtopology X U) S ⟷ S ∈ (λT. U ∩ T) ` Collect (openin X)" by (simp add: image_iff inf_commute openin_subtopology) lemma closedin_subtopology_alt: "closedin (subtopology X U) S ⟷ S ∈ (λT. U ∩ T) ` Collect (closedin X)" by (simp add: image_iff inf_commute closedin_subtopology) lemma subtopology_superset: assumes UV: "topspace U ⊆ V" shows "subtopology U V = U" proof - { fix S have "openin U S" if "openin U T" "S = T ∩ V" for T by (metis Int_subset_iff assms inf.orderE openin_subset that) then have "(∃T. openin U T ∧ S = T ∩ V) ⟷ openin U S" by (metis assms inf.orderE inf_assoc openin_subset) } then show ?thesis unfolding topology_eq openin_subtopology by blast qed lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" by (simp add: subtopology_superset) lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" by (simp add: subtopology_superset) lemma subtopology_empty_iff_trivial [simp]: "subtopology X {} = trivial_topology" by (simp add: subtopology_eq_discrete_topology_empty) lemma subtopology_restrict: "subtopology X (topspace X ∩ S) = subtopology X S" by (metis subtopology_subtopology subtopology_topspace) lemma openin_subtopology_empty: "openin (subtopology U {}) S ⟷ S = {}" by (metis Int_empty_right openin_empty openin_subtopology) lemma closedin_subtopology_empty: "closedin (subtopology U {}) S ⟷ S = {}" by (metis Int_empty_right closedin_empty closedin_subtopology) lemma closedin_subtopology_refl [simp]: "closedin (subtopology U X) X ⟷ X ⊆ topspace U" by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology) lemma closedin_topspace_empty [simp]: "closedin trivial_topology S ⟷ S = {}" by (simp add: closedin_def) lemma openin_topspace_empty [simp]: "openin trivial_topology S ⟷ S = {}" by (simp add: openin_closedin_eq) lemma openin_imp_subset: "openin (subtopology U S) T ⟹ T ⊆ S" by (metis Int_iff openin_subtopology subsetI) lemma closedin_imp_subset: "closedin (subtopology U S) T ⟹ T ⊆ S" by (simp add: closedin_def) lemma openin_open_subtopology: "openin X S ⟹ openin (subtopology X S) T ⟷ openin X T ∧ T ⊆ S" by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology) lemma closedin_closed_subtopology: "closedin X S ⟹ (closedin (subtopology X S) T ⟷ closedin X T ∧ T ⊆ S)" by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE) lemma closedin_trans_full: "⟦closedin (subtopology X U) S; closedin X U⟧ ⟹ closedin X S" using closedin_closed_subtopology by blast lemma openin_subtopology_Un: "⟦openin (subtopology X T) S; openin (subtopology X U) S⟧ ⟹ openin (subtopology X (T ∪ U)) S" by (simp add: openin_subtopology) blast lemma closedin_subtopology_Un: "⟦closedin (subtopology X T) S; closedin (subtopology X U) S⟧ ⟹ closedin (subtopology X (T ∪ U)) S" by (simp add: closedin_subtopology) blast lemma openin_trans_full: "⟦openin (subtopology X U) S; openin X U⟧ ⟹ openin X S" by (simp add: openin_open_subtopology) subsection ‹The canonical topology from the underlying type class› abbreviation✐‹tag important› euclidean :: "'a::topological_space topology" where "euclidean ≡ topology open" abbreviation top_of_set :: "'a::topological_space set ⇒ 'a topology" where "top_of_set ≡ subtopology (topology open)" lemma open_openin: "open S ⟷ openin euclidean S" by simp declare open_openin [symmetric, simp] lemma topspace_euclidean [simp]: "topspace euclidean = UNIV" by (force simp: topspace_def) lemma topspace_euclidean_subtopology[simp]: "topspace (top_of_set S) = S" by (simp) lemma closed_closedin: "closed S ⟷ closedin euclidean S" by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV) declare closed_closedin [symmetric, simp] lemma openin_subtopology_self [simp]: "openin (top_of_set S) S" by (metis openin_topspace topspace_euclidean_subtopology) lemma euclidean_nontrivial [simp]: "euclidean ≠ trivial_topology" by (simp add: subtopology_eq_discrete_topology_empty) subsubsection‹The most basic facts about the usual topology and metric on R› abbreviation euclideanreal :: "real topology" where "euclideanreal ≡ topology open" subsection ‹Basic "localization" results are handy for connectedness.› lemma openin_open: "openin (top_of_set U) S ⟷ (∃T. open T ∧ (S = U ∩ T))" by (auto simp: openin_subtopology) lemma openin_Int_open: "⟦openin (top_of_set U) S; open T⟧ ⟹ openin (top_of_set U) (S ∩ T)" by (metis open_Int Int_assoc openin_open) lemma openin_open_Int[intro]: "open S ⟹ openin (top_of_set U) (U ∩ S)" by (auto simp: openin_open) lemma open_openin_trans[trans]: "open S ⟹ open T ⟹ T ⊆ S ⟹ openin (top_of_set S) T" by (metis Int_absorb1 openin_open_Int) lemma open_subset: "S ⊆ T ⟹ open S ⟹ openin (top_of_set T) S" by (auto simp: openin_open) lemma closedin_closed: "closedin (top_of_set U) S ⟷ (∃T. closed T ∧ S = U ∩ T)" by (simp add: closedin_subtopology Int_ac) lemma closedin_closed_Int: "closed S ⟹ closedin (top_of_set U) (U ∩ S)" by (metis closedin_closed) lemma closed_subset: "S ⊆ T ⟹ closed S ⟹ closedin (top_of_set T) S" by (auto simp: closedin_closed) lemma closedin_closed_subset: "⟦closedin (top_of_set U) V; T ⊆ U; S = V ∩ T⟧ ⟹ closedin (top_of_set T) S" by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE) lemma finite_imp_closedin: fixes S :: "'a::t1_space set" shows "⟦finite S; S ⊆ T⟧ ⟹ closedin (top_of_set T) S" by (simp add: finite_imp_closed closed_subset) lemma closedin_singleton [simp]: fixes a :: "'a::t1_space" shows "closedin (top_of_set U) {a} ⟷ a ∈ U" using closedin_subset by (force intro: closed_subset) lemma openin_euclidean_subtopology_iff: fixes S U :: "'a::metric_space set" shows "openin (top_of_set U) S ⟷ S ⊆ U ∧ (∀x∈S. ∃e>0. ∀x'∈U. dist x' x < e ⟶ x'∈ S)" (is "?lhs ⟷ ?rhs") proof assume ?lhs then show ?rhs unfolding openin_open open_dist by blast next define T where "T = {x. ∃a∈S. ∃d>0. (∀y∈U. dist y a < d ⟶ y ∈ S) ∧ dist x a < d}" have 1: "∀x∈T. ∃e>0. ∀y. dist y x < e ⟶ y ∈ T" unfolding T_def apply clarsimp apply (rule_tac x="d - dist x a" in exI) by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq) assume ?rhs then have 2: "S = U ∩ T" unfolding T_def by auto (metis dist_self) from 1 2 show ?lhs unfolding openin_open open_dist by fast qed lemma connected_openin: "connected S ⟷ ¬(∃E1 E2. openin (top_of_set S) E1 ∧ openin (top_of_set S) E2 ∧ S ⊆ E1 ∪ E2 ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})" unfolding connected_def openin_open disjoint_iff_not_equal by blast lemma connected_openin_eq: "connected S ⟷ ¬(∃E1 E2. openin (top_of_set S) E1 ∧ openin (top_of_set S) E2 ∧ E1 ∪ E2 = S ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})" unfolding connected_openin by (metis (no_types, lifting) Un_subset_iff openin_imp_subset subset_antisym) lemma connected_closedin: "connected S ⟷ (∄E1 E2. closedin (top_of_set S) E1 ∧ closedin (top_of_set S) E2 ∧ S ⊆ E1 ∪ E2 ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (auto simp add: connected_closed closedin_closed) next assume R: ?rhs then show ?lhs proof (clarsimp simp add: connected_closed closedin_closed) fix A B assume s_sub: "S ⊆ A ∪ B" "B ∩ S ≠ {}" and disj: "A ∩ B ∩ S = {}" and cl: "closed A" "closed B" have "S - A = B ∩ S" using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto then show "A ∩ S = {}" by (metis Int_Diff_Un Int_Diff_disjoint R cl closedin_closed_Int dual_order.refl inf_commute s_sub(2)) qed qed lemma connected_closedin_eq: "connected S ⟷ ¬(∃E1 E2. closedin (top_of_set S) E1 ∧ closedin (top_of_set S) E2 ∧ E1 ∪ E2 = S ∧ E1 ∩ E2 = {} ∧ E1 ≠ {} ∧ E2 ≠ {})" unfolding connected_closedin by (metis Un_subset_iff closedin_imp_subset subset_antisym) text ‹These "transitivity" results are handy too› lemma openin_trans[trans]: "openin (top_of_set T) S ⟹ openin (top_of_set U) T ⟹ openin (top_of_set U) S" by (metis openin_Int_open openin_open) lemma openin_open_trans: "openin (top_of_set T) S ⟹ open T ⟹ open S" by (auto simp: openin_open intro: openin_trans) lemma closedin_trans[trans]: "closedin (top_of_set T) S ⟹ closedin (top_of_set U) T ⟹ closedin (top_of_set U) S" by (auto simp: closedin_closed closed_Inter Int_assoc) lemma closedin_closed_trans: "closedin (top_of_set T) S ⟹ closed T ⟹ closed S" by (auto simp: closedin_closed intro: closedin_trans) lemma openin_subtopology_Int_subset: "⟦openin (top_of_set u) (u ∩ S); v ⊆ u⟧ ⟹ openin (top_of_set v) (v ∩ S)" by (auto simp: openin_subtopology) lemma openin_open_eq: "open s ⟹ (openin (top_of_set s) t ⟷ open t ∧ t ⊆ s)" using open_subset openin_open_trans openin_subset by fastforce subsection‹Derived set (set of limit points)› definition derived_set_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixl "derived'_set'_of" 80) where "X derived_set_of S ≡ {x ∈ topspace X. (∀T. x ∈ T ∧ openin X T ⟶ (∃y≠x. y ∈ S ∧ y ∈ T))}" lemma derived_set_of_restrict [simp]: "X derived_set_of (topspace X ∩ S) = X derived_set_of S" by (simp add: derived_set_of_def) (metis openin_subset subset_iff) lemma in_derived_set_of: "x ∈ X derived_set_of S ⟷ x ∈ topspace X ∧ (∀T. x ∈ T ∧ openin X T ⟶ (∃y≠x. y ∈ S ∧ y ∈ T))" by (simp add: derived_set_of_def) lemma derived_set_of_subset_topspace: "X derived_set_of S ⊆ topspace X" by (auto simp add: derived_set_of_def) lemma derived_set_of_subtopology: "(subtopology X U) derived_set_of S = U ∩ (X derived_set_of (U ∩ S))" by (simp add: derived_set_of_def openin_subtopology) blast lemma derived_set_of_subset_subtopology: "(subtopology X S) derived_set_of T ⊆ S" by (simp add: derived_set_of_subtopology) lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}" by (auto simp: derived_set_of_def) lemma derived_set_of_mono: "S ⊆ T ⟹ X derived_set_of S ⊆ X derived_set_of T" unfolding derived_set_of_def by blast lemma derived_set_of_Un: "X derived_set_of (S ∪ T) = X derived_set_of S ∪ X derived_set_of T" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" by (clarsimp simp: in_derived_set_of) (metis IntE IntI openin_Int) show "?rhs ⊆ ?lhs" by (simp add: derived_set_of_mono) qed lemma derived_set_of_Union: "finite ℱ ⟹ X derived_set_of (⋃ℱ) = (⋃S ∈ ℱ. X derived_set_of S)" proof (induction ℱ rule: finite_induct) case (insert S ℱ) then show ?case by (simp add: derived_set_of_Un) qed auto lemma derived_set_of_topspace: "X derived_set_of (topspace X) = {x ∈ topspace X. ¬ openin X {x}}" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" by (auto simp: in_derived_set_of) show "?rhs ⊆ ?lhs" by (clarsimp simp: in_derived_set_of) (metis openin_closedin_eq openin_subopen singletonD subset_eq) qed lemma discrete_topology_unique_derived_set: "discrete_topology U = X ⟷ topspace X = U ∧ X derived_set_of U = {}" by (auto simp: discrete_topology_unique derived_set_of_topspace) lemma subtopology_eq_discrete_topology_eq: "subtopology X U = discrete_topology U ⟷ U ⊆ topspace X ∧ U ∩ X derived_set_of U = {}" using discrete_topology_unique_derived_set [of U "subtopology X U"] by (auto simp: eq_commute derived_set_of_subtopology) lemma subtopology_eq_discrete_topology: "S ⊆ topspace X ∧ S ∩ X derived_set_of S = {} ⟹ subtopology X S = discrete_topology S" by (simp add: subtopology_eq_discrete_topology_eq) lemma subtopology_eq_discrete_topology_gen: assumes "S ∩ X derived_set_of S = {}" shows "subtopology X S = discrete_topology(topspace X ∩ S)" proof - have "subtopology X S = subtopology X (topspace X ∩ S)" by (simp add: subtopology_restrict) then show ?thesis using assms by (simp add: inf.assoc subtopology_eq_discrete_topology_eq) qed lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U ∩ S)" proof - have "(λT. ∃Sa. T = Sa ∩ S ∧ Sa ⊆ U) = (λSa. Sa ⊆ U ∧ Sa ⊆ S)" by force then show ?thesis by (simp add: subtopology_def) (simp add: discrete_topology_def) qed lemma openin_Int_derived_set_of_subset: "openin X S ⟹ S ∩ X derived_set_of T ⊆ X derived_set_of (S ∩ T)" by (auto simp: derived_set_of_def) lemma openin_Int_derived_set_of_eq: assumes "openin X S" shows "S ∩ X derived_set_of T = S ∩ X derived_set_of (S ∩ T)" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" by (simp add: assms openin_Int_derived_set_of_subset) show "?rhs ⊆ ?lhs" by (metis derived_set_of_mono inf_commute inf_le1 inf_mono order_refl) qed subsection‹ Closure with respect to a topological space› definition closure_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr "closure'_of" 80) where "X closure_of S ≡ {x ∈ topspace X. ∀T. x ∈ T ∧ openin X T ⟶ (∃y ∈ S. y ∈ T)}" lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X ∩ S)" unfolding closure_of_def using openin_subset by blast lemma in_closure_of: "x ∈ X closure_of S ⟷ x ∈ topspace X ∧ (∀T. x ∈ T ∧ openin X T ⟶ (∃y. y ∈ S ∧ y ∈ T))" by (auto simp: closure_of_def) lemma closure_of: "X closure_of S = topspace X ∩ (S ∪ X derived_set_of S)" by (fastforce simp: in_closure_of in_derived_set_of) lemma closure_of_alt: "X closure_of S = topspace X ∩ S ∪ X derived_set_of S" using derived_set_of_subset_topspace [of X S] unfolding closure_of_def in_derived_set_of by safe (auto simp: in_derived_set_of) lemma derived_set_of_subset_closure_of: "X derived_set_of S ⊆ X closure_of S" by (fastforce simp: closure_of_def in_derived_set_of) lemma closure_of_subtopology: "(subtopology X U) closure_of S = U ∩ (X closure_of (U ∩ S))" unfolding closure_of_def topspace_subtopology openin_subtopology by safe (metis (full_types) IntI Int_iff inf.commute)+ lemma closure_of_empty [simp]: "X closure_of {} = {}" by (simp add: closure_of_alt) lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X" by (simp add: closure_of) lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X" by (simp add: closure_of) lemma closure_of_subset_topspace: "X closure_of S ⊆ topspace X" by (simp add: closure_of) lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T ⊆ S" by (simp add: closure_of_subtopology) lemma closure_of_mono: "S ⊆ T ⟹ X closure_of S ⊆ X closure_of T" by (fastforce simp add: closure_of_def) lemma closure_of_subtopology_subset: "(subtopology X U) closure_of S ⊆ (X closure_of S)" unfolding closure_of_subtopology by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2) lemma closure_of_subtopology_mono: "T ⊆ U ⟹ (subtopology X T) closure_of S ⊆ (subtopology X U) closure_of S" unfolding closure_of_subtopology by auto (meson closure_of_mono inf_mono subset_iff) lemma closure_of_Un [simp]: "X closure_of (S ∪ T) = X closure_of S ∪ X closure_of T" by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_Un inf_sup_distrib1) lemma closure_of_Union: "finite ℱ ⟹ X closure_of (⋃ℱ) = (⋃S ∈ ℱ. X closure_of S)" by (induction ℱ rule: finite_induct) auto lemma closure_of_subset: "S ⊆ topspace X ⟹ S ⊆ X closure_of S" by (auto simp: closure_of_def) lemma closure_of_subset_Int: "topspace X ∩ S ⊆ X closure_of S" by (auto simp: closure_of_def) lemma closure_of_subset_eq: "S ⊆ topspace X ∧ X closure_of S ⊆ S ⟷ closedin X S" proof - have "openin X (topspace X - S)" if "⋀x. ⟦x ∈ topspace X; ∀T. x ∈ T ∧ openin X T ⟶ S ∩ T ≠ {}⟧ ⟹ x ∈ S" apply (subst openin_subopen) by (metis Diff_iff Diff_mono Diff_triv inf.commute openin_subset order_refl that) then show ?thesis by (auto simp: closedin_def closure_of_def disjoint_iff_not_equal) qed lemma closure_of_eq: "X closure_of S = S ⟷ closedin X S" by (metis closure_of_subset closure_of_subset_eq closure_of_subset_topspace subset_antisym) lemma closedin_contains_derived_set: "closedin X S ⟷ X derived_set_of S ⊆ S ∧ S ⊆ topspace X" proof (intro iffI conjI) show "closedin X S ⟹ X derived_set_of S ⊆ S" using closure_of_eq derived_set_of_subset_closure_of by fastforce show "closedin X S ⟹ S ⊆ topspace X" using closedin_subset by blast show "X derived_set_of S ⊆ S ∧ S ⊆ topspace X ⟹ closedin X S" by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE) qed lemma derived_set_subset_gen: "X derived_set_of S ⊆ S ⟷ closedin X (topspace X ∩ S)" by (simp add: closedin_contains_derived_set derived_set_of_subset_topspace) lemma derived_set_subset: "S ⊆ topspace X ⟹ (X derived_set_of S ⊆ S ⟷ closedin X S)" by (simp add: closedin_contains_derived_set) lemma closedin_derived_set: "closedin (subtopology X T) S ⟷ S ⊆ topspace X ∧ S ⊆ T ∧ (∀x. x ∈ X derived_set_of S ∧ x ∈ T ⟶ x ∈ S)" by (auto simp: closedin_contains_derived_set derived_set_of_subtopology Int_absorb1) lemma closedin_Int_closure_of: "closedin (subtopology X S) T ⟷ S ∩ X closure_of T = T" by (metis Int_left_absorb closure_of_eq closure_of_subtopology) lemma closure_of_closedin: "closedin X S ⟹ X closure_of S = S" by (simp add: closure_of_eq) lemma closure_of_eq_diff: "X closure_of S = topspace X - ⋃{T. openin X T ∧ disjnt S T}" by (auto simp: closure_of_def disjnt_iff) lemma closedin_closure_of [simp]: "closedin X (X closure_of S)" unfolding closure_of_eq_diff by blast lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S" by (simp add: closure_of_eq) lemma closure_of_hull: assumes "S ⊆ topspace X" shows "X closure_of S = (closedin X) hull S" by (metis assms closedin_closure_of closure_of_eq closure_of_mono closure_of_subset hull_unique) lemma closure_of_minimal: "⟦S ⊆ T; closedin X T⟧ ⟹ (X closure_of S) ⊆ T" by (metis closure_of_eq closure_of_mono) lemma closure_of_minimal_eq: "⟦S ⊆ topspace X; closedin X T⟧ ⟹ (X closure_of S) ⊆ T ⟷ S ⊆ T" by (meson closure_of_minimal closure_of_subset subset_trans) lemma closure_of_unique: "⟦S ⊆ T; closedin X T; ⋀T'. ⟦S ⊆ T'; closedin X T'⟧ ⟹ T ⊆ T'⟧ ⟹ X closure_of S = T" by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans) lemma closure_of_eq_empty_gen: "X closure_of S = {} ⟷ disjnt (topspace X) S" unfolding disjnt_def closure_of_restrict [where S=S] using closure_of by fastforce lemma closure_of_eq_empty: "S ⊆ topspace X ⟹ X closure_of S = {} ⟷ S = {}" using closure_of_subset by fastforce lemma openin_Int_closure_of_subset: assumes "openin X S" shows "S ∩ X closure_of T ⊆ X closure_of (S ∩ T)" proof - have "S ∩ X derived_set_of T = S ∩ X derived_set_of (S ∩ T)" by (meson assms openin_Int_derived_set_of_eq) moreover have "S ∩ (S ∩ T) = S ∩ T" by fastforce ultimately show ?thesis by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1) qed lemma closure_of_openin_Int_closure_of: assumes "openin X S" shows "X closure_of (S ∩ X closure_of T) = X closure_of (S ∩ T)" proof show "X closure_of (S ∩ X closure_of T) ⊆ X closure_of (S ∩ T)" by (simp add: assms closure_of_minimal openin_Int_closure_of_subset) next show "X closure_of (S ∩ T) ⊆ X closure_of (S ∩ X closure_of T)" by (metis Int_subset_iff assms closure_of_alt closure_of_mono inf_mono openin_subset subset_refl sup.coboundedI1) qed lemma openin_Int_closure_of_eq: assumes "openin X S" shows "S ∩ X closure_of T = S ∩ X closure_of (S ∩ T)" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" by (simp add: assms openin_Int_closure_of_subset) show "?rhs ⊆ ?lhs" by (metis closure_of_mono inf_commute inf_le1 inf_mono order_refl) qed lemma openin_Int_closure_of_eq_empty: assumes "openin X S" shows "S ∩ X closure_of T = {} ⟷ S ∩ T = {}" (is "?lhs = ?rhs") proof show "?lhs ⟹ ?rhs" unfolding disjoint_iff by (meson assms in_closure_of in_mono openin_subset) show "?rhs ⟹ ?lhs" by (simp add: assms openin_Int_closure_of_eq) qed lemma closure_of_openin_Int_superset: "openin X S ∧ S ⊆ X closure_of T ⟹ X closure_of (S ∩ T) = X closure_of S" by (metis closure_of_openin_Int_closure_of inf.orderE) lemma closure_of_openin_subtopology_Int_closure_of: assumes S: "openin (subtopology X U) S" and "T ⊆ U" shows "X closure_of (S ∩ X closure_of T) = X closure_of (S ∩ T)" (is "?lhs = ?rhs") proof obtain S0 where S0: "openin X S0" "S = S0 ∩ U" using assms by (auto simp: openin_subtopology) then show "?lhs ⊆ ?rhs" proof - have "S0 ∩ X closure_of T = S0 ∩ X closure_of (S0 ∩ T)" by (meson S0(1) openin_Int_closure_of_eq) moreover have "S0 ∩ T = S0 ∩ U ∩ T" using ‹T ⊆ U› by fastforce ultimately have "S ∩ X closure_of T ⊆ X closure_of (S ∩ T)" using S0(2) by auto then show ?thesis by (meson closedin_closure_of closure_of_minimal) qed next show "?rhs ⊆ ?lhs" proof - have "T ∩ S ⊆ T ∪ X derived_set_of T" by force then show ?thesis by (smt (verit, del_insts) Int_iff in_closure_of inf.orderE openin_subset subsetI) qed qed lemma closure_of_subtopology_open: "openin X U ∨ S ⊆ U ⟹ (subtopology X U) closure_of S = U ∩ X closure_of S" by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq) lemma discrete_topology_closure_of: "(discrete_topology U) closure_of S = U ∩ S" by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl) text‹ Interior with respect to a topological space. › definition interior_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr "interior'_of" 80) where "X interior_of S ≡ {x. ∃T. openin X T ∧ x ∈ T ∧ T ⊆ S}" lemma interior_of_restrict: "X interior_of S = X interior_of (topspace X ∩ S)" using openin_subset by (auto simp: interior_of_def) lemma interior_of_eq: "(X interior_of S = S) ⟷ openin X S" unfolding interior_of_def using openin_subopen by blast lemma interior_of_openin: "openin X S ⟹ X interior_of S = S" by (simp add: interior_of_eq) lemma interior_of_empty [simp]: "X interior_of {} = {}" by (simp add: interior_of_eq) lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X" by (simp add: interior_of_eq) lemma openin_interior_of [simp]: "openin X (X interior_of S)" unfolding interior_of_def using openin_subopen by fastforce lemma interior_of_interior_of [simp]: "X interior_of X interior_of S = X interior_of S" by (simp add: interior_of_eq) lemma interior_of_subset: "X interior_of S ⊆ S" by (auto simp: interior_of_def) lemma interior_of_subset_closure_of: "X interior_of S ⊆ X closure_of S" by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset) lemma subset_interior_of_eq: "S ⊆ X interior_of S ⟷ openin X S" by (metis interior_of_eq interior_of_subset subset_antisym) lemma interior_of_mono: "S ⊆ T ⟹ X interior_of S ⊆ X interior_of T" by (auto simp: interior_of_def) lemma interior_of_maximal: "⟦T ⊆ S; openin X T⟧ ⟹ T ⊆ X interior_of S" by (auto simp: interior_of_def) lemma interior_of_maximal_eq: "openin X T ⟹ T ⊆ X interior_of S ⟷ T ⊆ S" by (meson interior_of_maximal interior_of_subset order_trans) lemma interior_of_unique: "⟦T ⊆ S; openin X T; ⋀T'. ⟦T' ⊆ S; openin X T'⟧ ⟹ T' ⊆ T⟧ ⟹ X interior_of S = T" by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym) lemma interior_of_subset_topspace: "X interior_of S ⊆ topspace X" by (simp add: openin_subset) lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T ⊆ S" by (meson openin_imp_subset openin_interior_of) lemma interior_of_Int: "X interior_of (S ∩ T) = X interior_of S ∩ X interior_of T" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" by (simp add: interior_of_mono) show "?rhs ⊆ ?lhs" by (meson inf_mono interior_of_maximal interior_of_subset openin_Int openin_interior_of) qed lemma interior_of_Inter_subset: "X interior_of (⋂ℱ) ⊆ (⋂S ∈ ℱ. X interior_of S)" by (simp add: INT_greatest Inf_lower interior_of_mono) lemma union_interior_of_subset: "X interior_of S ∪ X interior_of T ⊆ X interior_of (S ∪ T)" by (simp add: interior_of_mono) lemma interior_of_eq_empty: "X interior_of S = {} ⟷ (∀T. openin X T ∧ T ⊆ S ⟶ T = {})" by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of) lemma interior_of_eq_empty_alt: "X interior_of S = {} ⟷ (∀T. openin X T ∧ T ≠ {} ⟶ T - S ≠ {})" by (auto simp: interior_of_eq_empty) lemma interior_of_Union_openin_subsets: "⋃{T. openin X T ∧ T ⊆ S} = X interior_of S" by (rule interior_of_unique [symmetric]) auto lemma interior_of_complement: "X interior_of (topspace X - S) = topspace X - X closure_of S" by (auto simp: interior_of_def closure_of_def) lemma interior_of_closure_of: "X interior_of S = topspace X - X closure_of (topspace X - S)" unfolding interior_of_complement [symmetric] by (metis Diff_Diff_Int interior_of_restrict) lemma closure_of_interior_of: "X closure_of S = topspace X - X interior_of (topspace X - S)" by (simp add: interior_of_complement Diff_Diff_Int closure_of) lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S" unfolding interior_of_def closure_of_def by (blast dest: openin_subset) lemma interior_of_eq_empty_complement: "X interior_of S = {} ⟷ X closure_of (topspace X - S) = topspace X" using interior_of_subset_topspace [of X S] closure_of_complement by fastforce lemma closure_of_eq_topspace: "X closure_of S = topspace X ⟷ X interior_of (topspace X - S) = {}" using closure_of_subset_topspace [of X S] interior_of_complement by fastforce lemma interior_of_subtopology_subset: "U ∩ X interior_of S ⊆ (subtopology X U) interior_of S" by (auto simp: interior_of_def openin_subtopology) lemma interior_of_subtopology_subsets: "T ⊆ U ⟹ T ∩ (subtopology X U) interior_of S ⊆ (subtopology X T) interior_of S" by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology) lemma interior_of_subtopology_mono: "⟦S ⊆ T; T ⊆ U⟧ ⟹ (subtopology X U) interior_of S ⊆ (subtopology X T) interior_of S" by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets) lemma interior_of_subtopology_open: assumes "openin X U" shows "(subtopology X U) interior_of S = U ∩ X interior_of S" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" by (meson assms interior_of_maximal interior_of_subset le_infI openin_interior_of openin_open_subtopology) show "?rhs ⊆ ?lhs" by (simp add: interior_of_subtopology_subset) qed lemma dense_intersects_open: "X closure_of S = topspace X ⟷ (∀T. openin X T ∧ T ≠ {} ⟶ S ∩ T ≠ {})" proof - have "X closure_of S = topspace X ⟷ (topspace X - X interior_of (topspace X - S) = topspace X)" by (simp add: closure_of_interior_of) also have "… ⟷ X interior_of (topspace X - S) = {}" by (simp add: closure_of_complement interior_of_eq_empty_complement) also have "… ⟷ (∀T. openin X T ∧ T ≠ {} ⟶ S ∩ T ≠ {})" unfolding interior_of_eq_empty_alt using openin_subset by fastforce finally show ?thesis . qed lemma interior_of_closedin_union_empty_interior_of: assumes "closedin X S" and disj: "X interior_of T = {}" shows "X interior_of (S ∪ T) = X interior_of S" proof - have "X closure_of (topspace X - T) = topspace X" by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of) then show ?thesis unfolding interior_of_closure_of by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset) qed lemma interior_of_union_eq_empty: "closedin X S ⟹ (X interior_of (S ∪ T) = {} ⟷ X interior_of S = {} ∧ X interior_of T = {})" by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset) lemma discrete_topology_interior_of [simp]: "(discrete_topology U) interior_of S = U ∩ S" by (simp add: interior_of_restrict [of _ S] interior_of_eq) subsection ‹Frontier with respect to topological space › definition frontier_of :: "'a topology ⇒ 'a set ⇒ 'a set" (infixr "frontier'_of" 80) where "X frontier_of S ≡ X closure_of S - X interior_of S" lemma frontier_of_closures: "X frontier_of S = X closure_of S ∩ X closure_of (topspace X - S)" by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of) lemma interior_of_union_frontier_of [simp]: "X interior_of S ∪ X frontier_of S = X closure_of S" by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym) lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X ∩ S)" by (metis closure_of_restrict frontier_of_def interior_of_restrict) lemma closedin_frontier_of: "closedin X (X frontier_of S)" by (simp add: closedin_Int frontier_of_closures) lemma frontier_of_subset_topspace: "X frontier_of S ⊆ topspace X" by (simp add: closedin_frontier_of closedin_subset) lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T ⊆ S" by (metis (no_types) closedin_derived_set closedin_frontier_of) lemma frontier_of_subtopology_subset: "U ∩ (subtopology X U) frontier_of S ⊆ (X frontier_of S)" proof - have "U ∩ X interior_of S - subtopology X U interior_of S = {}" by (simp add: interior_of_subtopology_subset) moreover have "X closure_of S ∩ subtopology X U closure_of S = subtopology X U closure_of S" by (meson closure_of_subtopology_subset inf.absorb_iff2) ultimately show ?thesis unfolding frontier_of_def by blast qed lemma frontier_of_subtopology_mono: "⟦S ⊆ T; T ⊆ U⟧ ⟹ (subtopology X T) frontier_of S ⊆ (subtopology X U) frontier_of S" by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono) lemma clopenin_eq_frontier_of: "closedin X S ∧ openin X S ⟷ S ⊆ topspace X ∧ X frontier_of S = {}" proof (cases "S ⊆ topspace X") case True then show ?thesis by (metis Diff_eq_empty_iff closure_of_eq closure_of_subset_eq frontier_of_def interior_of_eq interior_of_subset interior_of_union_frontier_of sup_bot_right) next case False then show ?thesis by (simp add: frontier_of_closures openin_closedin_eq) qed lemma frontier_of_eq_empty: "S ⊆ topspace X ⟹ (X frontier_of S = {} ⟷ closedin X S ∧ openin X S)" by (simp add: clopenin_eq_frontier_of) lemma frontier_of_openin: "openin X S ⟹ X frontier_of S = X closure_of S - S" by (metis (no_types) frontier_of_def interior_of_eq) lemma frontier_of_openin_straddle_Int: assumes "openin X U" "U ∩ X frontier_of S ≠ {}" shows "U ∩ S ≠ {}" "U - S ≠ {}" proof - have "U ∩ (X closure_of S ∩ X closure_of (topspace X - S)) ≠ {}" using assms by (simp add: frontier_of_closures) then show "U ∩ S ≠ {}" using assms openin_Int_closure_of_eq_empty by fastforce show "U - S ≠ {}" proof - have "∃A. X closure_of (A - S) ∩ U ≠ {}" using ‹U ∩ (X closure_of S ∩ X closure_of (topspace X - S)) ≠ {}› by blast then have "¬ U ⊆ S" by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty) then show ?thesis by blast qed qed lemma frontier_of_subset_closedin: "closedin X S ⟹ (X frontier_of S) ⊆ S" using closure_of_eq frontier_of_def by fastforce lemma frontier_of_empty [simp]: "X frontier_of {} = {}" by (simp add: frontier_of_def) lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}" by (simp add: frontier_of_def) lemma frontier_of_subset_eq: assumes "S ⊆ topspace X" shows "(X frontier_of S) ⊆ S ⟷ closedin X S" proof show "X frontier_of S ⊆ S ⟹ closedin X S" by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff) show "closedin X S ⟹ X frontier_of S ⊆ S" by (simp add: frontier_of_subset_closedin) qed lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S" by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute) lemma frontier_of_disjoint_eq: assumes "S ⊆ topspace X" shows "((X frontier_of S) ∩ S = {} ⟷ openin X S)" proof assume "X frontier_of S ∩ S = {}" then have "closedin X (topspace X - S)" using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce then show "openin X S" using assms by (simp add: openin_closedin) next show "openin X S ⟹ X frontier_of S ∩ S = {}" by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute) qed lemma frontier_of_disjoint_eq_alt: "S ⊆ (topspace X - X frontier_of S) ⟷ openin X S" proof (cases "S ⊆ topspace X") case True show ?thesis using True frontier_of_disjoint_eq by auto next case False then show ?thesis by (meson Diff_subset openin_subset subset_trans) qed lemma frontier_of_Int: "X frontier_of (S ∩ T) = X closure_of (S ∩ T) ∩ (X frontier_of S ∪ X frontier_of T)" proof - have *: "U ⊆ S ∧ U ⊆ T ⟹ U ∩ (S ∩ A ∪ T ∩ B) = U ∩ (A ∪ B)" for U S T A B :: "'a set" by blast show ?thesis by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un) qed lemma frontier_of_Int_subset: "X frontier_of (S ∩ T) ⊆ X frontier_of S ∪ X frontier_of T" by (simp add: frontier_of_Int) lemma frontier_of_Int_closedin: assumes "closedin X S" "closedin X T" shows "X frontier_of(S ∩ T) = X frontier_of S ∩ T ∪ S ∩ X frontier_of T" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" using assms by (force simp add: frontier_of_Int closedin_Int closure_of_closedin) show "?rhs ⊆ ?lhs" using assms frontier_of_subset_closedin by (auto simp add: frontier_of_Int closedin_Int closure_of_closedin) qed lemma frontier_of_Un_subset: "X frontier_of(S ∪ T) ⊆ X frontier_of S ∪ X frontier_of T" by (metis Diff_Un frontier_of_Int_subset frontier_of_complement) lemma frontier_of_Union_subset: "finite ℱ ⟹ X frontier_of (⋃ℱ) ⊆ (⋃T ∈ ℱ. X frontier_of T)" proof (induction ℱ rule: finite_induct) case (insert A ℱ) then show ?case using frontier_of_Un_subset by fastforce qed simp lemma frontier_of_frontier_of_subset: "X frontier_of (X frontier_of S) ⊆ X frontier_of S" by (simp add: closedin_frontier_of frontier_of_subset_closedin) lemma frontier_of_subtopology_open: "openin X U ⟹ (subtopology X U) frontier_of S = U ∩ X frontier_of S" by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open) lemma discrete_topology_frontier_of [simp]: "(discrete_topology U) frontier_of S = {}" by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures) lemma openin_subset_topspace_eq: assumes "disjnt S (X frontier_of U)" shows "openin (subtopology X U) S ⟷ openin X S ∧ S ⊆ U" proof assume S: "openin (subtopology X U) S" show "openin X S ∧ S ⊆ U" proof show "S ⊆ U" using S openin_imp_subset by blast have "disjnt S (X frontier_of (topspace X ∩ U))" by (metis assms frontier_of_restrict) moreover have "openin (subtopology X (topspace X ∩ U)) S" by (simp add: S subtopology_restrict) moreover have "openin X S" if dis: "disjnt S (X frontier_of U)" and ope: "openin (subtopology X U) S" and "U ⊆ topspace X" for S U proof - obtain T where T: "openin X T" "S = T ∩ U" using ope by (auto simp: openin_subtopology) have "T ∩ U = T ∩ X interior_of U" using that T interior_of_subset in_closure_of by (fastforce simp: disjnt_iff frontier_of_def) then show ?thesis using ‹S = T ∩ U› ‹openin X T› by auto qed ultimately show "openin X S" by blast qed qed (metis inf.absorb_iff1 openin_subtopology_Int) subsection‹Locally finite collections› definition locally_finite_in where "locally_finite_in X 𝒜 ⟷ (⋃𝒜 ⊆ topspace X) ∧ (∀x ∈ topspace X. ∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ 𝒜. U ∩ V ≠ {}})" lemma finite_imp_locally_finite_in: "⟦finite 𝒜; ⋃𝒜 ⊆ topspace X⟧ ⟹ locally_finite_in X 𝒜" by (auto simp: locally_finite_in_def) lemma locally_finite_in_subset: assumes "locally_finite_in X 𝒜" "ℬ ⊆ 𝒜" shows "locally_finite_in X ℬ" proof - have "finite (𝒜 ∩ {U. U ∩ V ≠ {}}) ⟹ finite (ℬ ∩ {U. U ∩ V ≠ {}})" for V by (meson ‹ℬ ⊆ 𝒜› finite_subset inf_le1 inf_le2 le_inf_iff subset_trans) then show ?thesis using assms unfolding locally_finite_in_def Int_def by fastforce qed lemma locally_finite_in_refinement: assumes 𝒜: "locally_finite_in X 𝒜" and f: "⋀S. S ∈ 𝒜 ⟹ f S ⊆ S" shows "locally_finite_in X (f ` 𝒜)" proof - show ?thesis unfolding locally_finite_in_def proof safe fix x assume "x ∈ topspace X" then obtain V where "openin X V" "x ∈ V" "finite {U ∈ 𝒜. U ∩ V ≠ {}}" using 𝒜 unfolding locally_finite_in_def by blast moreover have "{U ∈ 𝒜. f U ∩ V ≠ {}} ⊆ {U ∈ 𝒜. U ∩ V ≠ {}}" for V using f by blast ultimately have "finite {U ∈ 𝒜. f U ∩ V ≠ {}}" using finite_subset by blast moreover have "f ` {U ∈ 𝒜. f U ∩ V ≠ {}} = {U ∈ f ` 𝒜. U ∩ V ≠ {}}" by blast ultimately have "finite {U ∈ f ` 𝒜. U ∩ V ≠ {}}" by (metis (no_types, lifting) finite_imageI) then show "∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ f ` 𝒜. U ∩ V ≠ {}}" using ‹openin X V› ‹x ∈ V› by blast next show "⋀x xa. ⟦xa ∈ 𝒜; x ∈ f xa⟧ ⟹ x ∈ topspace X" by (meson Sup_upper 𝒜 f locally_finite_in_def subset_iff) qed qed lemma locally_finite_in_subtopology: assumes 𝒜: "locally_finite_in X 𝒜" "⋃𝒜 ⊆ S" shows "locally_finite_in (subtopology X S) 𝒜" unfolding locally_finite_in_def proof safe fix x assume x: "x ∈ topspace (subtopology X S)" then obtain V where "openin X V" "x ∈ V" and fin: "finite {U ∈ 𝒜. U ∩ V ≠ {}}" using 𝒜 unfolding locally_finite_in_def topspace_subtopology by blast show "∃V. openin (subtopology X S) V ∧ x ∈ V ∧ finite {U ∈ 𝒜. U ∩ V ≠ {}}" proof (intro exI conjI) show "openin (subtopology X S) (S ∩ V)" by (simp add: ‹openin X V› openin_subtopology_Int2) have "{U ∈ 𝒜. U ∩ (S ∩ V) ≠ {}} ⊆ {U ∈ 𝒜. U ∩ V ≠ {}}" by auto with fin show "finite {U ∈ 𝒜. U ∩ (S ∩ V) ≠ {}}" using finite_subset by auto show "x ∈ S ∩ V" using x ‹x ∈ V› by (simp) qed next show "⋀x A. ⟦x ∈ A; A ∈ 𝒜⟧ ⟹ x ∈ topspace (subtopology X S)" using assms unfolding locally_finite_in_def topspace_subtopology by blast qed lemma closedin_locally_finite_Union: assumes clo: "⋀S. S ∈ 𝒜 ⟹ closedin X S" and 𝒜: "locally_finite_in X 𝒜" shows "closedin X (⋃𝒜)" using 𝒜 unfolding locally_finite_in_def closedin_def proof clarify show "openin X (topspace X - ⋃𝒜)" proof (subst openin_subopen, clarify) fix x assume "x ∈ topspace X" and "x ∉ ⋃𝒜" then obtain V where "openin X V" "x ∈ V" and fin: "finite {U ∈ 𝒜. U ∩ V ≠ {}}" using 𝒜 unfolding locally_finite_in_def by blast let ?T = "V - ⋃{S ∈ 𝒜. S ∩ V ≠ {}}" show "∃T. openin X T ∧ x ∈ T ∧ T ⊆ topspace X - ⋃𝒜" proof (intro exI conjI) show "openin X ?T" by (metis (no_types, lifting) fin ‹openin X V› clo closedin_Union mem_Collect_eq openin_diff) show "x ∈ ?T" using ‹x ∉ ⋃𝒜› ‹x ∈ V› by auto show "?T ⊆ topspace X - ⋃𝒜" using ‹openin X V› openin_subset by auto qed qed qed lemma locally_finite_in_closure: assumes 𝒜: "locally_finite_in X 𝒜" shows "locally_finite_in X ((λS. X closure_of S) ` 𝒜)" using 𝒜 unfolding locally_finite_in_def proof (intro conjI; clarsimp) fix x A assume "x ∈ X closure_of A" then show "x ∈ topspace X" by (meson in_closure_of) next fix x assume "x ∈ topspace X" and "⋃𝒜 ⊆ topspace X" then obtain V where V: "openin X V" "x ∈ V" and fin: "finite {U ∈ 𝒜. U ∩ V ≠ {}}" using 𝒜 unfolding locally_finite_in_def by blast have eq: "{y ∈ f ` 𝒜. Q y} = f ` {x. x ∈ 𝒜 ∧ Q(f x)}" for f and Q :: "'a set ⇒ bool" by blast have eq2: "{A ∈ 𝒜. X closure_of A ∩ V ≠ {}} = {A ∈ 𝒜. A ∩ V ≠ {}}" using openin_Int_closure_of_eq_empty V by blast have "finite {U ∈ (closure_of) X ` 𝒜. U ∩ V ≠ {}}" by (simp add: eq eq2 fin) with V show "∃V. openin X V ∧ x ∈ V ∧ finite {U ∈ (closure_of) X ` 𝒜. U ∩ V ≠ {}}" by blast qed lemma closedin_Union_locally_finite_closure: "locally_finite_in X 𝒜 ⟹ closedin X (⋃((λS. X closure_of S) ` 𝒜))" by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure) lemma closure_of_Union_subset: "⋃((λS. X closure_of S) ` 𝒜) ⊆ X closure_of (⋃𝒜)" by (simp add: SUP_le_iff Sup_upper closure_of_mono) lemma closure_of_locally_finite_Union: assumes "locally_finite_in X 𝒜" shows "X closure_of (⋃𝒜) = ⋃((λS. X closure_of S) ` 𝒜)" proof (rule closure_of_unique) show "⋃ 𝒜 ⊆ ⋃ ((closure_of) X ` 𝒜)" using assms by (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def) show "closedin X (⋃ ((closure_of) X ` 𝒜))" using assms by (simp add: closedin_Union_locally_finite_closure) show "⋀T'. ⟦⋃ 𝒜 ⊆ T'; closedin X T'⟧ ⟹ ⋃ ((closure_of) X ` 𝒜) ⊆ T'" by (simp add: Sup_le_iff closure_of_minimal) qed subsection✐‹tag important› ‹Continuous maps› text ‹We will need to deal with continuous maps in terms of topologies and not in terms of type classes, as defined below.› definition continuous_map where "continuous_map X Y f ≡ f ∈ topspace X → topspace Y ∧ (∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U})" lemma continuous_map: "continuous_map X Y f ⟷ f ` (topspace X) ⊆ topspace Y ∧ (∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U})" by (auto simp: continuous_map_def) lemma continuous_map_image_subset_topspace: "continuous_map X Y f ⟹ f ` (topspace X) ⊆ topspace Y" by (auto simp: continuous_map_def) lemma continuous_map_funspace: "continuous_map X Y f ⟹ f ∈ topspace X → topspace Y" by (auto simp: continuous_map_def) lemma continuous_map_on_empty [simp]: "continuous_map trivial_topology Y f" by (auto simp: continuous_map_def) lemma continuous_map_on_empty2 [simp]: "continuous_map X trivial_topology f ⟷ X = trivial_topology" using continuous_map_image_subset_topspace by fastforce lemma continuous_map_closedin: "continuous_map X Y f ⟷ f ∈ topspace X → topspace Y ∧ (∀C. closedin Y C ⟶ closedin X {x ∈ topspace X. f x ∈ C})" proof - have "(∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U}) = (∀C. closedin Y C ⟶ closedin X {x ∈ topspace X. f x ∈ C})" if "f ∈ topspace X → topspace Y" proof - have eq: "{x ∈ topspace X. f x ∈ topspace Y ∧ f x ∉ C} = (topspace X - {x ∈ topspace X. f x ∈ C})" for C using that by blast show ?thesis proof (intro iffI allI impI) fix C assume "∀U. openin Y U ⟶ openin X {x ∈ topspace X. f x ∈ U}" and "closedin Y C" then show "closedin X {x ∈ topspace X. f x ∈ C}" by (auto simp add: closedin_def eq) next fix U assume "∀C. closedin Y C ⟶ closedin X {x ∈ topspace X. f x ∈ C}" and "openin Y U" then show "openin X {x ∈ topspace X. f x ∈ U}" by (auto simp add: openin_closedin_eq eq) qed qed then show ?thesis by (auto simp: continuous_map_def) qed lemma openin_continuous_map_preimage: "⟦continuous_map X Y f; openin Y U⟧ ⟹ openin X {x ∈ topspace X. f x ∈ U}" by (simp add: continuous_map_def) lemma closedin_continuous_map_preimage: "⟦continuous_map X Y f; closedin Y C⟧ ⟹ closedin X {x ∈ topspace X. f x ∈ C}" by (simp add: continuous_map_closedin) lemma openin_continuous_map_preimage_gen: assumes "continuous_map X Y f" "openin X U" "openin Y V" shows "openin X {x ∈ U. f x ∈ V}" proof - have eq: "{x ∈ U. f x ∈ V} = U ∩ {x ∈ topspace X. f x ∈ V}" using assms(2) openin_closedin_eq by fastforce show ?thesis unfolding eq using assms openin_continuous_map_preimage by fastforce qed lemma closedin_continuous_map_preimage_gen: assumes "continuous_map X Y f" "closedin X U" "closedin Y V" shows "closedin X {x ∈ U. f x ∈ V}" proof - have eq: "{x ∈ U. f x ∈ V} = U ∩ {x ∈ topspace X. f x ∈ V}" using assms(2) closedin_def by fastforce show ?thesis unfolding eq using assms closedin_continuous_map_preimage by fastforce qed lemma continuous_map_image_closure_subset: assumes "continuous_map X Y f" shows "f ` (X closure_of S) ⊆ Y closure_of f ` S" proof - have *: "f ` (topspace X) ⊆ topspace Y" by (meson assms continuous_map) have "X closure_of T ⊆ {x ∈ X closure_of T. f x ∈ Y closure_of (f ` T)}" if "T ⊆ topspace X" for T proof (rule closure_of_minimal) show "T ⊆ {x ∈ X closure_of T. f x ∈ Y closure_of f ` T}" using closure_of_subset * that by (fastforce simp: in_closure_of) next show "closedin X {x ∈ X closure_of T. f x ∈ Y closure_of f ` T}" using assms closedin_continuous_map_preimage_gen by fastforce qed then show ?thesis by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq) qed lemma continuous_map_subset_aux1: "continuous_map X Y f ⟹ (∀S. f ` (X closure_of S) ⊆ Y closure_of f ` S)" using continuous_map_image_closure_subset by blast lemma continuous_map_subset_aux2: assumes "∀S. S ⊆ topspace X ⟶ f ` (X 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}" by (simp add: assms continuous_map_closure_preimage_subset) moreover have "X closure_of (topspace X - {x ∈