diff --git a/src/HOL/Analysis/Abstract_Topology.thy b/src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy +++ b/src/HOL/Analysis/Abstract_Topology.thy @@ -1,4800 +1,4799 @@ -(* Author: L C Paulson, University of Cambridge [ported from HOL Light] -*) +(* 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\<^marker>\tag important\ istopology :: "('a set \ bool) \ bool" where "istopology L \ (\S T. L S \ L T \ L (S \ T)) \ (\\. (\K\\. L K) \ L (\\))" typedef\<^marker>\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\<^marker>\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) subsection \Subspace topology\ definition\<^marker>\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 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_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_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_restrict: "subtopology X (topspace X \ S) = subtopology X S" by (metis subtopology_subtopology subtopology_topspace) lemma openin_subtopology_empty: "openin (subtopology U {}) S \ S = {}" by (metis Int_empty_right openin_empty openin_subtopology) lemma closedin_subtopology_empty: "closedin (subtopology U {}) S \ S = {}" by (metis Int_empty_right closedin_empty closedin_subtopology) lemma closedin_subtopology_refl [simp]: "closedin (subtopology U X) X \ X \ topspace U" by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology) lemma closedin_topspace_empty: "topspace T = {} \ (closedin T S \ S = {})" by (simp add: closedin_def) lemma open_in_topspace_empty: "topspace X = {} \ openin X S \ S = {}" by (simp add: openin_closedin_eq) lemma openin_imp_subset: "openin (subtopology U S) T \ T \ S" by (metis Int_iff openin_subtopology subsetI) lemma closedin_imp_subset: "closedin (subtopology U S) T \ T \ S" by (simp add: closedin_def) lemma openin_open_subtopology: "openin X S \ openin (subtopology X S) T \ openin X T \ T \ S" by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology) lemma closedin_closed_subtopology: "closedin X S \ (closedin (subtopology X S) T \ closedin X T \ T \ S)" by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE) lemma openin_subtopology_Un: "\openin (subtopology X T) S; openin (subtopology X U) S\ \ 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\<^marker>\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) 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) 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\<^marker>\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 \ (\x \ topspace X. f 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_on_empty: "topspace X = {} \ continuous_map X Y f" by (auto simp: continuous_map_def) lemma continuous_map_closedin: "continuous_map X Y f \ (\x \ topspace X. f 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 "\x. x \ topspace X \ f x \ topspace Y" proof - have eq: "{x \ topspace X. f x \ topspace Y \ f x \ C} = (topspace X - {x \ topspace X. f x \ C})" for C using that by blast show ?thesis proof (intro iffI allI impI) fix C assume "\U. openin Y U \ openin X {x \ topspace X. f x \ U}" and "closedin Y C" then 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) fix x assume "x \ topspace X" then show "f 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)" using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis 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 \ topspace X. f x \ T}) \ {x \ topspace X. f x \ Y closure_of (topspace Y - T)}" using continuous_map_closure_preimage_subset [OF assms] eq by presburger ultimately show ?thesis by (auto simp: frontier_of_closures) qed lemma topology_finer_continuous_id: assumes "topspace X = topspace Y" shows "(\S. openin X S \ openin Y S) \ continuous_map Y X id" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" unfolding continuous_map_def using assms openin_subopen openin_subset by fastforce show "?rhs \ ?lhs" unfolding continuous_map_def using assms openin_subopen topspace_def by fastforce qed lemma continuous_map_const [simp]: "continuous_map X Y (\x. C) \ topspace X = {} \ C \ topspace Y" proof (cases "topspace X = {}") case False show ?thesis proof (cases "C \ topspace Y") case True with openin_subopen show ?thesis by (auto simp: continuous_map_def) next case False then show ?thesis unfolding continuous_map_def by fastforce qed qed (auto simp: continuous_map_on_empty) declare continuous_map_const [THEN iffD2, continuous_intros] lemma continuous_map_compose [continuous_intros]: assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" shows "continuous_map X X'' (g \ f)" unfolding continuous_map_def proof (intro conjI ballI allI impI) fix x assume "x \ topspace X" then show "(g \ f) x \ topspace X''" using assms unfolding continuous_map_def by force next fix U assume "openin X'' U" have eq: "{x \ topspace X. (g \ f) x \ U} = {x \ topspace X. f x \ {y. y \ topspace X' \ g y \ U}}" by auto (meson f continuous_map_def) show "openin X {x \ topspace X. (g \ f) x \ U}" unfolding eq using assms unfolding continuous_map_def using \openin X'' U\ by blast qed lemma continuous_map_eq: assumes "continuous_map X X' f" and "\x. x \ topspace X \ f x = g x" shows "continuous_map X X' g" proof - have eq: "{x \ topspace X. f x \ U} = {x \ topspace X. g x \ U}" for U using assms by auto show ?thesis using assms by (simp add: continuous_map_def eq) qed lemma restrict_continuous_map [simp]: "topspace X \ S \ continuous_map X X' (restrict f S) \ continuous_map X X' f" by (auto simp: elim!: continuous_map_eq) lemma continuous_map_in_subtopology: "continuous_map X (subtopology X' S) f \ continuous_map X X' f \ f ` (topspace X) \ S" (is "?lhs = ?rhs") proof assume L: ?lhs show ?rhs proof - have "\A. f ` (X closure_of A) \ subtopology X' S closure_of f ` A" by (meson L continuous_map_image_closure_subset) then show ?thesis by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset order.trans) qed next assume R: ?rhs then have eq: "{x \ topspace X. f x \ U} = {x \ topspace X. f x \ U \ f x \ S}" for U by auto show ?lhs using R unfolding continuous_map by (auto simp: openin_subtopology eq) qed lemma continuous_map_from_subtopology: "continuous_map X X' f \ continuous_map (subtopology X S) X' f" by (auto simp: continuous_map openin_subtopology) lemma continuous_map_into_fulltopology: "continuous_map X (subtopology X' T) f \ continuous_map X X' f" by (auto simp: continuous_map_in_subtopology) lemma continuous_map_into_subtopology: "\continuous_map X X' f; f ` topspace X \ T\ \ continuous_map X (subtopology X' T) f" by (auto simp: continuous_map_in_subtopology) lemma continuous_map_from_subtopology_mono: "\continuous_map (subtopology X T) X' f; S \ T\ \ continuous_map (subtopology X S) X' f" by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology) lemma continuous_map_from_discrete_topology [simp]: "continuous_map (discrete_topology U) X f \ f ` U \ topspace X" by (auto simp: continuous_map_def) lemma continuous_map_iff_continuous [simp]: "continuous_map (top_of_set S) euclidean g = continuous_on S g" by (fastforce simp add: continuous_map openin_subtopology continuous_on_open_invariant) lemma continuous_map_iff_continuous2 [simp]: "continuous_map euclidean euclidean g = continuous_on UNIV g" by (metis continuous_map_iff_continuous subtopology_UNIV) lemma continuous_map_openin_preimage_eq: "continuous_map X Y f \ f ` (topspace X) \ topspace Y \ (\U. openin Y U \ openin X (topspace X \ f -` U))" by (auto simp: continuous_map_def vimage_def Int_def) lemma continuous_map_closedin_preimage_eq: "continuous_map X Y f \ f ` (topspace X) \ topspace Y \ (\U. closedin Y U \ closedin X (topspace X \ f -` U))" by (auto simp: continuous_map_closedin vimage_def Int_def) lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt" by (simp add: continuous_at_imp_continuous_on isCont_real_sqrt) lemma continuous_map_sqrt [continuous_intros]: "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. sqrt(f x))" by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply) lemma continuous_map_id [simp, continuous_intros]: "continuous_map X X id" unfolding continuous_map_def using openin_subopen topspace_def by fastforce declare continuous_map_id [unfolded id_def, simp, continuous_intros] lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id" by (simp add: continuous_map_from_subtopology) declare continuous_map_id_subt [unfolded id_def, simp] lemma\<^marker>\tag important\ continuous_map_alt: "continuous_map T1 T2 f = ((\U. openin T2 U \ openin T1 (f -` U \ topspace T1)) \ f ` topspace T1 \ topspace T2)" by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute) lemma continuous_map_open [intro]: "continuous_map T1 T2 f \ openin T2 U \ openin T1 (f-`U \ topspace(T1))" unfolding continuous_map_alt by auto lemma continuous_map_preimage_topspace [intro]: assumes "continuous_map T1 T2 f" shows "f-`(topspace T2) \ topspace T1 = topspace T1" using assms unfolding continuous_map_def by auto subsection\Open and closed maps (not a priori assumed continuous)\ definition open_map :: "'a topology \ 'b topology \ ('a \ 'b) \ bool" where "open_map X1 X2 f \ \U. openin X1 U \ openin X2 (f ` U)" definition closed_map :: "'a topology \ 'b topology \ ('a \ 'b) \ bool" where "closed_map X1 X2 f \ \U. closedin X1 U \ closedin X2 (f ` U)" lemma open_map_imp_subset_topspace: "open_map X1 X2 f \ f ` (topspace X1) \ topspace X2" unfolding open_map_def by (simp add: openin_subset) lemma open_map_on_empty: "topspace X = {} \ open_map X Y f" by (metis empty_iff imageE in_mono open_map_def openin_subopen openin_subset) lemma closed_map_on_empty: "topspace X = {} \ closed_map X Y f" by (simp add: closed_map_def closedin_topspace_empty) lemma closed_map_const: "closed_map X Y (\x. c) \ topspace X = {} \ closedin Y {c}" by (metis closed_map_def closed_map_on_empty closedin_empty closedin_topspace image_constant_conv) lemma open_map_imp_subset: "\open_map X1 X2 f; S \ topspace X1\ \ f ` S \ topspace X2" by (meson order_trans open_map_imp_subset_topspace subset_image_iff) lemma topology_finer_open_id: "(\S. openin X S \ openin X' S) \ open_map X X' id" unfolding open_map_def by auto lemma open_map_id: "open_map X X id" unfolding open_map_def by auto lemma open_map_eq: "\open_map X X' f; \x. x \ topspace X \ f x = g x\ \ open_map X X' g" unfolding open_map_def by (metis image_cong openin_subset subset_iff) lemma open_map_inclusion_eq: "open_map (subtopology X S) X id \ openin X (topspace X \ S)" by (metis openin_topspace openin_trans_full subtopology_restrict topology_finer_open_id topspace_subtopology) lemma open_map_inclusion: "openin X S \ open_map (subtopology X S) X id" by (simp add: open_map_inclusion_eq openin_Int) lemma open_map_compose: "\open_map X X' f; open_map X' X'' g\ \ open_map X X'' (g \ f)" by (metis (no_types, lifting) image_comp open_map_def) lemma closed_map_imp_subset_topspace: "closed_map X1 X2 f \ f ` (topspace X1) \ topspace X2" by (simp add: closed_map_def closedin_subset) lemma closed_map_imp_subset: "\closed_map X1 X2 f; S \ topspace X1\ \ f ` S \ topspace X2" using closed_map_imp_subset_topspace by blast lemma topology_finer_closed_id: "(\S. closedin X S \ closedin X' S) \ closed_map X X' id" by (simp add: closed_map_def) lemma closed_map_id: "closed_map X X id" by (simp add: closed_map_def) lemma closed_map_eq: "\closed_map X X' f; \x. x \ topspace X \ f x = g x\ \ closed_map X X' g" unfolding closed_map_def by (metis image_cong closedin_subset subset_iff) lemma closed_map_compose: "\closed_map X X' f; closed_map X' X'' g\ \ closed_map X X'' (g \ f)" by (metis (no_types, lifting) closed_map_def image_comp) lemma closed_map_inclusion_eq: "closed_map (subtopology X S) X id \ closedin X (topspace X \ S)" proof - have *: "closedin X (T \ S)" if "closedin X (S \ topspace X)" "closedin X T" for T by (smt (verit, best) closedin_Int closure_of_subset_eq inf_sup_aci le_iff_inf that) then show ?thesis by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *) qed lemma closed_map_inclusion: "closedin X S \ closed_map (subtopology X S) X id" by (simp add: closed_map_inclusion_eq closedin_Int) lemma open_map_into_subtopology: "\open_map X X' f; f ` topspace X \ S\ \ open_map X (subtopology X' S) f" unfolding open_map_def openin_subtopology using openin_subset by fastforce lemma closed_map_into_subtopology: "\closed_map X X' f; f ` topspace X \ S\ \ closed_map X (subtopology X' S) f" unfolding closed_map_def closedin_subtopology using closedin_subset by fastforce lemma open_map_into_discrete_topology: "open_map X (discrete_topology U) f \ f ` (topspace X) \ U" unfolding open_map_def openin_discrete_topology using openin_subset by blast lemma closed_map_into_discrete_topology: "closed_map X (discrete_topology U) f \ f ` (topspace X) \ U" unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast lemma bijective_open_imp_closed_map: "\open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\ \ closed_map X X' f" unfolding open_map_def closed_map_def closedin_def by auto (metis Diff_subset inj_on_image_set_diff) lemma bijective_closed_imp_open_map: "\closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\ \ open_map X X' f" unfolding closed_map_def open_map_def openin_closedin_eq by auto (metis Diff_subset inj_on_image_set_diff) lemma open_map_from_subtopology: "\open_map X X' f; openin X U\ \ open_map (subtopology X U) X' f" unfolding open_map_def openin_subtopology_alt by blast lemma closed_map_from_subtopology: "\closed_map X X' f; closedin X U\ \ closed_map (subtopology X U) X' f" unfolding closed_map_def closedin_subtopology_alt by blast lemma open_map_restriction: assumes f: "open_map X X' f" and U: "{x \ topspace X. f x \ V} = U" shows "open_map (subtopology X U) (subtopology X' V) f" unfolding open_map_def proof clarsimp fix W assume "openin (subtopology X U) W" then obtain T where "openin X T" "W = T \ U" by (meson openin_subtopology) with f U have "f ` W = (f ` T) \ V" unfolding open_map_def openin_closedin_eq by auto then show "openin (subtopology X' V) (f ` W)" by (metis \openin X T\ f open_map_def openin_subtopology_Int) qed lemma closed_map_restriction: assumes f: "closed_map X X' f" and U: "{x \ topspace X. f x \ V} = U" shows "closed_map (subtopology X U) (subtopology X' V) f" unfolding closed_map_def proof clarsimp fix W assume "closedin (subtopology X U) W" then obtain T where "closedin X T" "W = T \ U" by (meson closedin_subtopology) with f U have "f ` W = (f ` T) \ V" unfolding closed_map_def closedin_def by auto then show "closedin (subtopology X' V) (f ` W)" by (metis \closedin X T\ closed_map_def closedin_subtopology f) qed lemma closed_map_closure_of_image: "closed_map X Y f \ f ` topspace X \ topspace Y \ (\S. S \ topspace X \ Y closure_of (f ` S) \ image f (X closure_of S))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (simp add: closed_map_def closed_map_imp_subset_topspace closure_of_minimal closure_of_subset image_mono) next assume ?rhs then show ?lhs by (metis closed_map_def closed_map_into_discrete_topology closure_of_eq closure_of_subset_eq topspace_discrete_topology) qed lemma open_map_interior_of_image_subset: "open_map X Y f \ (\S. image f (X interior_of S) \ Y interior_of (f ` S))" by (metis image_mono interior_of_eq interior_of_maximal interior_of_subset open_map_def openin_interior_of subset_antisym) lemma open_map_interior_of_image_subset_alt: "open_map X Y f \ (\S\topspace X. f ` (X interior_of S) \ Y interior_of f ` S)" by (metis interior_of_eq open_map_def open_map_interior_of_image_subset openin_subset subset_interior_of_eq) lemma open_map_interior_of_image_subset_gen: "open_map X Y f \ (f ` topspace X \ topspace Y \ (\S. f ` (X interior_of S) \ Y interior_of f ` S))" by (meson open_map_imp_subset_topspace open_map_interior_of_image_subset) lemma open_map_preimage_neighbourhood: "open_map X Y f \ (f ` topspace X \ topspace Y \ (\U T. closedin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U \ (\V. closedin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U)))" (is "?lhs=?rhs") proof assume L: ?lhs show ?rhs proof (intro conjI strip) show "f ` topspace X \ topspace Y" by (simp add: \open_map X Y f\ open_map_imp_subset_topspace) next fix U T assume UT: "closedin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U" have "closedin Y (topspace Y - f ` (topspace X - U))" by (meson UT L open_map_def openin_closedin_eq openin_diff openin_topspace) with UT show "\V. closedin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U" using image_iff by auto qed next assume R: ?rhs show ?lhs unfolding open_map_def proof (intro strip) fix U assume "openin X U" have "{x \ topspace X. f x \ topspace Y - f ` U} \ topspace X - U" by blast then obtain V where V: "closedin Y V" and sub: "topspace Y - f ` U \ V" "{x \ topspace X. f x \ V} \ topspace X - U" using R \openin X U\ by (meson Diff_subset openin_closedin_eq) then have "f ` U \ topspace Y - V" using R \openin X U\ openin_subset by fastforce with sub have "f ` U = topspace Y - V" by auto then show "openin Y (f ` U)" using V(1) by auto qed qed lemma closed_map_preimage_neighbourhood: "closed_map X Y f \ image f (topspace X) \ topspace Y \ (\U T. openin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U \ (\V. openin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U))" (is "?lhs=?rhs") proof assume L: ?lhs show ?rhs proof (intro conjI strip) show "f ` topspace X \ topspace Y" by (simp add: L closed_map_imp_subset_topspace) next fix U T assume UT: "openin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U" then have "openin Y (topspace Y - f ` (topspace X - U))" by (meson L closed_map_def closedin_def closedin_diff closedin_topspace) then show "\V. openin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U" using UT image_iff by auto qed next assume R: ?rhs show ?lhs unfolding closed_map_def proof (intro strip) fix U assume "closedin X U" have "{x \ topspace X. f x \ topspace Y - f ` U} \ topspace X - U" by blast then obtain V where V: "openin Y V" and sub: "topspace Y - f ` U \ V" "{x \ topspace X. f x \ V} \ topspace X - U" using R Diff_subset \closedin X U\ unfolding closedin_def by (smt (verit, ccfv_threshold) Collect_mem_eq Collect_mono_iff) then have "f ` U \ topspace Y - V" using R \closedin X U\ closedin_subset by fastforce with sub have "f ` U = topspace Y - V" by auto with V show "closedin Y (f ` U)" by auto qed qed lemma closed_map_fibre_neighbourhood: "closed_map X Y f \ f ` (topspace X) \ topspace Y \ (\U y. openin X U \ y \ topspace Y \ {x \ topspace X. f x = y} \ U \ (\V. openin Y V \ y \ V \ {x \ topspace X. f x \ V} \ U))" unfolding closed_map_preimage_neighbourhood proof (intro conj_cong refl all_cong1) fix U assume "f ` topspace X \ topspace Y" show "(\T. openin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U \ (\V. openin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U)) = (\y. openin X U \ y \ topspace Y \ {x \ topspace X. f x = y} \ U \ (\V. openin Y V \ y \ V \ {x \ topspace X. f x \ V} \ U))" (is "(\T. ?P T) \ (\y. ?Q y)") proof assume L [rule_format]: "\T. ?P T" show "\y. ?Q y" proof fix y show "?Q y" using L [of "{y}"] by blast qed next assume R: "\y. ?Q y" show "\T. ?P T" proof (cases "openin X U") case True note [[unify_search_bound=3]] obtain V where V: "\y. \y \ topspace Y; {x \ topspace X. f x = y} \ U\ \ openin Y (V y) \ y \ V y \ {x \ topspace X. f x \ V y} \ U" using R by (simp add: True) meson show ?thesis proof clarify fix T assume "openin X U" and "T \ topspace Y" and "{x \ topspace X. f x \ T} \ U" with V show "\V. openin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U" by (rule_tac x="\y\T. V y" in exI) fastforce qed qed auto qed qed lemma open_map_in_subtopology: "openin Y S \ (open_map X (subtopology Y S) f \ open_map X Y f \ f ` (topspace X) \ S)" by (metis le_inf_iff open_map_def open_map_imp_subset_topspace open_map_into_subtopology openin_trans_full topspace_subtopology) lemma open_map_from_open_subtopology: "\openin Y S; open_map X (subtopology Y S) f\ \ open_map X Y f" using open_map_in_subtopology by blast lemma closed_map_in_subtopology: "closedin Y S \ closed_map X (subtopology Y S) f \ (closed_map X Y f \ f ` topspace X \ S)" by (metis closed_map_def closed_map_imp_subset_topspace closed_map_into_subtopology closedin_closed_subtopology closedin_subset topspace_subtopology_subset) lemma closed_map_from_closed_subtopology: "\closedin Y S; closed_map X (subtopology Y S) f\ \ closed_map X Y f" using closed_map_in_subtopology by blast lemma closed_map_from_composition_left: assumes cmf: "closed_map X Z (g \ f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y" shows "closed_map Y Z g" unfolding closed_map_def proof (intro strip) fix U assume "closedin Y U" then have "closedin X {x \ topspace X. f x \ U}" using contf closedin_continuous_map_preimage by blast then have "closedin Z ((g \ f) ` {x \ topspace X. f x \ U})" using cmf closed_map_def by blast moreover have "\y. y \ U \ \x \ topspace X. f x \ U \ g y = g (f x)" by (smt (verit, ccfv_SIG) \closedin Y U\ closedin_subset fim image_iff subsetD) then have "(g \ f) ` {x \ topspace X. f x \ U} = g`U" by auto ultimately show "closedin Z (g ` U)" by metis qed text \identical proof as the above\ lemma open_map_from_composition_left: assumes cmf: "open_map X Z (g \ f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y" shows "open_map Y Z g" unfolding open_map_def proof (intro strip) fix U assume "openin Y U" then have "openin X {x \ topspace X. f x \ U}" using contf openin_continuous_map_preimage by blast then have "openin Z ((g \ f) ` {x \ topspace X. f x \ U})" using cmf open_map_def by blast moreover have "\y. y \ U \ \x \ topspace X. f x \ U \ g y = g (f x)" by (smt (verit, ccfv_SIG) \openin Y U\ openin_subset fim image_iff subsetD) then have "(g \ f) ` {x \ topspace X. f x \ U} = g`U" by auto ultimately show "openin Z (g ` U)" by metis qed lemma closed_map_from_composition_right: assumes cmf: "closed_map X Z (g \ f)" "f ` topspace X \ topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)" shows "closed_map X Y f" unfolding closed_map_def proof (intro strip) fix C assume "closedin X C" have "\y c. \y \ topspace Y; g y = g (f c); c \ C\ \ y \ f ` C" using \closedin X C\ assms closedin_subset inj_onD by fastforce then have "f ` C = {x \ topspace Y. g x \ (g \ f) ` C}" using \closedin X C\ assms(2) closedin_subset by fastforce moreover have "closedin Z ((g \ f) ` C)" using \closedin X C\ cmf closed_map_def by blast ultimately show "closedin Y (f ` C)" using assms(3) closedin_continuous_map_preimage by fastforce qed text \identical proof as the above\ lemma open_map_from_composition_right: assumes "open_map X Z (g \ f)" "f ` topspace X \ topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)" shows "open_map X Y f" unfolding open_map_def proof (intro strip) fix C assume "openin X C" have "\y c. \y \ topspace Y; g y = g (f c); c \ C\ \ y \ f ` C" using \openin X C\ assms openin_subset inj_onD by fastforce then have "f ` C = {x \ topspace Y. g x \ (g \ f) ` C}" using \openin X C\ assms(2) openin_subset by fastforce moreover have "openin Z ((g \ f) ` C)" using \openin X C\ assms(1) open_map_def by blast ultimately show "openin Y (f ` C)" using assms(3) openin_continuous_map_preimage by fastforce qed subsection\Quotient maps\ definition quotient_map where "quotient_map X X' f \ f ` (topspace X) = topspace X' \ (\U. U \ topspace X' \ (openin X {x. x \ topspace X \ f x \ U} \ openin X' U))" lemma quotient_map_eq: assumes "quotient_map X X' f" "\x. x \ topspace X \ f x = g x" shows "quotient_map X X' g" by (smt (verit) Collect_cong assms image_cong quotient_map_def) lemma quotient_map_compose: assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g" shows "quotient_map X X'' (g \ f)" unfolding quotient_map_def proof (intro conjI allI impI) show "(g \ f) ` topspace X = topspace X''" using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def) next fix U'' assume U'': "U'' \ topspace X''" define U' where "U' \ {y \ topspace X'. g y \ U''}" have "U' \ topspace X'" by (auto simp add: U'_def) then have U': "openin X {x \ topspace X. f x \ U'} = openin X' U'" using assms unfolding quotient_map_def by simp have "{x \ topspace X. f x \ topspace X' \ g (f x) \ U''} = {x \ topspace X. (g \ f) x \ U''}" using f quotient_map_def by fastforce then show "openin X {x \ topspace X. (g \ f) x \ U''} = openin X'' U''" by (smt (verit, best) Collect_cong U' U'_def U'' g mem_Collect_eq quotient_map_def) qed lemma quotient_map_from_composition: assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \ f)" shows "quotient_map X' X'' g" unfolding quotient_map_def proof (intro conjI allI impI) show "g ` topspace X' = topspace X''" using assms unfolding continuous_map_def quotient_map_def by fastforce next fix U'' :: "'c set" assume U'': "U'' \ topspace X''" have eq: "{x \ topspace X. g (f x) \ U''} = {x \ topspace X. f x \ {y. y \ topspace X' \ g y \ U''}}" using continuous_map_def f by fastforce show "openin X' {x \ topspace X'. g x \ U''} = openin X'' U''" using assms unfolding continuous_map_def quotient_map_def by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq) qed lemma quotient_imp_continuous_map: "quotient_map X X' f \ continuous_map X X' f" by (simp add: continuous_map openin_subset quotient_map_def) lemma quotient_imp_surjective_map: "quotient_map X X' f \ f ` (topspace X) = topspace X'" by (simp add: quotient_map_def) lemma quotient_map_closedin: "quotient_map X X' f \ f ` (topspace X) = topspace X' \ (\U. U \ topspace X' \ (closedin X {x. x \ topspace X \ f x \ U} \ closedin X' U))" proof - have eq: "(topspace X - {x \ topspace X. f x \ U'}) = {x \ topspace X. f x \ topspace X' \ f x \ U'}" if "f ` topspace X = topspace X'" "U' \ topspace X'" for U' using that by auto have "(\U\topspace X'. openin X {x \ topspace X. f x \ U} = openin X' U) = (\U\topspace X'. closedin X {x \ topspace X. f x \ U} = closedin X' U)" if "f ` topspace X = topspace X'" proof (rule iffI; intro allI impI subsetI) fix U' assume *[rule_format]: "\U\topspace X'. openin X {x \ topspace X. f x \ U} = openin X' U" and U': "U' \ topspace X'" show "closedin X {x \ topspace X. f x \ U'} = closedin X' U'" using U' by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that]) next fix U' :: "'b set" assume *[rule_format]: "\U\topspace X'. closedin X {x \ topspace X. f x \ U} = closedin X' U" and U': "U' \ topspace X'" show "openin X {x \ topspace X. f x \ U'} = openin X' U'" using U' by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that]) qed then show ?thesis unfolding quotient_map_def by force qed lemma continuous_open_imp_quotient_map: assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'" shows "quotient_map X X' f" proof - { fix U assume U: "U \ topspace X'" and "openin X {x \ topspace X. f x \ U}" then have ope: "openin X' (f ` {x \ topspace X. f x \ U})" using om unfolding open_map_def by blast then have "openin X' U" using U feq by (subst openin_subopen) force } moreover have "openin X {x \ topspace X. f x \ U}" if "U \ topspace X'" and "openin X' U" for U using that assms unfolding continuous_map_def by blast ultimately show ?thesis unfolding quotient_map_def using assms by blast qed lemma continuous_closed_imp_quotient_map: assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'" shows "quotient_map X X' f" proof - have "f ` {x \ topspace X. f x \ U} = U" if "U \ topspace X'" for U using that feq by auto with assms show ?thesis unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto qed lemma continuous_open_quotient_map: "\continuous_map X X' f; open_map X X' f\ \ quotient_map X X' f \ f ` (topspace X) = topspace X'" by (meson continuous_open_imp_quotient_map quotient_map_def) lemma continuous_closed_quotient_map: "\continuous_map X X' f; closed_map X X' f\ \ quotient_map X X' f \ f ` (topspace X) = topspace X'" by (meson continuous_closed_imp_quotient_map quotient_map_def) lemma injective_quotient_map: assumes "inj_on f (topspace X)" shows "quotient_map X X' f \ continuous_map X X' f \ open_map X X' f \ closed_map X X' f \ f ` (topspace X) = topspace X'" (is "?lhs = ?rhs") proof assume L: ?lhs have om: "open_map X X' f" proof (clarsimp simp add: open_map_def) fix U assume "openin X U" then have "U \ topspace X" by (simp add: openin_subset) moreover have "{x \ topspace X. f x \ f ` U} = U" using \U \ topspace X\ assms inj_onD by fastforce ultimately show "openin X' (f ` U)" using L unfolding quotient_map_def by (metis (no_types, lifting) Collect_cong \openin X U\ image_mono) qed then have "closed_map X X' f" by (simp add: L assms bijective_open_imp_closed_map quotient_imp_surjective_map) then show ?rhs using L om by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map) next assume ?rhs then show ?lhs by (simp add: continuous_closed_imp_quotient_map) qed lemma continuous_compose_quotient_map: assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \ f)" shows "continuous_map X' X'' g" unfolding quotient_map_def continuous_map_def proof (intro conjI ballI allI impI) show "\x'. x' \ topspace X' \ g x' \ topspace X''" using assms unfolding quotient_map_def by (metis (no_types, opaque_lifting) continuous_map_image_subset_topspace image_comp image_subset_iff) next fix U'' :: "'c set" assume U'': "openin X'' U''" have "f ` topspace X = topspace X'" by (simp add: f quotient_imp_surjective_map) then have eq: "{x \ topspace X. f x \ topspace X' \ g (f x) \ U} = {x \ topspace X. g (f x) \ U}" for U by auto have "openin X {x \ topspace X. f x \ topspace X' \ g (f x) \ U''}" unfolding eq using U'' g openin_continuous_map_preimage by fastforce then have *: "openin X {x \ topspace X. f x \ {x \ topspace X'. g x \ U''}}" by auto show "openin X' {x \ topspace X'. g x \ U''}" using f unfolding quotient_map_def by (metis (no_types) Collect_subset *) qed lemma continuous_compose_quotient_map_eq: "quotient_map X X' f \ continuous_map X X'' (g \ f) \ continuous_map X' X'' g" using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast lemma quotient_map_compose_eq: "quotient_map X X' f \ quotient_map X X'' (g \ f) \ quotient_map X' X'' g" by (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_compose quotient_map_from_composition) lemma quotient_map_restriction: assumes quo: "quotient_map X Y f" and U: "{x \ topspace X. f x \ V} = U" and disj: "openin Y V \ closedin Y V" shows "quotient_map (subtopology X U) (subtopology Y V) f" using disj proof assume V: "openin Y V" with U have sub: "U \ topspace X" "V \ topspace Y" by (auto simp: openin_subset) have fim: "f ` topspace X = topspace Y" and Y: "\U. U \ topspace Y \ openin X {x \ topspace X. f x \ U} = openin Y U" using quo unfolding quotient_map_def by auto have "openin X U" using U V Y sub(2) by blast show ?thesis unfolding quotient_map_def proof (intro conjI allI impI) show "f ` topspace (subtopology X U) = topspace (subtopology Y V)" using sub U fim by (auto) next fix Y' :: "'b set" assume "Y' \ topspace (subtopology Y V)" then have "Y' \ topspace Y" "Y' \ V" by (simp_all) then have eq: "{x \ topspace X. x \ U \ f x \ Y'} = {x \ topspace X. f x \ Y'}" using U by blast then show "openin (subtopology X U) {x \ topspace (subtopology X U). f x \ Y'} = openin (subtopology Y V) Y'" using U V Y \openin X U\ \Y' \ topspace Y\ \Y' \ V\ by (simp add: openin_open_subtopology eq) (auto simp: openin_closedin_eq) qed next assume V: "closedin Y V" with U have sub: "U \ topspace X" "V \ topspace Y" by (auto simp: closedin_subset) have fim: "f ` topspace X = topspace Y" and Y: "\U. U \ topspace Y \ closedin X {x \ topspace X. f x \ U} = closedin Y U" using quo unfolding quotient_map_closedin by auto have "closedin X U" using U V Y sub(2) by blast show ?thesis unfolding quotient_map_closedin proof (intro conjI allI impI) show "f ` topspace (subtopology X U) = topspace (subtopology Y V)" using sub U fim by (auto) next fix Y' :: "'b set" assume "Y' \ topspace (subtopology Y V)" then have "Y' \ topspace Y" "Y' \ V" by (simp_all) then have eq: "{x \ topspace X. x \ U \ f x \ Y'} = {x \ topspace X. f x \ Y'}" using U by blast then show "closedin (subtopology X U) {x \ topspace (subtopology X U). f x \ Y'} = closedin (subtopology Y V) Y'" using U V Y \closedin X U\ \Y' \ topspace Y\ \Y' \ V\ by (simp add: closedin_closed_subtopology eq) (auto simp: closedin_def) qed qed lemma quotient_map_saturated_open: "quotient_map X Y f \ continuous_map X Y f \ f ` (topspace X) = topspace Y \ (\U. openin X U \ {x \ topspace X. f x \ f ` U} \ U \ openin Y (f ` U))" (is "?lhs = ?rhs") proof assume L: ?lhs then have fim: "f ` topspace X = topspace Y" and Y: "\U. U \ topspace Y \ openin Y U = openin X {x \ topspace X. f x \ U}" unfolding quotient_map_def by auto show ?rhs proof (intro conjI allI impI) show "continuous_map X Y f" by (simp add: L quotient_imp_continuous_map) show "f ` topspace X = topspace Y" by (simp add: fim) next fix U :: "'a set" assume U: "openin X U \ {x \ topspace X. f x \ f ` U} \ U" then have sub: "f ` U \ topspace Y" and eq: "{x \ topspace X. f x \ f ` U} = U" using fim openin_subset by fastforce+ show "openin Y (f ` U)" by (simp add: sub Y eq U) qed next assume ?rhs then have YX: "\U. openin Y U \ openin X {x \ topspace X. f x \ U}" and fim: "f ` topspace X = topspace Y" and XY: "\U. \openin X U; {x \ topspace X. f x \ f ` U} \ U\ \ openin Y (f ` U)" by (auto simp: quotient_map_def continuous_map_def) show ?lhs proof (simp add: quotient_map_def fim, intro allI impI iffI) fix U :: "'b set" assume "U \ topspace Y" and X: "openin X {x \ topspace X. f x \ U}" have feq: "f ` {x \ topspace X. f x \ U} = U" using \U \ topspace Y\ fim by auto show "openin Y U" using XY [OF X] by (simp add: feq) next fix U :: "'b set" assume "U \ topspace Y" and Y: "openin Y U" show "openin X {x \ topspace X. f x \ U}" by (metis YX [OF Y]) qed qed lemma quotient_map_saturated_closed: "quotient_map X Y f \ continuous_map X Y f \ f ` (topspace X) = topspace Y \ (\U. closedin X U \ {x \ topspace X. f x \ f ` U} \ U \ closedin Y (f ` U))" (is "?lhs = ?rhs") proof assume L: ?lhs then obtain fim: "f ` topspace X = topspace Y" and Y: "\U. U \ topspace Y \ closedin Y U = closedin X {x \ topspace X. f x \ U}" by (simp add: quotient_map_closedin) show ?rhs proof (intro conjI allI impI) show "continuous_map X Y f" by (simp add: L quotient_imp_continuous_map) show "f ` topspace X = topspace Y" by (simp add: fim) next fix U :: "'a set" assume U: "closedin X U \ {x \ topspace X. f x \ f ` U} \ U" then have sub: "f ` U \ topspace Y" and eq: "{x \ topspace X. f x \ f ` U} = U" using fim closedin_subset by fastforce+ show "closedin Y (f ` U)" by (simp add: sub Y eq U) qed next assume ?rhs then obtain YX: "\U. closedin Y U \ closedin X {x \ topspace X. f x \ U}" and fim: "f ` topspace X = topspace Y" and XY: "\U. \closedin X U; {x \ topspace X. f x \ f ` U} \ U\ \ closedin Y (f ` U)" by (simp add: continuous_map_closedin) show ?lhs proof (simp add: quotient_map_closedin fim, intro allI impI iffI) fix U :: "'b set" assume "U \ topspace Y" and X: "closedin X {x \ topspace X. f x \ U}" have feq: "f ` {x \ topspace X. f x \ U} = U" using \U \ topspace Y\ fim by auto show "closedin Y U" using XY [OF X] by (simp add: feq) next fix U :: "'b set" assume "U \ topspace Y" and Y: "closedin Y U" show "closedin X {x \ topspace X. f x \ U}" by (metis YX [OF Y]) qed qed lemma quotient_map_onto_image: assumes "f ` topspace X \ topspace Y" and U: "\U. U \ topspace Y \ openin X {x \ topspace X. f x \ U} = openin Y U" shows "quotient_map X (subtopology Y (f ` topspace X)) f" unfolding quotient_map_def topspace_subtopology proof (intro conjI strip) fix U assume "U \ topspace Y \ f ` topspace X" with U have "openin X {x \ topspace X. f x \ U} \ \x. openin Y x \ U = f ` topspace X \ x" by fastforce moreover have "\x. openin Y x \ U = f ` topspace X \ x \ openin X {x \ topspace X. f x \ U}" by (metis (mono_tags, lifting) Collect_cong IntE IntI U image_eqI openin_subset) ultimately show "openin X {x \ topspace X. f x \ U} = openin (subtopology Y (f ` topspace X)) U" by (force simp: openin_subtopology_alt image_iff) qed (use assms in auto) lemma quotient_map_lift_exists: assumes f: "quotient_map X Y f" and h: "continuous_map X Z h" and "\x y. \x \ topspace X; y \ topspace X; f x = f y\ \ h x = h y" obtains g where "continuous_map Y Z g" "g ` topspace Y = h ` topspace X" "\x. x \ topspace X \ g(f x) = h x" proof - obtain g where g: "\x. x \ topspace X \ h x = g(f x)" using function_factors_left_gen[of "\x. x \ topspace X" f h] assms by blast show ?thesis proof show "g ` topspace Y = h ` topspace X" using f g by (force dest!: quotient_imp_surjective_map) show "continuous_map Y Z g" by (smt (verit) f g h continuous_compose_quotient_map_eq continuous_map_eq o_def) qed (simp add: g) qed subsection\ Separated Sets\ definition separatedin :: "'a topology \ 'a set \ 'a set \ bool" where "separatedin X S T \ S \ topspace X \ T \ topspace X \ S \ X closure_of T = {} \ T \ X closure_of S = {}" lemma separatedin_empty [simp]: "separatedin X S {} \ S \ topspace X" "separatedin X {} S \ S \ topspace X" by (simp_all add: separatedin_def) lemma separatedin_refl [simp]: "separatedin X S S \ S = {}" by (metis closure_of_subset empty_subsetI inf.orderE separatedin_def) lemma separatedin_sym: "separatedin X S T \ separatedin X T S" by (auto simp: separatedin_def) lemma separatedin_imp_disjoint: "separatedin X S T \ disjnt S T" by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def) lemma separatedin_mono: "\separatedin X S T; S' \ S; T' \ T\ \ separatedin X S' T'" unfolding separatedin_def using closure_of_mono by blast lemma separatedin_open_sets: "\openin X S; openin X T\ \ separatedin X S T \ disjnt S T" unfolding disjnt_def separatedin_def by (auto simp: openin_Int_closure_of_eq_empty openin_subset) lemma separatedin_closed_sets: "\closedin X S; closedin X T\ \ separatedin X S T \ disjnt S T" unfolding closure_of_eq disjnt_def separatedin_def by (metis closedin_def closure_of_eq inf_commute) lemma separatedin_subtopology: "separatedin (subtopology X U) S T \ S \ U \ T \ U \ separatedin X S T" by (auto simp: separatedin_def closure_of_subtopology Int_ac disjoint_iff elim!: inf.orderE) lemma separatedin_discrete_topology: "separatedin (discrete_topology U) S T \ S \ U \ T \ U \ disjnt S T" by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology) lemma separated_eq_distinguishable: "separatedin X {x} {y} \ x \ topspace X \ y \ topspace X \ (\U. openin X U \ x \ U \ (y \ U)) \ (\v. openin X v \ y \ v \ (x \ v))" by (force simp: separatedin_def closure_of_def) lemma separatedin_Un [simp]: "separatedin X S (T \ U) \ separatedin X S T \ separatedin X S U" "separatedin X (S \ T) U \ separatedin X S U \ separatedin X T U" by (auto simp: separatedin_def) lemma separatedin_Union: "finite \ \ separatedin X S (\\) \ S \ topspace X \ (\T \ \. separatedin X S T)" "finite \ \ separatedin X (\\) S \ (\T \ \. separatedin X S T) \ S \ topspace X" by (auto simp: separatedin_def closure_of_Union) lemma separatedin_openin_diff: "\openin X S; openin X T\ \ separatedin X (S - T) (T - S)" unfolding separatedin_def by (metis Diff_Int_distrib2 Diff_disjoint Diff_empty Diff_mono empty_Diff empty_subsetI openin_Int_closure_of_eq_empty openin_subset) lemma separatedin_closedin_diff: assumes "closedin X S" "closedin X T" shows "separatedin X (S - T) (T - S)" proof - have "S - T \ topspace X" "T - S \ topspace X" using assms closedin_subset by auto with assms show ?thesis by (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2) qed lemma separation_closedin_Un_gen: "separatedin X S T \ S \ topspace X \ T \ topspace X \ disjnt S T \ closedin (subtopology X (S \ T)) S \ closedin (subtopology X (S \ T)) T" by (auto simp add: separatedin_def closedin_Int_closure_of disjnt_iff dest: closure_of_subset) lemma separation_openin_Un_gen: "separatedin X S T \ S \ topspace X \ T \ topspace X \ disjnt S T \ openin (subtopology X (S \ T)) S \ openin (subtopology X (S \ T)) T" unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def) lemma separatedin_full: "S \ T = topspace X \ separatedin X S T \ disjnt S T \ closedin X S \ openin X S \ closedin X T \ openin X T" by (metis separatedin_open_sets separation_closedin_Un_gen separation_openin_Un_gen subtopology_topspace) subsection\Homeomorphisms\ text\(1-way and 2-way versions may be useful in places)\ definition homeomorphic_map :: "'a topology \ 'b topology \ ('a \ 'b) \ bool" where "homeomorphic_map X Y f \ quotient_map X Y f \ inj_on f (topspace X)" definition homeomorphic_maps :: "'a topology \ 'b topology \ ('a \ 'b) \ ('b \ 'a) \ bool" where "homeomorphic_maps X Y f g \ continuous_map X Y f \ continuous_map Y X g \ (\x \ topspace X. g(f x) = x) \ (\y \ topspace Y. f(g y) = y)" lemma homeomorphic_map_eq: "\homeomorphic_map X Y f; \x. x \ topspace X \ f x = g x\ \ homeomorphic_map X Y g" by (meson homeomorphic_map_def inj_on_cong quotient_map_eq) lemma homeomorphic_maps_eq: "\homeomorphic_maps X Y f g; \x. x \ topspace X \ f x = f' x; \y. y \ topspace Y \ g y = g' y\ \ homeomorphic_maps X Y f' g'" unfolding homeomorphic_maps_def by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff) lemma homeomorphic_maps_sym: "homeomorphic_maps X Y f g \ homeomorphic_maps Y X g f" by (auto simp: homeomorphic_maps_def) lemma homeomorphic_maps_id: "homeomorphic_maps X Y id id \ Y = X" (is "?lhs = ?rhs") proof assume L: ?lhs then have "topspace X = topspace Y" by (auto simp: homeomorphic_maps_def continuous_map_def) with L show ?rhs unfolding homeomorphic_maps_def by (metis topology_finer_continuous_id topology_eq) next assume ?rhs then show ?lhs unfolding homeomorphic_maps_def by auto qed lemma homeomorphic_map_id [simp]: "homeomorphic_map X Y id \ Y = X" (is "?lhs = ?rhs") proof assume L: ?lhs then have eq: "topspace X = topspace Y" by (auto simp: homeomorphic_map_def continuous_map_def quotient_map_def) then have "\S. openin X S \ openin Y S" by (meson L homeomorphic_map_def injective_quotient_map topology_finer_open_id) then show ?rhs using L unfolding homeomorphic_map_def by (metis eq quotient_imp_continuous_map topology_eq topology_finer_continuous_id) next assume ?rhs then show ?lhs unfolding homeomorphic_map_def by (simp add: closed_map_id continuous_closed_imp_quotient_map) qed lemma homeomorphic_map_compose: assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g" shows "homeomorphic_map X X'' (g \ f)" proof - have "inj_on g (f ` topspace X)" by (metis (no_types) assms homeomorphic_map_def quotient_imp_surjective_map) then show ?thesis using assms by (meson comp_inj_on homeomorphic_map_def quotient_map_compose_eq) qed lemma homeomorphic_maps_compose: "homeomorphic_maps X Y f h \ homeomorphic_maps Y X'' g k \ homeomorphic_maps X X'' (g \ f) (h \ k)" unfolding homeomorphic_maps_def by (auto simp: continuous_map_compose; simp add: continuous_map_def) lemma homeomorphic_eq_everything_map: "homeomorphic_map X Y f \ continuous_map X Y f \ open_map X Y f \ closed_map X Y f \ f ` (topspace X) = topspace Y \ inj_on f (topspace X)" unfolding homeomorphic_map_def by (force simp: injective_quotient_map intro: injective_quotient_map) lemma homeomorphic_imp_continuous_map: "homeomorphic_map X Y f \ continuous_map X Y f" by (simp add: homeomorphic_eq_everything_map) lemma homeomorphic_imp_open_map: "homeomorphic_map X Y f \ open_map X Y f" by (simp add: homeomorphic_eq_everything_map) lemma homeomorphic_imp_closed_map: "homeomorphic_map X Y f \ closed_map X Y f" by (simp add: homeomorphic_eq_everything_map) lemma homeomorphic_imp_surjective_map: "homeomorphic_map X Y f \ f ` (topspace X) = topspace Y" by (simp add: homeomorphic_eq_everything_map) lemma homeomorphic_imp_injective_map: "homeomorphic_map X Y f \ inj_on f (topspace X)" by (simp add: homeomorphic_eq_everything_map) lemma bijective_open_imp_homeomorphic_map: "\continuous_map X Y f; open_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\ \ homeomorphic_map X Y f" by (simp add: homeomorphic_map_def continuous_open_imp_quotient_map) lemma bijective_closed_imp_homeomorphic_map: "\continuous_map X Y f; closed_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\ \ homeomorphic_map X Y f" by (simp add: continuous_closed_quotient_map homeomorphic_map_def) lemma open_eq_continuous_inverse_map: assumes X: "\x. x \ topspace X \ f x \ topspace Y \ g(f x) = x" and Y: "\y. y \ topspace Y \ g y \ topspace X \ f(g y) = y" shows "open_map X Y f \ continuous_map Y X g" proof - have eq: "{x \ topspace Y. g x \ U} = f ` U" if "openin X U" for U using openin_subset [OF that] by (force simp: X Y image_iff) show ?thesis by (auto simp: Y open_map_def continuous_map_def eq) qed lemma closed_eq_continuous_inverse_map: assumes X: "\x. x \ topspace X \ f x \ topspace Y \ g(f x) = x" and Y: "\y. y \ topspace Y \ g y \ topspace X \ f(g y) = y" shows "closed_map X Y f \ continuous_map Y X g" proof - have eq: "{x \ topspace Y. g x \ U} = f ` U" if "closedin X U" for U using closedin_subset [OF that] by (force simp: X Y image_iff) show ?thesis by (auto simp: Y closed_map_def continuous_map_closedin eq) qed lemma homeomorphic_maps_map: "homeomorphic_maps X Y f g \ homeomorphic_map X Y f \ homeomorphic_map Y X g \ (\x \ topspace X. g(f x) = x) \ (\y \ topspace Y. f(g y) = y)" (is "?lhs = ?rhs") proof assume ?lhs then have L: "continuous_map X Y f" "continuous_map Y X g" "\x\topspace X. g (f x) = x" "\x'\topspace Y. f (g x') = x'" by (auto simp: homeomorphic_maps_def) show ?rhs proof (intro conjI bijective_open_imp_homeomorphic_map L) show "open_map X Y f" using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def) show "open_map Y X g" using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def) show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X" using L by (force simp: continuous_map_closedin)+ show "inj_on f (topspace X)" "inj_on g (topspace Y)" using L unfolding inj_on_def by metis+ qed next assume ?rhs then show ?lhs by (auto simp: homeomorphic_maps_def homeomorphic_imp_continuous_map) qed lemma homeomorphic_maps_imp_map: "homeomorphic_maps X Y f g \ homeomorphic_map X Y f" using homeomorphic_maps_map by blast lemma homeomorphic_map_maps: "homeomorphic_map X Y f \ (\g. homeomorphic_maps X Y f g)" (is "?lhs = ?rhs") proof assume ?lhs then have L: "continuous_map X Y f" "open_map X Y f" "closed_map X Y f" "f ` (topspace X) = topspace Y" "inj_on f (topspace X)" by (auto simp: homeomorphic_eq_everything_map) have X: "\x. x \ topspace X \ f x \ topspace Y \ inv_into (topspace X) f (f x) = x" using L by auto have Y: "\y. y \ topspace Y \ inv_into (topspace X) f y \ topspace X \ f (inv_into (topspace X) f y) = y" by (simp add: L f_inv_into_f inv_into_into) have "homeomorphic_maps X Y f (inv_into (topspace X) f)" unfolding homeomorphic_maps_def proof (intro conjI L) show "continuous_map Y X (inv_into (topspace X) f)" by (simp add: L X Y flip: open_eq_continuous_inverse_map [where f=f]) next show "\x\topspace X. inv_into (topspace X) f (f x) = x" "\y\topspace Y. f (inv_into (topspace X) f y) = y" using X Y by auto qed then show ?rhs by metis next assume ?rhs then show ?lhs using homeomorphic_maps_map by blast qed lemma homeomorphic_maps_involution: "\continuous_map X X f; \x. x \ topspace X \ f(f x) = x\ \ homeomorphic_maps X X f f" by (auto simp: homeomorphic_maps_def) lemma homeomorphic_map_involution: "\continuous_map X X f; \x. x \ topspace X \ f(f x) = x\ \ homeomorphic_map X X f" using homeomorphic_maps_involution homeomorphic_maps_map by blast lemma homeomorphic_map_openness: assumes hom: "homeomorphic_map X Y f" and U: "U \ topspace X" shows "openin Y (f ` U) \ openin X U" proof - obtain g where "homeomorphic_maps X Y f g" using assms by (auto simp: homeomorphic_map_maps) then have g: "homeomorphic_map Y X g" and gf: "\x. x \ topspace X \ g(f x) = x" by (auto simp: homeomorphic_maps_map) then have "openin X U \ openin Y (f ` U)" using hom homeomorphic_imp_open_map open_map_def by blast show "openin Y (f ` U) = openin X U" proof assume L: "openin Y (f ` U)" have "U = g ` (f ` U)" using U gf by force then show "openin X U" by (metis L homeomorphic_imp_open_map open_map_def g) next assume "openin X U" then show "openin Y (f ` U)" using hom homeomorphic_imp_open_map open_map_def by blast qed qed lemma homeomorphic_map_closedness: assumes hom: "homeomorphic_map X Y f" and U: "U \ topspace X" shows "closedin Y (f ` U) \ closedin X U" proof - obtain g where "homeomorphic_maps X Y f g" using assms by (auto simp: homeomorphic_map_maps) then have g: "homeomorphic_map Y X g" and gf: "\x. x \ topspace X \ g(f x) = x" by (auto simp: homeomorphic_maps_map) then have "closedin X U \ closedin Y (f ` U)" using hom homeomorphic_imp_closed_map closed_map_def by blast show "closedin Y (f ` U) = closedin X U" proof assume L: "closedin Y (f ` U)" have "U = g ` (f ` U)" using U gf by force then show "closedin X U" by (metis L homeomorphic_imp_closed_map closed_map_def g) next assume "closedin X U" then show "closedin Y (f ` U)" using hom homeomorphic_imp_closed_map closed_map_def by blast qed qed lemma homeomorphic_map_openness_eq: "homeomorphic_map X Y f \ openin X U \ U \ topspace X \ openin Y (f ` U)" by (meson homeomorphic_map_openness openin_closedin_eq) lemma homeomorphic_map_closedness_eq: "homeomorphic_map X Y f \ closedin X U \ U \ topspace X \ closedin Y (f ` U)" by (meson closedin_subset homeomorphic_map_closedness) lemma all_openin_homeomorphic_image: assumes "homeomorphic_map X Y f" shows "(\V. openin Y V \ P V) \ (\U. openin X U \ P(f ` U))" by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff) lemma all_closedin_homeomorphic_image: assumes "homeomorphic_map X Y f" shows "(\V. closedin Y V \ P V) \ (\U. closedin X U \ P(f ` U))" (is "?lhs = ?rhs") by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff) lemma homeomorphic_map_derived_set_of: assumes hom: "homeomorphic_map X Y f" and S: "S \ topspace X" shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)" proof - have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)" using hom by (auto simp: homeomorphic_eq_everything_map) have iff: "(\T. x \ T \ openin X T \ (\y. y \ x \ y \ S \ y \ T)) = (\T. T \ topspace Y \ f x \ T \ openin Y T \ (\y. y \ f x \ y \ f ` S \ y \ T))" if "x \ topspace X" for x proof - have \
: "(x \ T \ openin X T) = (T \ topspace X \ f x \ f ` T \ openin Y (f ` T))" for T by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that) moreover have "(\y. y \ x \ y \ S \ y \ T) = (\y. y \ f x \ y \ f ` S \ y \ f ` T)" (is "?lhs = ?rhs") if "T \ topspace X \ f x \ f ` T \ openin Y (f ` T)" for T by (smt (verit, del_insts) S \x \ topspace X\ image_iff inj inj_on_def subsetD that) ultimately show ?thesis by (auto simp flip: fim simp: all_subset_image) qed have *: "\T = f ` S; \x. x \ S \ P x \ Q(f x)\ \ {y. y \ T \ Q y} = f ` {x \ S. P x}" for T S P Q by auto show ?thesis unfolding derived_set_of_def by (rule *) (use fim iff openin_subset in force)+ qed lemma homeomorphic_map_closure_of: assumes hom: "homeomorphic_map X Y f" and S: "S \ topspace X" shows "Y closure_of (f ` S) = f ` (X closure_of S)" unfolding closure_of using homeomorphic_imp_surjective_map [OF hom] S by (auto simp: in_derived_set_of homeomorphic_map_derived_set_of [OF assms]) lemma homeomorphic_map_interior_of: assumes hom: "homeomorphic_map X Y f" and S: "S \ topspace X" shows "Y interior_of (f ` S) = f ` (X interior_of S)" proof - { fix y assume "y \ topspace Y" and "y \ Y closure_of (topspace Y - f ` S)" then have "y \ f ` (topspace X - X closure_of (topspace X - S))" using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom] by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) } moreover { fix x assume "x \ topspace X" then have "f x \ topspace Y" using hom homeomorphic_imp_surjective_map by blast } moreover { fix x assume "x \ topspace X" and "x \ X closure_of (topspace X - S)" and "f x \ Y closure_of (topspace Y - f ` S)" then have "False" using homeomorphic_map_closure_of [OF hom] hom unfolding homeomorphic_eq_everything_map by (metis Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff inj_on_image_set_diff) } ultimately show ?thesis by (auto simp: interior_of_closure_of) qed lemma homeomorphic_map_frontier_of: assumes hom: "homeomorphic_map X Y f" and S: "S \ topspace X" shows "Y frontier_of (f ` S) = f ` (X frontier_of S)" unfolding frontier_of_def proof (intro equalityI subsetI DiffI) fix y assume "y \ Y closure_of f ` S - Y interior_of f ` S" then show "y \ f ` (X closure_of S - X interior_of S)" using S hom homeomorphic_map_closure_of homeomorphic_map_interior_of by fastforce next fix y assume "y \ f ` (X closure_of S - X interior_of S)" then show "y \ Y closure_of f ` S" using S hom homeomorphic_map_closure_of by fastforce next fix x assume "x \ f ` (X closure_of S - X interior_of S)" then obtain y where y: "x = f y" "y \ X closure_of S" "y \ X interior_of S" by blast then show "x \ Y interior_of f ` S" using S hom homeomorphic_map_interior_of y(1) unfolding homeomorphic_map_def by (smt (verit, ccfv_SIG) in_closure_of inj_on_image_mem_iff interior_of_subset_topspace) qed lemma homeomorphic_maps_subtopologies: "\homeomorphic_maps X Y f g; f ` (topspace X \ S) = topspace Y \ T\ \ homeomorphic_maps (subtopology X S) (subtopology Y T) f g" unfolding homeomorphic_maps_def by (force simp: continuous_map_from_subtopology continuous_map_in_subtopology) lemma homeomorphic_maps_subtopologies_alt: "\homeomorphic_maps X Y f g; f ` (topspace X \ S) \ T; g ` (topspace Y \ T) \ S\ \ homeomorphic_maps (subtopology X S) (subtopology Y T) f g" unfolding homeomorphic_maps_def by (force simp: continuous_map_from_subtopology continuous_map_in_subtopology) lemma homeomorphic_map_subtopologies: "\homeomorphic_map X Y f; f ` (topspace X \ S) = topspace Y \ T\ \ homeomorphic_map (subtopology X S) (subtopology Y T) f" by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies) lemma homeomorphic_map_subtopologies_alt: assumes hom: "homeomorphic_map X Y f" and S: "\x. \x \ topspace X; f x \ topspace Y\ \ f x \ T \ x \ S" shows "homeomorphic_map (subtopology X S) (subtopology Y T) f" proof - have "homeomorphic_maps (subtopology X S) (subtopology Y T) f g" if "homeomorphic_maps X Y f g" for g proof (rule homeomorphic_maps_subtopologies [OF that]) have "f ` (topspace X \ S) \ topspace Y \ T" using S hom homeomorphic_imp_surjective_map by fastforce then show "f ` (topspace X \ S) = topspace Y \ T" using that unfolding homeomorphic_maps_def continuous_map_def by (smt (verit, del_insts) Int_iff S image_iff subsetI subset_antisym) qed then show ?thesis using hom by (meson homeomorphic_map_maps) qed subsection\Relation of homeomorphism between topological spaces\ definition homeomorphic_space (infixr "homeomorphic'_space" 50) where "X homeomorphic_space Y \ \f g. homeomorphic_maps X Y f g" lemma homeomorphic_space_refl: "X homeomorphic_space X" by (meson homeomorphic_maps_id homeomorphic_space_def) lemma homeomorphic_space_sym: "X homeomorphic_space Y \ Y homeomorphic_space X" unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym) lemma homeomorphic_space_trans [trans]: "\X1 homeomorphic_space X2; X2 homeomorphic_space X3\ \ X1 homeomorphic_space X3" unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose) lemma homeomorphic_space: "X homeomorphic_space Y \ (\f. homeomorphic_map X Y f)" by (simp add: homeomorphic_map_maps homeomorphic_space_def) lemma homeomorphic_maps_imp_homeomorphic_space: "homeomorphic_maps X Y f g \ X homeomorphic_space Y" unfolding homeomorphic_space_def by metis lemma homeomorphic_map_imp_homeomorphic_space: "homeomorphic_map X Y f \ X homeomorphic_space Y" unfolding homeomorphic_map_maps using homeomorphic_space_def by blast lemma homeomorphic_empty_space: "X homeomorphic_space Y \ topspace X = {} \ topspace Y = {}" by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty) lemma homeomorphic_empty_space_eq: assumes "topspace X = {}" shows "X homeomorphic_space Y \ topspace Y = {}" unfolding homeomorphic_maps_def homeomorphic_space_def by (metis assms continuous_map_on_empty continuous_map_closedin ex_in_conv) subsection\Connected topological spaces\ definition connected_space :: "'a topology \ bool" where "connected_space X \ \(\E1 E2. openin X E1 \ openin X E2 \ topspace X \ E1 \ E2 \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" definition connectedin :: "'a topology \ 'a set \ bool" where "connectedin X S \ S \ topspace X \ connected_space (subtopology X S)" lemma connected_spaceD: "\connected_space X; openin X U; openin X V; topspace X \ U \ V; U \ V = {}; U \ {}; V \ {}\ \ False" by (auto simp: connected_space_def) lemma connectedin_subset_topspace: "connectedin X S \ S \ topspace X" by (simp add: connectedin_def) lemma connectedin_topspace: "connectedin X (topspace X) \ connected_space X" by (simp add: connectedin_def) lemma connected_space_subtopology: "connectedin X S \ connected_space (subtopology X S)" by (simp add: connectedin_def) lemma connectedin_subtopology: "connectedin (subtopology X S) T \ connectedin X T \ T \ S" by (force simp: connectedin_def subtopology_subtopology inf_absorb2) lemma connected_space_eq: "connected_space X \ (\E1 E2. openin X E1 \ openin X E2 \ E1 \ E2 = topspace X \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" unfolding connected_space_def by (metis openin_Un openin_subset subset_antisym) lemma connected_space_closedin: "connected_space X \ (\E1 E2. closedin X E1 \ closedin X E2 \ topspace X \ E1 \ E2 \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" (is "?lhs = ?rhs") proof assume ?lhs then have "\E1 E2. \openin X E1; E1 \ E2 = {}; topspace X \ E1 \ E2; openin X E2\ \ E1 = {} \ E2 = {}" by (simp add: connected_space_def) then show ?rhs unfolding connected_space_def by (metis disjnt_def separatedin_closed_sets separation_openin_Un_gen subtopology_superset) next assume R: ?rhs then show ?lhs unfolding connected_space_def by (metis Diff_triv Int_commute separatedin_openin_diff separation_closedin_Un_gen subtopology_superset) qed lemma connected_space_closedin_eq: "connected_space X \ (\E1 E2. closedin X E1 \ closedin X E2 \ E1 \ E2 = topspace X \ E1 \ E2 = {} \ E1 \ {} \ E2 \ {})" by (metis closedin_Un closedin_def connected_space_closedin subset_antisym) lemma connected_space_clopen_in: "connected_space X \ (\T. openin X T \ closedin X T \ T = {} \ T = topspace X)" proof - have eq: "openin X E1 \ openin X E2 \ E1 \ E2 = topspace X \ E1 \ E2 = {} \ P \ E2 = topspace X - E1 \ openin X E1 \ openin X E2 \ P" for E1 E2 P using openin_subset by blast show ?thesis unfolding connected_space_eq eq closedin_def by (auto simp: openin_closedin_eq) qed lemma connectedin: "connectedin X S \ S \ topspace X \ (\E1 E2. openin X E1 \ openin X E2 \ S \ E1 \ E2 \ E1 \ E2 \ S = {} \ E1 \ S \ {} \ E2 \ S \ {})" (is "?lhs = ?rhs") proof - have *: "(\E1:: 'a set. \E2:: 'a set. (\T1:: 'a set. P1 T1 \ E1 = f1 T1) \ (\T2:: 'a set. P2 T2 \ E2 = f2 T2) \ R E1 E2) \ (\T1 T2. P1 T1 \ P2 T2 \ R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R by auto show ?thesis unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology * by (intro conj_cong arg_cong [where f=Not] ex_cong1; blast dest!: openin_subset) qed lemma connectedinD: "\connectedin X S; openin X E1; openin X E2; S \ E1 \ E2; E1 \ E2 \ S = {}; E1 \ S \ {}; E2 \ S \ {}\ \ False" by (meson connectedin) lemma connectedin_iff_connected [simp]: "connectedin euclidean S \ connected S" by (simp add: connected_def connectedin) lemma connectedin_closedin: "connectedin X S \ S \ topspace X \ \(\E1 E2. closedin X E1 \ closedin X E2 \ S \ (E1 \ E2) \ (E1 \ E2 \ S = {}) \ \(E1 \ S = {}) \ \(E2 \ S = {}))" proof - have *: "(\E1:: 'a set. \E2:: 'a set. (\T1:: 'a set. P1 T1 \ E1 = f1 T1) \ (\T2:: 'a set. P2 T2 \ E2 = f2 T2) \ R E1 E2) \ (\T1 T2. P1 T1 \ P2 T2 \ R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R by auto show ?thesis unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology * by (intro conj_cong arg_cong [where f=Not] ex_cong1; blast dest!: openin_subset) qed lemma connectedin_empty [simp]: "connectedin X {}" by (simp add: connectedin) lemma connected_space_topspace_empty: "topspace X = {} \ connected_space X" using connectedin_topspace by fastforce lemma connectedin_sing [simp]: "connectedin X {a} \ a \ topspace X" by (simp add: connectedin) lemma connectedin_absolute [simp]: "connectedin (subtopology X S) S \ connectedin X S" by (simp add: connectedin_subtopology) lemma connectedin_Union: assumes \: "\S. S \ \ \ connectedin X S" and ne: "\\ \ {}" shows "connectedin X (\\)" proof - have "\\ \ topspace X" using \ by (simp add: Union_least connectedin_def) moreover have False if "openin X E1" "openin X E2" and cover: "\\ \ E1 \ E2" and disj: "E1 \ E2 \ \\ = {}" and overlap1: "E1 \ \\ \ {}" and overlap2: "E2 \ \\ \ {}" for E1 E2 proof - have disjS: "E1 \ E2 \ S = {}" if "S \ \" for S using Diff_triv that disj by auto have coverS: "S \ E1 \ E2" if "S \ \" for S using that cover by blast have "\ \ {}" using overlap1 by blast obtain a where a: "\U. U \ \ \ a \ U" using ne by force with \\ \ {}\ have "a \ \\" by blast then consider "a \ E1" | "a \ E2" using \\\ \ E1 \ E2\ by auto then show False proof cases case 1 then obtain b S where "b \ E2" "b \ S" "S \ \" using overlap2 by blast then show ?thesis using "1" \openin X E1\ \openin X E2\ disjS coverS a [OF \S \ \\] \[OF \S \ \\] unfolding connectedin by (meson disjoint_iff_not_equal) next case 2 then obtain b S where "b \ E1" "b \ S" "S \ \" using overlap1 by blast then show ?thesis using "2" \openin X E1\ \openin X E2\ disjS coverS a [OF \S \ \\] \[OF \S \ \\] unfolding connectedin by (meson disjoint_iff_not_equal) qed qed ultimately show ?thesis unfolding connectedin by blast qed lemma connectedin_Un: "\connectedin X S; connectedin X T; S \ T \ {}\ \ connectedin X (S \ T)" using connectedin_Union [of "{S,T}"] by auto lemma connected_space_subconnected: "connected_space X \ (\x \ topspace X. \y \ topspace X. \S. connectedin X S \ x \ S \ y \ S)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using connectedin_topspace by blast next assume R [rule_format]: ?rhs have False if "openin X U" "openin X V" and disj: "U \ V = {}" and cover: "topspace X \ U \ V" and "U \ {}" "V \ {}" for U V proof - obtain u v where "u \ U" "v \ V" using \U \ {}\ \V \ {}\ by auto then obtain T where "u \ T" "v \ T" and T: "connectedin X T" using R [of u v] that by (meson \openin X U\ \openin X V\ subsetD openin_subset) then show False using that unfolding connectedin by (metis IntI \u \ U\ \v \ V\ empty_iff inf_bot_left subset_trans) qed then show ?lhs by (auto simp: connected_space_def) qed lemma connectedin_intermediate_closure_of: assumes "connectedin X S" "S \ T" "T \ X closure_of S" shows "connectedin X T" proof - have S: "S \ topspace X" and T: "T \ topspace X" using assms by (meson closure_of_subset_topspace dual_order.trans)+ have \
: "\E1 E2. \openin X E1; openin X E2; E1 \ S = {} \ E2 \ S = {}\ \ E1 \ T = {} \ E2 \ T = {}" using assms unfolding disjoint_iff by (meson in_closure_of subsetD) then show ?thesis using assms unfolding connectedin closure_of_subset_topspace S T by (metis Int_empty_right T dual_order.trans inf.orderE inf_left_commute) qed lemma connectedin_closure_of: "connectedin X S \ connectedin X (X closure_of S)" by (meson closure_of_subset connectedin_def connectedin_intermediate_closure_of subset_refl) lemma connectedin_separation: "connectedin X S \ S \ topspace X \ (\C1 C2. C1 \ C2 = S \ C1 \ {} \ C2 \ {} \ C1 \ X closure_of C2 = {} \ C2 \ X closure_of C1 = {})" unfolding connectedin_def connected_space_closedin_eq closedin_Int_closure_of topspace_subtopology apply (intro conj_cong refl arg_cong [where f=Not]) apply (intro ex_cong1 iffI, blast) using closure_of_subset_Int by force lemma connectedin_eq_not_separated: "connectedin X S \ S \ topspace X \ (\C1 C2. C1 \ C2 = S \ C1 \ {} \ C2 \ {} \ separatedin X C1 C2)" unfolding separatedin_def by (metis connectedin_separation sup.boundedE) lemma connectedin_eq_not_separated_subset: "connectedin X S \ S \ topspace X \ (\C1 C2. S \ C1 \ C2 \ S \ C1 \ {} \ S \ C2 \ {} \ separatedin X C1 C2)" proof - have "\C1 C2. S \ C1 \ C2 \ S \ C1 = {} \ S \ C2 = {} \ \ separatedin X C1 C2" if "\C1 C2. C1 \ C2 = S \ C1 = {} \ C2 = {} \ \ separatedin X C1 C2" proof (intro allI) fix C1 C2 show "S \ C1 \ C2 \ S \ C1 = {} \ S \ C2 = {} \ \ separatedin X C1 C2" using that [of "S \ C1" "S \ C2"] by (auto simp: separatedin_mono) qed then show ?thesis by (metis Un_Int_eq(1) Un_Int_eq(2) connectedin_eq_not_separated order_refl) qed lemma connected_space_eq_not_separated: "connected_space X \ (\C1 C2. C1 \ C2 = topspace X \ C1 \ {} \ C2 \ {} \ separatedin X C1 C2)" by (simp add: connectedin_eq_not_separated flip: connectedin_topspace) lemma connected_space_eq_not_separated_subset: "connected_space X \ (\C1 C2. topspace X \ C1 \ C2 \ C1 \ {} \ C2 \ {} \ separatedin X C1 C2)" by (metis connected_space_eq_not_separated le_sup_iff separatedin_def subset_antisym) lemma connectedin_subset_separated_union: "\connectedin X C; separatedin X S T; C \ S \ T\ \ C \ S \ C \ T" unfolding connectedin_eq_not_separated_subset by blast lemma connectedin_nonseparated_union: assumes "connectedin X S" "connectedin X T" "\separatedin X S T" shows "connectedin X (S \ T)" proof - have "\C1 C2. \T \ C1 \ C2; S \ C1 \ C2\ \ S \ C1 = {} \ T \ C1 = {} \ S \ C2 = {} \ T \ C2 = {} \ \ separatedin X C1 C2" using assms unfolding connectedin_eq_not_separated_subset by (metis (no_types, lifting) assms connectedin_subset_separated_union inf.orderE separatedin_empty(1) separatedin_mono separatedin_sym) then show ?thesis unfolding connectedin_eq_not_separated_subset by (simp add: assms connectedin_subset_topspace Int_Un_distrib2) qed lemma connected_space_closures: "connected_space X \ (\e1 e2. e1 \ e2 = topspace X \ X closure_of e1 \ X closure_of e2 = {} \ e1 \ {} \ e2 \ {})" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding connected_space_closedin_eq by (metis Un_upper1 Un_upper2 closedin_closure_of closure_of_Un closure_of_eq_empty closure_of_topspace) next assume ?rhs then show ?lhs unfolding connected_space_closedin_eq by (metis closure_of_eq) qed lemma connectedin_Int_frontier_of: assumes "connectedin X S" "S \ T \ {}" "S - T \ {}" shows "S \ X frontier_of T \ {}" proof - have "S \ topspace X" and *: "\E1 E2. openin X E1 \ openin X E2 \ E1 \ E2 \ S = {} \ S \ E1 \ E2 \ E1 \ S = {} \ E2 \ S = {}" using \connectedin X S\ by (auto simp: connectedin) moreover have "S - (topspace X \ T) \ {}" using assms(3) by blast moreover have "S \ topspace X \ T \ {}" using assms connectedin by fastforce moreover have False if "S \ T \ {}" "S - T \ {}" "T \ topspace X" "S \ X frontier_of T = {}" for T proof - have null: "S \ (X closure_of T - X interior_of T) = {}" using that unfolding frontier_of_def by blast have "X interior_of T \ (topspace X - X closure_of T) \ S = {}" by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty) moreover have "S \ X interior_of T \ (topspace X - X closure_of T)" using that \S \ topspace X\ null by auto moreover have "S \ X interior_of T \ {}" using closure_of_subset that(1) that(3) null by fastforce ultimately have "S \ X interior_of (topspace X - T) = {}" by (metis "*" inf_commute interior_of_complement openin_interior_of) then have "topspace (subtopology X S) \ X interior_of T = S" using \S \ topspace X\ interior_of_complement null by fastforce then show ?thesis using that by (metis Diff_eq_empty_iff inf_le2 interior_of_subset subset_trans) qed ultimately show ?thesis by (metis Int_lower1 frontier_of_restrict inf_assoc) qed lemma connectedin_continuous_map_image: assumes f: "continuous_map X Y f" and "connectedin X S" shows "connectedin Y (f ` S)" proof - have "S \ topspace X" and *: "\E1 E2. openin X E1 \ openin X E2 \ E1 \ E2 \ S = {} \ S \ E1 \ E2 \ E1 \ S = {} \ E2 \ S = {}" using \connectedin X S\ by (auto simp: connectedin) show ?thesis unfolding connectedin connected_space_def proof (intro conjI notI; clarify) show "f x \ topspace Y" if "x \ S" for x using \S \ topspace X\ continuous_map_image_subset_topspace f that by blast next fix U V let ?U = "{x \ topspace X. f x \ U}" let ?V = "{x \ topspace X. f x \ V}" assume UV: "openin Y U" "openin Y V" "f ` S \ U \ V" "U \ V \ f ` S = {}" "U \ f ` S \ {}" "V \ f ` S \ {}" then have 1: "?U \ ?V \ S = {}" by auto have 2: "openin X ?U" "openin X ?V" using \openin Y U\ \openin Y V\ continuous_map f by fastforce+ show "False" using * [of ?U ?V] UV \S \ topspace X\ by (auto simp: 1 2) qed qed lemma homeomorphic_connected_space: "X homeomorphic_space Y \ connected_space X \ connected_space Y" unfolding homeomorphic_space_def homeomorphic_maps_def by (metis connected_space_subconnected connectedin_continuous_map_image connectedin_topspace continuous_map_image_subset_topspace image_eqI image_subset_iff) lemma homeomorphic_map_connectedness: assumes f: "homeomorphic_map X Y f" and U: "U \ topspace X" shows "connectedin Y (f ` U) \ connectedin X U" proof - have 1: "f ` U \ topspace Y \ U \ topspace X" using U f homeomorphic_imp_surjective_map by blast moreover have "connected_space (subtopology Y (f ` U)) \ connected_space (subtopology X U)" proof (rule homeomorphic_connected_space) have "f ` U \ topspace Y" by (simp add: U 1) then have "topspace Y \ f ` U = f ` U" by (simp add: subset_antisym) then show "subtopology Y (f ` U) homeomorphic_space subtopology X U" by (metis U f homeomorphic_map_imp_homeomorphic_space homeomorphic_map_subtopologies homeomorphic_space_sym inf.absorb_iff2) qed ultimately show ?thesis by (auto simp: connectedin_def) qed lemma homeomorphic_map_connectedness_eq: "homeomorphic_map X Y f \ connectedin X U \ U \ topspace X \ connectedin Y (f ` U)" using homeomorphic_map_connectedness connectedin_subset_topspace by metis lemma connectedin_discrete_topology: "connectedin (discrete_topology U) S \ S \ U \ (\a. S \ {a})" proof (cases "S \ U") case True show ?thesis proof (cases "S = {}") case False moreover have "connectedin (discrete_topology U) S \ (\a. S = {a})" proof show "connectedin (discrete_topology U) S \ \a. S = {a}" using False connectedin_Int_frontier_of insert_Diff by fastforce qed (use True in auto) ultimately show ?thesis by auto qed simp next case False then show ?thesis by (simp add: connectedin_def) qed lemma connected_space_discrete_topology: "connected_space (discrete_topology U) \ (\a. U \ {a})" by (metis connectedin_discrete_topology connectedin_topspace order_refl topspace_discrete_topology) subsection\Compact sets\ definition compactin where "compactin X S \ S \ topspace X \ (\\. (\U \ \. openin X U) \ S \ \\ \ (\\. finite \ \ \ \ \ \ S \ \\))" definition compact_space where "compact_space X \ compactin X (topspace X)" lemma compact_space_alt: "compact_space X \ (\\. (\U \ \. openin X U) \ topspace X \ \\ \ (\\. finite \ \ \ \ \ \ topspace X \ \\))" by (simp add: compact_space_def compactin_def) lemma compact_space: "compact_space X \ (\\. (\U \ \. openin X U) \ \\ = topspace X \ (\\. finite \ \ \ \ \ \ \\ = topspace X))" unfolding compact_space_alt using openin_subset by fastforce lemma compactinD: "\compactin X S; \U. U \ \ \ openin X U; S \ \\\ \ \\. finite \ \ \ \ \ \ S \ \\" by (auto simp: compactin_def) lemma compactin_euclidean_iff [simp]: "compactin euclidean S \ compact S" by (simp add: compact_eq_Heine_Borel compactin_def) meson lemma compactin_absolute [simp]: "compactin (subtopology X S) S \ compactin X S" proof - have eq: "(\U \ \. \Y. openin X Y \ U = Y \ S) \ \ \ (\Y. Y \ S) ` {y. openin X y}" for \ by auto show ?thesis by (auto simp: compactin_def openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image) qed lemma compactin_subspace: "compactin X S \ S \ topspace X \ compact_space (subtopology X S)" unfolding compact_space_def topspace_subtopology by (metis compactin_absolute compactin_def inf.absorb2) lemma compact_space_subtopology: "compactin X S \ compact_space (subtopology X S)" by (simp add: compactin_subspace) lemma compactin_subtopology: "compactin (subtopology X S) T \ compactin X T \ T \ S" by (metis compactin_subspace inf.absorb_iff2 le_inf_iff subtopology_subtopology topspace_subtopology) lemma compactin_subset_topspace: "compactin X S \ S \ topspace X" by (simp add: compactin_subspace) lemma compactin_contractive: "\compactin X' S; topspace X' = topspace X; \U. openin X U \ openin X' U\ \ compactin X S" by (simp add: compactin_def) lemma finite_imp_compactin: "\S \ topspace X; finite S\ \ compactin X S" by (metis compactin_subspace compact_space finite_UnionD inf.absorb_iff2 order_refl topspace_subtopology) lemma compactin_empty [iff]: "compactin X {}" by (simp add: finite_imp_compactin) lemma compact_space_topspace_empty: "topspace X = {} \ compact_space X" by (simp add: compact_space_def) lemma finite_imp_compactin_eq: "finite S \ (compactin X S \ S \ topspace X)" using compactin_subset_topspace finite_imp_compactin by blast lemma compactin_sing [simp]: "compactin X {a} \ a \ topspace X" by (simp add: finite_imp_compactin_eq) lemma closed_compactin: assumes XK: "compactin X K" and "C \ K" and XC: "closedin X C" shows "compactin X C" unfolding compactin_def proof (intro conjI allI impI) show "C \ topspace X" by (simp add: XC closedin_subset) next fix \ :: "'a set set" assume \: "Ball \ (openin X) \ C \ \\" have "(\U\insert (topspace X - C) \. openin X U)" using XC \ by blast moreover have "K \ \(insert (topspace X - C) \)" using \ XK compactin_subset_topspace by fastforce ultimately obtain \ where "finite \" "\ \ insert (topspace X - C) \" "K \ \\" using assms unfolding compactin_def by metis moreover have "openin X (topspace X - C)" using XC by auto ultimately show "\\. finite \ \ \ \ \ \ C \ \\" using \C \ K\ by (rule_tac x="\ - {topspace X - C}" in exI) auto qed lemma closedin_compact_space: "\compact_space X; closedin X S\ \ compactin X S" by (simp add: closed_compactin closedin_subset compact_space_def) lemma compact_Int_closedin: assumes "compactin X S" "closedin X T" shows "compactin X (S \ T)" proof - have "compactin (subtopology X S) (S \ T)" by (metis assms closedin_compact_space closedin_subtopology compactin_subspace inf_commute) then show ?thesis by (simp add: compactin_subtopology) qed lemma closed_Int_compactin: "\closedin X S; compactin X T\ \ compactin X (S \ T)" by (metis compact_Int_closedin inf_commute) lemma compactin_Un: assumes S: "compactin X S" and T: "compactin X T" shows "compactin X (S \ T)" unfolding compactin_def proof (intro conjI allI impI) show "S \ T \ topspace X" using assms by (auto simp: compactin_def) next fix \ :: "'a set set" assume \: "Ball \ (openin X) \ S \ T \ \\" with S obtain \ where \: "finite \" "\ \ \" "S \ \\" unfolding compactin_def by (meson sup.bounded_iff) obtain \ where "finite \" "\ \ \" "T \ \\" using \ T unfolding compactin_def by (meson sup.bounded_iff) with \ show "\\. finite \ \ \ \ \ \ S \ T \ \\" by (rule_tac x="\ \ \" in exI) auto qed lemma compactin_Union: "\finite \; \S. S \ \ \ compactin X S\ \ compactin X (\\)" by (induction rule: finite_induct) (simp_all add: compactin_Un) lemma compactin_subtopology_imp_compact: assumes "compactin (subtopology X S) K" shows "compactin X K" using assms proof (clarsimp simp add: compactin_def) fix \ define \ where "\ \ (\U. U \ S) ` \" assume "K \ topspace X" and "K \ S" and "\x\\. openin X x" and "K \ \\" then have "\V \ \. openin (subtopology X S) V" "K \ \\" unfolding \_def by (auto simp: openin_subtopology) moreover assume "\\. (\x\\. openin (subtopology X S) x) \ K \ \\ \ (\\. finite \ \ \ \ \ \ K \ \\)" ultimately obtain \ where "finite \" "\ \ \" "K \ \\" by meson then have \: "\U. U \ \ \ V = U \ S" if "V \ \" for V unfolding \_def using that by blast let ?\ = "(\F. @U. U \ \ \ F = U \ S) ` \" show "\\. finite \ \ \ \ \ \ K \ \\" proof (intro exI conjI) show "finite ?\" using \finite \\ by blast show "?\ \ \" using someI_ex [OF \] by blast show "K \ \?\" proof clarsimp fix x assume "x \ K" then show "\V \ \. x \ (SOME U. U \ \ \ V = U \ S)" using \K \ \\\ someI_ex [OF \] by (metis (no_types, lifting) IntD1 Union_iff subsetCE) qed qed qed lemma compact_imp_compactin_subtopology: assumes "compactin X K" "K \ S" shows "compactin (subtopology X S) K" using assms proof (clarsimp simp add: compactin_def) fix \ :: "'a set set" define \ where "\ \ {V. openin X V \ (\U \ \. U = V \ S)}" assume "K \ S" and "K \ topspace X" and "\U\\. openin (subtopology X S) U" and "K \ \\" then have "\V \ \. openin X V" "K \ \\" unfolding \_def by (fastforce simp: subset_eq openin_subtopology)+ moreover assume "\\. (\U\\. openin X U) \ K \ \\ \ (\\. finite \ \ \ \ \ \ K \ \\)" ultimately obtain \ where "finite \" "\ \ \" "K \ \\" by meson let ?\ = "(\F. F \ S) ` \" show "\\. finite \ \ \ \ \ \ K \ \\" proof (intro exI conjI) show "finite ?\" using \finite \\ by blast show "?\ \ \" using \_def \\ \ \\ by blast show "K \ \?\" using \K \ \\\ assms(2) by auto qed qed proposition compact_space_fip: "compact_space X \ (\\. (\C\\. closedin X C) \ (\\. finite \ \ \ \ \ \ \\ \ {}) \ \\ \ {})" (is "_ = ?rhs") proof (cases "topspace X = {}") case True then show ?thesis unfolding compact_space_def by (metis Sup_bot_conv(1) closedin_topspace_empty compactin_empty finite.emptyI finite_UnionD order_refl) next case False show ?thesis proof safe fix \ :: "'a set set" assume * [rule_format]: "\\. finite \ \ \ \ \ \ \\ \ {}" define \ where "\ \ (\S. topspace X - S) ` \" assume clo: "\C\\. closedin X C" and [simp]: "\\ = {}" then have "\V \ \. openin X V" "topspace X \ \\" by (auto simp: \_def) moreover assume [unfolded compact_space_alt, rule_format, of \]: "compact_space X" ultimately obtain \ where \: "finite \" "\ \ \" "topspace X \ topspace X - \\" by (auto simp: ex_finite_subset_image \_def) moreover have "\ \ {}" using \ \topspace X \ {}\ by blast ultimately show "False" using * [of \] by auto (metis Diff_iff Inter_iff clo closedin_def subsetD) next assume R [rule_format]: ?rhs show "compact_space X" unfolding compact_space_alt proof clarify fix \ :: "'a set set" define \ where "\ \ (\S. topspace X - S) ` \" assume "\C\\. openin X C" and "topspace X \ \\" with \topspace X \ {}\ have *: "\V \ \. closedin X V" "\ \ {}" by (auto simp: \_def) show "\\. finite \ \ \ \ \ \ topspace X \ \\" proof (rule ccontr; simp) assume "\\\\. finite \ \ \ topspace X \ \\" then have "\\. finite \ \ \ \ \ \ \\ \ {}" by (simp add: \_def all_finite_subset_image) with \topspace X \ \\\ show False using R [of \] * by (simp add: \_def) qed qed qed qed corollary compactin_fip: "compactin X S \ S \ topspace X \ (\\. (\C\\. closedin X C) \ (\\. finite \ \ \ \ \ \ S \ \\ \ {}) \ S \ \\ \ {})" proof (cases "S = {}") case False show ?thesis proof (cases "S \ topspace X") case True then have "compactin X S \ (\\. \ \ (\T. S \ T) ` {T. closedin X T} \ (\\. finite \ \ \ \ \ \ \\ \ {}) \ \\ \ {})" by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL) also have "\ = (\\\Collect (closedin X). (\\. finite \ \ \ \ (\) S ` \ \ \\ \ {}) \ \ ((\) S ` \) \ {})" by (simp add: all_subset_image) also have "\ = (\\. (\C\\. closedin X C) \ (\\. finite \ \ \ \ \ \ S \ \\ \ {}) \ S \ \\ \ {})" proof - have eq: "((\\. finite \ \ \ \ \ \ \ ((\) S ` \) \ {}) \ \ ((\) S ` \) \ {}) \ ((\\. finite \ \ \ \ \ \ S \ \\ \ {}) \ S \ \\ \ {})" for \ by simp (use \S \ {}\ in blast) show ?thesis unfolding imp_conjL [symmetric] all_finite_subset_image eq by blast qed finally show ?thesis using True by simp qed (simp add: compactin_subspace) qed force corollary compact_space_imp_nest: fixes C :: "nat \ 'a set" assumes "compact_space X" and clo: "\n. closedin X (C n)" and ne: "\n. C n \ {}" and dec: "decseq C" shows "(\n. C n) \ {}" proof - let ?\ = "range (\n. \m \ n. C m)" have "closedin X A" if "A \ ?\" for A using that clo by auto moreover have "(\n\K. \m \ n. C m) \ {}" if "finite K" for K proof - obtain n where "\k. k \ K \ k \ n" using Max.coboundedI \finite K\ by blast with dec have "C n \ (\n\K. \m \ n. C m)" unfolding decseq_def by blast with ne [of n] show ?thesis by blast qed ultimately show ?thesis using \compact_space X\ [unfolded compact_space_fip, rule_format, of ?\] by (simp add: all_finite_subset_image INT_extend_simps UN_atMost_UNIV del: INT_simps) qed lemma compactin_discrete_topology: "compactin (discrete_topology X) S \ S \ X \ finite S" (is "?lhs = ?rhs") proof (intro iffI conjI) assume L: ?lhs then show "S \ X" by (auto simp: compactin_def) have *: "\\. Ball \ (openin (discrete_topology X)) \ S \ \\ \ (\\. finite \ \ \ \ \ \ S \ \\)" using L by (auto simp: compactin_def) show "finite S" using * [of "(\x. {x}) ` X"] \S \ X\ by clarsimp (metis UN_singleton finite_subset_image infinite_super) next assume ?rhs then show ?lhs by (simp add: finite_imp_compactin) qed lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \ finite X" by (simp add: compactin_discrete_topology compact_space_def) lemma compact_space_imp_Bolzano_Weierstrass: assumes "compact_space X" "infinite S" "S \ topspace X" shows "X derived_set_of S \ {}" proof assume X: "X derived_set_of S = {}" then have "closedin X S" by (simp add: closedin_contains_derived_set assms) then have "compactin X S" by (rule closedin_compact_space [OF \compact_space X\]) with X show False by (metis \infinite S\ compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq) qed lemma compactin_imp_Bolzano_Weierstrass: "\compactin X S; infinite T \ T \ S\ \ S \ X derived_set_of T \ {}" using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"] by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2) lemma compact_closure_of_imp_Bolzano_Weierstrass: "\compactin X (X closure_of S); infinite T; T \ S; T \ topspace X\ \ X derived_set_of T \ {}" using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce lemma discrete_compactin_eq_finite: "S \ X derived_set_of S = {} \ compactin X S \ S \ topspace X \ finite S" by (meson compactin_imp_Bolzano_Weierstrass finite_imp_compactin_eq order_refl) lemma discrete_compact_space_eq_finite: "X derived_set_of (topspace X) = {} \ (compact_space X \ finite(topspace X))" by (metis compact_space_discrete_topology discrete_topology_unique_derived_set) lemma image_compactin: assumes cpt: "compactin X S" and cont: "continuous_map X Y f" shows "compactin Y (f ` S)" unfolding compactin_def proof (intro conjI allI impI) show "f ` S \ topspace Y" using compactin_subset_topspace cont continuous_map_image_subset_topspace cpt by blast next fix \ :: "'b set set" assume \: "Ball \ (openin Y) \ f ` S \ \\" define \ where "\ \ (\U. {x \ topspace X. f x \ U}) ` \" have "S \ topspace X" and *: "\\. \\U\\. openin X U; S \ \\\ \ \\. finite \ \ \ \ \ \ S \ \\" using cpt by (auto simp: compactin_def) obtain \ where \: "finite \" "\ \ \" "S \ \\" proof - have 1: "\U\\. openin X U" unfolding \_def using \ cont[unfolded continuous_map] by blast have 2: "S \ \\" unfolding \_def using compactin_subset_topspace cpt \ by fastforce show thesis using * [OF 1 2] that by metis qed have "\v \ \. \U. U \ \ \ v = {x \ topspace X. f x \ U}" using \_def by blast then obtain U where U: "\v \ \. U v \ \ \ v = {x \ topspace X. f x \ U v}" by metis show "\\. finite \ \ \ \ \ \ f ` S \ \\" proof (intro conjI exI) show "finite (U ` \)" by (simp add: \finite \\) next show "U ` \ \ \" using \\ \ \\ U by auto next show "f ` S \ \ (U ` \)" using \(2-3) U UnionE subset_eq U by fastforce qed qed lemma homeomorphic_compact_space: assumes "X homeomorphic_space Y" shows "compact_space X \ compact_space Y" using homeomorphic_space_sym by (metis assms compact_space_def homeomorphic_eq_everything_map homeomorphic_space image_compactin) lemma homeomorphic_map_compactness: assumes hom: "homeomorphic_map X Y f" and U: "U \ topspace X" shows "compactin Y (f ` U) \ compactin X U" proof - have "f ` U \ topspace Y" using hom U homeomorphic_imp_surjective_map by blast moreover have "homeomorphic_map (subtopology X U) (subtopology Y (f ` U)) f" using U hom homeomorphic_imp_surjective_map by (blast intro: homeomorphic_map_subtopologies) then have "compact_space (subtopology Y (f ` U)) = compact_space (subtopology X U)" using homeomorphic_compact_space homeomorphic_map_imp_homeomorphic_space by blast ultimately show ?thesis by (simp add: compactin_subspace U) qed lemma homeomorphic_map_compactness_eq: "homeomorphic_map X Y f \ compactin X U \ U \ topspace X \ compactin Y (f ` U)" by (meson compactin_subset_topspace homeomorphic_map_compactness) subsection\Embedding maps\ definition embedding_map where "embedding_map X Y f \ homeomorphic_map X (subtopology Y (f ` (topspace X))) f" lemma embedding_map_eq: "\embedding_map X Y f; \x. x \ topspace X \ f x = g x\ \ embedding_map X Y g" unfolding embedding_map_def by (metis homeomorphic_map_eq image_cong) lemma embedding_map_compose: assumes "embedding_map X X' f" "embedding_map X' X'' g" shows "embedding_map X X'' (g \ f)" proof - have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g" using assms by (auto simp: embedding_map_def) then obtain C where "g ` topspace X' \ C = (g \ f) ` topspace X" by (metis homeomorphic_imp_surjective_map image_comp image_mono inf.absorb_iff2 topspace_subtopology) then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \ f) ` topspace X)) g" by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology) then show ?thesis unfolding embedding_map_def using hm(1) homeomorphic_map_compose by blast qed lemma surjective_embedding_map: "embedding_map X Y f \ f ` (topspace X) = topspace Y \ homeomorphic_map X Y f" by (force simp: embedding_map_def homeomorphic_eq_everything_map) lemma embedding_map_in_subtopology: "embedding_map X (subtopology Y S) f \ embedding_map X Y f \ f ` (topspace X) \ S" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" unfolding embedding_map_def by (metis continuous_map_in_subtopology homeomorphic_imp_continuous_map inf_absorb2 subtopology_subtopology) qed (simp add: embedding_map_def inf.absorb_iff2 subtopology_subtopology) lemma injective_open_imp_embedding_map: "\continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\ \ embedding_map X Y f" unfolding embedding_map_def by (simp add: continuous_map_in_subtopology continuous_open_quotient_map eq_iff homeomorphic_map_def open_map_imp_subset open_map_into_subtopology) lemma injective_closed_imp_embedding_map: "\continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\ \ embedding_map X Y f" unfolding embedding_map_def by (simp add: closed_map_imp_subset closed_map_into_subtopology continuous_closed_quotient_map continuous_map_in_subtopology dual_order.eq_iff homeomorphic_map_def) lemma embedding_map_imp_homeomorphic_space: "embedding_map X Y f \ X homeomorphic_space (subtopology Y (f ` (topspace X)))" unfolding embedding_map_def using homeomorphic_space by blast lemma embedding_imp_closed_map: "\embedding_map X Y f; closedin Y (f ` topspace X)\ \ closed_map X Y f" unfolding closed_map_def by (auto simp: closedin_closed_subtopology embedding_map_def homeomorphic_map_closedness_eq) lemma embedding_imp_closed_map_eq: "embedding_map X Y f \ (closed_map X Y f \ closedin Y (f ` topspace X))" using closed_map_def embedding_imp_closed_map by blast subsection\Retraction and section maps\ definition retraction_maps :: "'a topology \ 'b topology \ ('a \ 'b) \ ('b \ 'a) \ bool" where "retraction_maps X Y f g \ continuous_map X Y f \ continuous_map Y X g \ (\x \ topspace Y. f(g x) = x)" definition section_map :: "'a topology \ 'b topology \ ('a \ 'b) \ bool" where "section_map X Y f \ \g. retraction_maps Y X g f" definition retraction_map :: "'a topology \ 'b topology \ ('a \ 'b) \ bool" where "retraction_map X Y f \ \g. retraction_maps X Y f g" lemma retraction_maps_eq: "\retraction_maps X Y f g; \x. x \ topspace X \ f x = f' x; \x. x \ topspace Y \ g x = g' x\ \ retraction_maps X Y f' g'" unfolding retraction_maps_def by (metis (no_types, lifting) continuous_map_def continuous_map_eq) lemma section_map_eq: "\section_map X Y f; \x. x \ topspace X \ f x = g x\ \ section_map X Y g" unfolding section_map_def using retraction_maps_eq by blast lemma retraction_map_eq: "\retraction_map X Y f; \x. x \ topspace X \ f x = g x\ \ retraction_map X Y g" unfolding retraction_map_def using retraction_maps_eq by blast lemma homeomorphic_imp_retraction_maps: "homeomorphic_maps X Y f g \ retraction_maps X Y f g" by (simp add: homeomorphic_maps_def retraction_maps_def) lemma section_and_retraction_eq_homeomorphic_map: "section_map X Y f \ retraction_map X Y f \ homeomorphic_map X Y f" (is "?lhs = ?rhs") proof assume ?lhs then obtain g where "homeomorphic_maps X Y f g" unfolding homeomorphic_maps_def retraction_map_def section_map_def by (smt (verit, best) continuous_map_def retraction_maps_def) then show ?rhs using homeomorphic_map_maps by blast next assume ?rhs then show ?lhs unfolding retraction_map_def section_map_def by (meson homeomorphic_imp_retraction_maps homeomorphic_map_maps homeomorphic_maps_sym) qed lemma section_imp_embedding_map: "section_map X Y f \ embedding_map X Y f" unfolding section_map_def embedding_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology) lemma retraction_imp_quotient_map: assumes "retraction_map X Y f" shows "quotient_map X Y f" unfolding quotient_map_def proof (intro conjI subsetI allI impI) show "f ` topspace X = topspace Y" using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def) next fix U assume U: "U \ topspace Y" have "openin Y U" if "\x\topspace Y. g x \ topspace X" "\x\topspace Y. f (g x) = x" "openin Y {x \ topspace Y. g x \ {x \ topspace X. f x \ U}}" for g using openin_subopen U that by fastforce then show "openin X {x \ topspace X. f x \ U} = openin Y U" using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def) qed lemma retraction_maps_compose: "\retraction_maps X Y f f'; retraction_maps Y Z g g'\ \ retraction_maps X Z (g \ f) (f' \ g')" by (clarsimp simp: retraction_maps_def continuous_map_compose) (simp add: continuous_map_def) lemma retraction_map_compose: "\retraction_map X Y f; retraction_map Y Z g\ \ retraction_map X Z (g \ f)" by (meson retraction_map_def retraction_maps_compose) lemma section_map_compose: "\section_map X Y f; section_map Y Z g\ \ section_map X Z (g \ f)" by (meson retraction_maps_compose section_map_def) lemma surjective_section_eq_homeomorphic_map: "section_map X Y f \ f ` (topspace X) = topspace Y \ homeomorphic_map X Y f" by (meson section_and_retraction_eq_homeomorphic_map section_imp_embedding_map surjective_embedding_map) lemma surjective_retraction_or_section_map: "f ` (topspace X) = topspace Y \ retraction_map X Y f \ section_map X Y f \ retraction_map X Y f" using section_and_retraction_eq_homeomorphic_map surjective_section_eq_homeomorphic_map by fastforce lemma retraction_imp_surjective_map: "retraction_map X Y f \ f ` (topspace X) = topspace Y" by (simp add: retraction_imp_quotient_map quotient_imp_surjective_map) lemma section_imp_injective_map: "\section_map X Y f; x \ topspace X; y \ topspace X\ \ f x = f y \ x = y" by (metis (mono_tags, opaque_lifting) retraction_maps_def section_map_def) lemma retraction_maps_to_retract_maps: "retraction_maps X Y r s \ retraction_maps X (subtopology X (s ` (topspace Y))) (s \ r) id" unfolding retraction_maps_def by (auto simp: continuous_map_compose continuous_map_into_subtopology continuous_map_from_subtopology) subsection \Continuity\ lemma continuous_on_open: "continuous_on S f \ (\T. openin (top_of_set (f ` S)) T \ openin (top_of_set S) (S \ f -` T))" unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong) lemma continuous_on_closed: "continuous_on S f \ (\T. closedin (top_of_set (f ` S)) T \ closedin (top_of_set S) (S \ f -` T))" unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong) lemma continuous_on_imp_closedin: assumes "continuous_on S f" "closedin (top_of_set (f ` S)) T" shows "closedin (top_of_set S) (S \ f -` T)" using assms continuous_on_closed by blast lemma continuous_map_subtopology_eu [simp]: "continuous_map (top_of_set S) (subtopology euclidean T) h \ continuous_on S h \ h ` S \ T" by (simp add: continuous_map_in_subtopology) lemma continuous_map_euclidean_top_of_set: assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f" shows "continuous_map euclidean (top_of_set S) f" by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage) subsection\<^marker>\tag unimportant\ \Half-global and completely global cases\ lemma continuous_openin_preimage_gen: assumes "continuous_on S f" "open T" shows "openin (top_of_set S) (S \ f -` T)" proof - have *: "(S \ f -` T) = (S \ f -` (T \ f ` S))" by auto have "openin (top_of_set (f ` S)) (T \ f ` S)" using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto then show ?thesis using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \ f ` S"]] using * by auto qed lemma continuous_closedin_preimage: assumes "continuous_on S f" and "closed T" shows "closedin (top_of_set S) (S \ f -` T)" proof - have *: "(S \ f -` T) = (S \ f -` (T \ f ` S))" by auto have "closedin (top_of_set (f ` S)) (T \ f ` S)" using closedin_closed_Int[of T "f ` S", OF assms(2)] by (simp add: Int_commute) then show ?thesis using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \ f ` S"]] using * by auto qed lemma continuous_openin_preimage_eq: "continuous_on S f \ (\T. open T \ openin (top_of_set S) (S \ f -` T))" by (metis Int_commute continuous_on_open_invariant open_openin openin_subtopology) lemma continuous_closedin_preimage_eq: "continuous_on S f \ (\T. closed T \ closedin (top_of_set S) (S \ f -` T))" by (metis Int_commute closedin_closed continuous_on_closed_invariant) lemma continuous_open_preimage: assumes contf: "continuous_on S f" and "open S" "open T" shows "open (S \ f -` T)" proof- obtain U where "open U" "(S \ f -` T) = S \ U" using continuous_openin_preimage_gen[OF contf \open T\] unfolding openin_open by auto then show ?thesis using open_Int[of S U, OF \open S\] by auto qed lemma continuous_closed_preimage: assumes contf: "continuous_on S f" and "closed S" "closed T" shows "closed (S \ f -` T)" proof- obtain U where "closed U" "(S \ f -` T) = S \ U" using continuous_closedin_preimage[OF contf \closed T\] unfolding closedin_closed by auto then show ?thesis using closed_Int[of S U, OF \closed S\] by auto qed lemma continuous_open_vimage: "open S \ (\x. continuous (at x) f) \ open (f -` S)" by (metis continuous_on_eq_continuous_within open_vimage) lemma continuous_closed_vimage: "closed S \ (\x. continuous (at x) f) \ closed (f -` S)" by (simp add: closed_vimage continuous_on_eq_continuous_within) lemma Times_in_interior_subtopology: assumes "(x, y) \ U" "openin (top_of_set (S \ T)) U" obtains V W where "openin (top_of_set S) V" "x \ V" "openin (top_of_set T) W" "y \ W" "(V \ W) \ U" proof - from assms obtain E where "open E" "U = S \ T \ E" "(x, y) \ E" "x \ S" "y \ T" by (auto simp: openin_open) from open_prod_elim[OF \open E\ \(x, y) \ E\] obtain E1 E2 where "open E1" "open E2" "(x, y) \ E1 \ E2" "E1 \ E2 \ E" by blast show ?thesis proof show "openin (top_of_set S) (E1 \ S)" "openin (top_of_set T) (E2 \ T)" using \open E1\ \open E2\ by (auto simp: openin_open) show "x \ E1 \ S" "y \ E2 \ T" using \(x, y) \ E1 \ E2\ \x \ S\ \y \ T\ by auto show "(E1 \ S) \ (E2 \ T) \ U" using \E1 \ E2 \ E\ \U = _\ by auto qed qed lemma closedin_Times: "closedin (top_of_set S) S' \ closedin (top_of_set T) T' \ closedin (top_of_set (S \ T)) (S' \ T')" unfolding closedin_closed using closed_Times by blast lemma openin_Times: "openin (top_of_set S) S' \ openin (top_of_set T) T' \ openin (top_of_set (S \ T)) (S' \ T')" unfolding openin_open using open_Times by blast lemma openin_Times_eq: fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" shows "openin (top_of_set (S \ T)) (S' \ T') \ S' = {} \ T' = {} \ openin (top_of_set S) S' \ openin (top_of_set T) T'" (is "?lhs = ?rhs") proof (cases "S' = {} \ T' = {}") case True then show ?thesis by auto next case False then obtain x y where "x \ S'" "y \ T'" by blast show ?thesis proof assume ?lhs have "openin (top_of_set S) S'" proof (subst openin_subopen, clarify) show "\U. openin (top_of_set S) U \ x \ U \ U \ S'" if "x \ S'" for x using that \y \ T'\ Times_in_interior_subtopology [OF _ \?lhs\, of x y] by simp (metis mem_Sigma_iff subsetD subsetI) qed moreover have "openin (top_of_set T) T'" proof (subst openin_subopen, clarify) show "\U. openin (top_of_set T) U \ y \ U \ U \ T'" if "y \ T'" for y using that \x \ S'\ Times_in_interior_subtopology [OF _ \?lhs\, of x y] by simp (metis mem_Sigma_iff subsetD subsetI) qed ultimately show ?rhs by simp next assume ?rhs with False show ?lhs by (simp add: openin_Times) qed qed lemma Lim_transform_within_openin: assumes f: "(f \ l) (at a within T)" and "openin (top_of_set T) S" "a \ S" and eq: "\x. \x \ S; x \ a\ \ f x = g x" shows "(g \ l) (at a within T)" proof - have "\\<^sub>F x in at a within T. x \ T \ x \ a" by (simp add: eventually_at_filter) moreover from \openin _ _\ obtain U where "open U" "S = T \ U" by (auto simp: openin_open) then have "a \ U" using \a \ S\ by auto from topological_tendstoD[OF tendsto_ident_at \open U\ \a \ U\] have "\\<^sub>F x in at a within T. x \ U" by auto ultimately have "\\<^sub>F x in at a within T. f x = g x" by eventually_elim (auto simp: \S = _\ eq) with f show ?thesis by (rule Lim_transform_eventually) qed lemma continuous_on_open_gen: assumes "f ` S \ T" shows "continuous_on S f \ (\U. openin (top_of_set T) U \ openin (top_of_set S) (S \ f -` U))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (clarsimp simp add: continuous_openin_preimage_eq openin_open) (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1) next assume R [rule_format]: ?rhs show ?lhs proof (clarsimp simp add: continuous_openin_preimage_eq) fix U::"'a set" assume "open U" then have "openin (top_of_set S) (S \ f -` (U \ T))" by (metis R inf_commute openin_open) then show "openin (top_of_set S) (S \ f -` U)" by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int) qed qed lemma continuous_openin_preimage: "\continuous_on S f; f ` S \ T; openin (top_of_set T) U\ \ openin (top_of_set S) (S \ f -` U)" by (simp add: continuous_on_open_gen) lemma continuous_on_closed_gen: assumes "f ` S \ T" shows "continuous_on S f \ (\U. closedin (top_of_set T) U \ closedin (top_of_set S) (S \ f -` U))" proof - have *: "U \ T \ S \ f -` (T - U) = S - (S \ f -` U)" for U using assms by blast then show ?thesis unfolding continuous_on_open_gen [OF assms] by (metis closedin_def inf.cobounded1 openin_closedin_eq topspace_euclidean_subtopology) qed lemma continuous_closedin_preimage_gen: assumes "continuous_on S f" "f ` S \ T" "closedin (top_of_set T) U" shows "closedin (top_of_set S) (S \ f -` U)" using assms continuous_on_closed_gen by blast lemma continuous_transform_within_openin: assumes "continuous (at a within T) f" and "openin (top_of_set T) S" "a \ S" and eq: "\x. x \ S \ f x = g x" shows "continuous (at a within T) g" using assms by (simp add: Lim_transform_within_openin continuous_within) subsection\<^marker>\tag important\ \The topology generated by some (open) subsets\ text \In the definition below of a generated topology, the \Empty\ case is not necessary, as it follows from \UN\ taking for \K\ the empty set. However, it is convenient to have, and is never a problem in proofs, so I prefer to write it down explicitly. We do not require \UNIV\ to be an open set, as this will not be the case in applications. (We are thinking of a topology on a subset of \UNIV\, the remaining part of \UNIV\ being irrelevant.)\ inductive generate_topology_on for S where Empty: "generate_topology_on S {}" | Int: "generate_topology_on S a \ generate_topology_on S b \ generate_topology_on S (a \ b)" | UN: "(\k. k \ K \ generate_topology_on S k) \ generate_topology_on S (\K)" | Basis: "s \ S \ generate_topology_on S s" lemma istopology_generate_topology_on: "istopology (generate_topology_on S)" unfolding istopology_def by (auto intro: generate_topology_on.intros) text \The basic property of the topology generated by a set \S\ is that it is the smallest topology containing all the elements of \S\:\ lemma generate_topology_on_coarsest: assumes T: "istopology T" "\s. s \ S \ T s" and gen: "generate_topology_on S s0" shows "T s0" using gen by (induct rule: generate_topology_on.induct) (use T in \auto simp: istopology_def\) abbreviation\<^marker>\tag unimportant\ topology_generated_by::"('a set set) \ ('a topology)" where "topology_generated_by S \ topology (generate_topology_on S)" lemma openin_topology_generated_by_iff: "openin (topology_generated_by S) s \ generate_topology_on S s" using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp lemma openin_topology_generated_by: "openin (topology_generated_by S) s \ generate_topology_on S s" using openin_topology_generated_by_iff by auto lemma topology_generated_by_topspace [simp]: "topspace (topology_generated_by S) = (\S)" proof { fix s assume "openin (topology_generated_by S) s" then have "generate_topology_on S s" by (rule openin_topology_generated_by) then have "s \ (\S)" by (induct, auto) } then show "topspace (topology_generated_by S) \ (\S)" unfolding topspace_def by auto next have "generate_topology_on S (\S)" using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp then show "(\S) \ topspace (topology_generated_by S)" unfolding topspace_def using openin_topology_generated_by_iff by auto qed lemma topology_generated_by_Basis: "s \ S \ openin (topology_generated_by S) s" by (simp add: Basis openin_topology_generated_by_iff) lemma generate_topology_on_Inter: "\finite \; \K. K \ \ \ generate_topology_on \ K; \ \ {}\ \ generate_topology_on \ (\\)" by (induction \ rule: finite_induct; force intro: generate_topology_on.intros) subsection\Topology bases and sub-bases\ lemma istopology_base_alt: "istopology (arbitrary union_of P) \ (\S T. (arbitrary union_of P) S \ (arbitrary union_of P) T \ (arbitrary union_of P) (S \ T))" by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union) lemma istopology_base_eq: "istopology (arbitrary union_of P) \ (\S T. P S \ P T \ (arbitrary union_of P) (S \ T))" by (simp add: istopology_base_alt arbitrary_union_of_Int_eq) lemma istopology_base: "(\S T. \P S; P T\ \ P(S \ T)) \ istopology (arbitrary union_of P)" by (simp add: arbitrary_def istopology_base_eq union_of_inc) lemma openin_topology_base_unique: "openin X = arbitrary union_of P \ (\V. P V \ openin X V) \ (\U x. openin X U \ x \ U \ (\V. P V \ x \ V \ V \ U))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (auto simp: union_of_def arbitrary_def) next assume R: ?rhs then have *: "\\\Collect P. \\ = S" if "openin X S" for S using that by (rule_tac x="{V. P V \ V \ S}" in exI) fastforce from R show ?lhs by (fastforce simp add: union_of_def arbitrary_def intro: *) qed lemma topology_base_unique: assumes "\S. P S \ openin X S" "\U x. \openin X U; x \ U\ \ \B. P B \ x \ B \ B \ U" shows "topology (arbitrary union_of P) = X" proof - have "X = topology (openin X)" by (simp add: openin_inverse) also from assms have "openin X = arbitrary union_of P" by (subst openin_topology_base_unique) auto finally show ?thesis .. qed lemma topology_bases_eq_aux: "\(arbitrary union_of P) S; \U x. \P U; x \ U\ \ \V. Q V \ x \ V \ V \ U\ \ (arbitrary union_of Q) S" by (metis arbitrary_union_of_alt arbitrary_union_of_idempot) lemma topology_bases_eq: "\\U x. \P U; x \ U\ \ \V. Q V \ x \ V \ V \ U; \V x. \Q V; x \ V\ \ \U. P U \ x \ U \ U \ V\ \ topology (arbitrary union_of P) = topology (arbitrary union_of Q)" by (fastforce intro: arg_cong [where f=topology] elim: topology_bases_eq_aux) lemma istopology_subbase: "istopology (arbitrary union_of (finite intersection_of P relative_to S))" by (simp add: finite_intersection_of_Int istopology_base relative_to_Int) lemma openin_subbase: "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S \ (arbitrary union_of (finite intersection_of B relative_to U)) S" by (simp add: istopology_subbase topology_inverse') lemma topspace_subbase [simp]: "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _") proof show "?lhs \ U" by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset) show "U \ ?lhs" by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase openin_subset relative_to_inc subset_UNIV topology_inverse') qed lemma minimal_topology_subbase: assumes X: "\S. P S \ openin X S" and "openin X U" and S: "openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S" shows "openin X S" proof - have "(arbitrary union_of (finite intersection_of P relative_to U)) S" using S openin_subbase by blast with X \openin X U\ show ?thesis by (force simp add: union_of_def intersection_of_def relative_to_def intro: openin_Int_Inter) qed lemma istopology_subbase_UNIV: "istopology (arbitrary union_of (finite intersection_of P))" by (simp add: istopology_base finite_intersection_of_Int) lemma generate_topology_on_eq: "generate_topology_on S = arbitrary union_of finite' intersection_of (\x. x \ S)" (is "?lhs = ?rhs") proof (intro ext iffI) fix A assume "?lhs A" then show "?rhs A" proof induction case (Int a b) then show ?case by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base) next case (UN K) then show ?case by (simp add: arbitrary_union_of_Union) next case (Basis s) then show ?case by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset) qed auto next fix A assume "?rhs A" then obtain \ where \: "\T. T \ \ \ \\. finite' \ \ \ \ S \ \\ = T" and eq: "A = \\" unfolding union_of_def intersection_of_def by auto show "?lhs A" unfolding eq proof (rule generate_topology_on.UN) fix T assume "T \ \" with \ obtain \ where "finite' \" "\ \ S" "\\ = T" by blast have "generate_topology_on S (\\)" proof (rule generate_topology_on_Inter) show "finite \" "\ \ {}" by (auto simp: \finite' \\) show "\K. K \ \ \ generate_topology_on S K" by (metis \\ \ S\ generate_topology_on.simps subset_iff) qed then show "generate_topology_on S T" using \\\ = T\ by blast qed qed lemma continuous_on_generated_topo_iff: "continuous_map T1 (topology_generated_by S) f \ ((\U. U \ S \ openin T1 (f-`U \ topspace(T1))) \ (f`(topspace T1) \ (\ S)))" unfolding continuous_map_alt topology_generated_by_topspace proof (auto simp add: topology_generated_by_Basis) assume H: "\U. U \ S \ openin T1 (f -` U \ topspace T1)" fix U assume "openin (topology_generated_by S) U" then have "generate_topology_on S U" by (rule openin_topology_generated_by) then show "openin T1 (f -` U \ topspace T1)" proof (induct) fix a b assume H: "openin T1 (f -` a \ topspace T1)" "openin T1 (f -` b \ topspace T1)" have "f -` (a \ b) \ topspace T1 = (f-`a \ topspace T1) \ (f-`b \ topspace T1)" by auto then show "openin T1 (f -` (a \ b) \ topspace T1)" using H by auto next fix K assume H: "openin T1 (f -` k \ topspace T1)" if "k\ K" for k define L where "L = {f -` k \ topspace T1|k. k \ K}" have *: "openin T1 l" if "l \L" for l using that H unfolding L_def by auto have "openin T1 (\L)" using openin_Union[OF *] by simp moreover have "(\L) = (f -` \K \ topspace T1)" unfolding L_def by auto ultimately show "openin T1 (f -` \K \ topspace T1)" by simp qed (auto simp add: H) qed lemma continuous_on_generated_topo: assumes "\U. U \S \ openin T1 (f-`U \ topspace(T1))" "f`(topspace T1) \ (\ S)" shows "continuous_map T1 (topology_generated_by S) f" using assms continuous_on_generated_topo_iff by blast subsection\<^marker>\tag important\ \Pullback topology\ text \Pulling back a topology by map gives again a topology. \subtopology\ is a special case of this notion, pulling back by the identity. We introduce the general notion as we will need it to define the strong operator topology on the space of continuous linear operators, by pulling back the product topology on the space of all functions.\ text \\pullback_topology A f T\ is the pullback of the topology \T\ by the map \f\ on the set \A\.\ definition\<^marker>\tag important\ pullback_topology::"('a set) \ ('a \ 'b) \ ('b topology) \ ('a topology)" where "pullback_topology A f T = topology (\S. \U. openin T U \ S = f-`U \ A)" lemma istopology_pullback_topology: "istopology (\S. \U. openin T U \ S = f-`U \ A)" unfolding istopology_def proof (auto) fix K assume "\S\K. \U. openin T U \ S = f -` U \ A" then have "\U. \S\K. openin T (U S) \ S = f-`(U S) \ A" by (rule bchoice) then obtain U where U: "\S\K. openin T (U S) \ S = f-`(U S) \ A" by blast define V where "V = (\S\K. U S)" have "openin T V" "\K = f -` V \ A" unfolding V_def using U by auto then show "\V. openin T V \ \K = f -` V \ A" by auto qed lemma openin_pullback_topology: "openin (pullback_topology A f T) S \ (\U. openin T U \ S = f-`U \ A)" unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto lemma topspace_pullback_topology: "topspace (pullback_topology A f T) = f-`(topspace T) \ A" by (auto simp add: topspace_def openin_pullback_topology) proposition continuous_map_pullback [intro]: assumes "continuous_map T1 T2 g" shows "continuous_map (pullback_topology A f T1) T2 (g o f)" unfolding continuous_map_alt proof (auto) fix U::"'b set" assume "openin T2 U" then have "openin T1 (g-`U \ topspace T1)" using assms unfolding continuous_map_alt by auto have "(g o f)-`U \ topspace (pullback_topology A f T1) = (g o f)-`U \ A \ f-`(topspace T1)" unfolding topspace_pullback_topology by auto also have "... = f-`(g-`U \ topspace T1) \ A " by auto also have "openin (pullback_topology A f T1) (...)" unfolding openin_pullback_topology using \openin T1 (g-`U \ topspace T1)\ by auto finally show "openin (pullback_topology A f T1) ((g \ f) -` U \ topspace (pullback_topology A f T1))" by auto next fix x assume "x \ topspace (pullback_topology A f T1)" then have "f x \ topspace T1" unfolding topspace_pullback_topology by auto then show "g (f x) \ topspace T2" using assms unfolding continuous_map_def by auto qed proposition continuous_map_pullback' [intro]: assumes "continuous_map T1 T2 (f o g)" "topspace T1 \ g-`A" shows "continuous_map T1 (pullback_topology A f T2) g" unfolding continuous_map_alt proof (auto) fix U assume "openin (pullback_topology A f T2) U" then have "\V. openin T2 V \ U = f-`V \ A" unfolding openin_pullback_topology by auto then obtain V where "openin T2 V" "U = f-`V \ A" by blast then have "g -` U \ topspace T1 = g-`(f-`V \ A) \ topspace T1" by blast also have "... = (f o g)-`V \ (g-`A \ topspace T1)" by auto also have "... = (f o g)-`V \ topspace T1" using assms(2) by auto also have "openin T1 (...)" using assms(1) \openin T2 V\ by auto finally show "openin T1 (g -` U \ topspace T1)" by simp next fix x assume "x \ topspace T1" have "(f o g) x \ topspace T2" using assms(1) \x \ topspace T1\ unfolding continuous_map_def by auto then have "g x \ f-`(topspace T2)" unfolding comp_def by blast moreover have "g x \ A" using assms(2) \x \ topspace T1\ by blast ultimately show "g x \ topspace (pullback_topology A f T2)" unfolding topspace_pullback_topology by blast qed subsection\Proper maps (not a priori assumed continuous) \ definition proper_map where "proper_map X Y f \ closed_map X Y f \ (\y \ topspace Y. compactin X {x \ topspace X. f x = y})" lemma proper_imp_closed_map: "proper_map X Y f \ closed_map X Y f" by (simp add: proper_map_def) lemma proper_map_imp_subset_topspace: "proper_map X Y f \ f ` (topspace X) \ topspace Y" by (simp add: closed_map_imp_subset_topspace proper_map_def) lemma closed_injective_imp_proper_map: assumes f: "closed_map X Y f" and inj: "inj_on f (topspace X)" shows "proper_map X Y f" unfolding proper_map_def proof (clarsimp simp: f) show "compactin X {x \ topspace X. f x = y}" if "y \ topspace Y" for y using inj_on_eq_iff [OF inj] that proof - have "{x \ topspace X. f x = y} = {} \ (\a \ topspace X. {x \ topspace X. f x = y} = {a})" using inj_on_eq_iff [OF inj] by auto then show ?thesis using that by (metis (no_types, lifting) compactin_empty compactin_sing) qed qed lemma injective_imp_proper_eq_closed_map: "inj_on f (topspace X) \ (proper_map X Y f \ closed_map X Y f)" using closed_injective_imp_proper_map proper_imp_closed_map by blast lemma homeomorphic_imp_proper_map: "homeomorphic_map X Y f \ proper_map X Y f" by (simp add: closed_injective_imp_proper_map homeomorphic_eq_everything_map) lemma compactin_proper_map_preimage: assumes f: "proper_map X Y f" and "compactin Y K" shows "compactin X {x. x \ topspace X \ f x \ K}" proof - have "f ` (topspace X) \ topspace Y" by (simp add: f proper_map_imp_subset_topspace) have *: "\y. y \ topspace Y \ compactin X {x \ topspace X. f x = y}" using f by (auto simp: proper_map_def) show ?thesis unfolding compactin_def proof clarsimp show "\\. finite \ \ \ \ \ \ {x \ topspace X. f x \ K} \ \\" if \: "\U\\. openin X U" and sub: "{x \ topspace X. f x \ K} \ \\" for \ proof - have "\y \ K. \\. finite \ \ \ \ \ \ {x \ topspace X. f x = y} \ \\" proof fix y assume "y \ K" then have "compactin X {x \ topspace X. f x = y}" by (metis "*" \compactin Y K\ compactin_subspace subsetD) with \y \ K\ show "\\. finite \ \ \ \ \ \ {x \ topspace X. f x = y} \ \\" unfolding compactin_def using \ sub by fastforce qed then obtain \ where \: "\y. y \ K \ finite (\ y) \ \ y \ \ \ {x \ topspace X. f x = y} \ \(\ y)" by (metis (full_types)) define F where "F \ \y. topspace Y - f ` (topspace X - \(\ y))" have "\\. finite \ \ \ \ F ` K \ K \ \\" proof (rule compactinD [OF \compactin Y K\]) have "\x. x \ K \ closedin Y (f ` (topspace X - \(\ x)))" using f unfolding proper_map_def closed_map_def by (meson \ \ openin_Union openin_closedin_eq subsetD) then show "openin Y U" if "U \ F ` K" for U using that by (auto simp: F_def) show "K \ \(F ` K)" using \ \compactin Y K\ unfolding F_def compactin_def by fastforce qed then obtain J where "finite J" "J \ K" and J: "K \ \(F ` J)" by (auto simp: ex_finite_subset_image) show ?thesis unfolding F_def proof (intro exI conjI) show "finite (\(\ ` J))" using \ \J \ K\ \finite J\ by blast show "\(\ ` J) \ \" using \ \J \ K\ by blast show "{x \ topspace X. f x \ K} \ \(\(\ ` J))" using J \J \ K\ unfolding F_def by auto qed qed qed qed lemma compact_space_proper_map_preimage: assumes f: "proper_map X Y f" and fim: "f ` (topspace X) = topspace Y" and "compact_space Y" shows "compact_space X" proof - have eq: "topspace X = {x \ topspace X. f x \ topspace Y}" using fim by blast moreover have "compactin Y (topspace Y)" using \compact_space Y\ compact_space_def by auto ultimately show ?thesis unfolding compact_space_def using eq f compactin_proper_map_preimage by fastforce qed lemma proper_map_alt: "proper_map X Y f \ closed_map X Y f \ (\K. compactin Y K \ compactin X {x. x \ topspace X \ f x \ K})" proof (intro iffI conjI allI impI) show "compactin X {x \ topspace X. f x \ K}" if "proper_map X Y f" and "compactin Y K" for K using that by (simp add: compactin_proper_map_preimage) show "proper_map X Y f" if f: "closed_map X Y f \ (\K. compactin Y K \ compactin X {x \ topspace X. f x \ K})" proof - have "compactin X {x \ topspace X. f x = y}" if "y \ topspace Y" for y proof - have "compactin X {x \ topspace X. f x \ {y}}" using f compactin_sing that by fastforce then show ?thesis by auto qed with f show ?thesis by (auto simp: proper_map_def) qed qed (simp add: proper_imp_closed_map) lemma proper_map_on_empty: "topspace X = {} \ proper_map X Y f" by (auto simp: proper_map_def closed_map_on_empty) lemma proper_map_id [simp]: "proper_map X X id" proof (clarsimp simp: proper_map_alt closed_map_id) fix K assume K: "compactin X K" then have "{a \ topspace X. a \ K} = K" by (simp add: compactin_subspace subset_antisym subset_iff) then show "compactin X {a \ topspace X. a \ K}" using K by auto qed lemma proper_map_compose: assumes "proper_map X Y f" "proper_map Y Z g" shows "proper_map X Z (g \ f)" proof - have "closed_map X Y f" and f: "\K. compactin Y K \ compactin X {x \ topspace X. f x \ K}" and "closed_map Y Z g" and g: "\K. compactin Z K \ compactin Y {x \ topspace Y. g x \ K}" using assms by (auto simp: proper_map_alt) show ?thesis unfolding proper_map_alt proof (intro conjI allI impI) show "closed_map X Z (g \ f)" using \closed_map X Y f\ \closed_map Y Z g\ closed_map_compose by blast have "{x \ topspace X. g (f x) \ K} = {x \ topspace X. f x \ {b \ topspace Y. g b \ K}}" for K using \closed_map X Y f\ closed_map_imp_subset_topspace by blast then show "compactin X {x \ topspace X. (g \ f) x \ K}" if "compactin Z K" for K using f [OF g [OF that]] by auto qed qed lemma proper_map_const: "proper_map X Y (\x. c) \ compact_space X \ (topspace X = {} \ closedin Y {c})" proof (cases "topspace X = {}") case True then show ?thesis by (simp add: compact_space_topspace_empty proper_map_on_empty) next case False have *: "compactin X {x \ topspace X. c = y}" if "compact_space X" for y using that unfolding compact_space_def by (metis (mono_tags, lifting) compactin_empty empty_subsetI mem_Collect_eq subsetI subset_antisym) then show ?thesis using closed_compactin closedin_subset by (force simp: False proper_map_def closed_map_const compact_space_def) qed lemma proper_map_inclusion: "S \ topspace X \ proper_map (subtopology X S) X id \ closedin X S \ (\k. compactin X k \ compactin X (S \ k))" by (metis closed_Int_compactin closed_map_inclusion_eq inf.absorb_iff2 inj_on_id injective_imp_proper_eq_closed_map) subsection\Perfect maps (proper, continuous and surjective)\ definition perfect_map where "perfect_map X Y f \ continuous_map X Y f \ proper_map X Y f \ f ` (topspace X) = topspace Y" lemma homeomorphic_imp_perfect_map: "homeomorphic_map X Y f \ perfect_map X Y f" by (simp add: homeomorphic_eq_everything_map homeomorphic_imp_proper_map perfect_map_def) lemma perfect_imp_quotient_map: "perfect_map X Y f \ quotient_map X Y f" by (simp add: continuous_closed_imp_quotient_map perfect_map_def proper_map_def) lemma homeomorphic_eq_injective_perfect_map: "homeomorphic_map X Y f \ perfect_map X Y f \ inj_on f (topspace X)" using homeomorphic_imp_perfect_map homeomorphic_map_def perfect_imp_quotient_map by blast lemma perfect_injective_eq_homeomorphic_map: "perfect_map X Y f \ inj_on f (topspace X) \ homeomorphic_map X Y f" by (simp add: homeomorphic_eq_injective_perfect_map) lemma perfect_map_id [simp]: "perfect_map X X id" by (simp add: homeomorphic_imp_perfect_map) lemma perfect_map_compose: "\perfect_map X Y f; perfect_map Y Z g\ \ perfect_map X Z (g \ f)" by (meson continuous_map_compose perfect_imp_quotient_map perfect_map_def proper_map_compose quotient_map_compose_eq quotient_map_def) lemma perfect_imp_continuous_map: "perfect_map X Y f \ continuous_map X Y f" using perfect_map_def by blast lemma perfect_imp_closed_map: "perfect_map X Y f \ closed_map X Y f" by (simp add: perfect_map_def proper_map_def) lemma perfect_imp_proper_map: "perfect_map X Y f \ proper_map X Y f" by (simp add: perfect_map_def) lemma perfect_imp_surjective_map: "perfect_map X Y f \ f ` (topspace X) = topspace Y" by (simp add: perfect_map_def) end diff --git a/src/HOL/Analysis/Analysis.thy b/src/HOL/Analysis/Analysis.thy --- a/src/HOL/Analysis/Analysis.thy +++ b/src/HOL/Analysis/Analysis.thy @@ -1,54 +1,56 @@ theory Analysis imports (* Linear Algebra *) Convex Determinants (* Topology *) + FSigma + Sum_Topology Connected Abstract_Limits Isolated (* Functional Analysis *) Elementary_Normed_Spaces Norm_Arith (* Vector Analysis *) Convex_Euclidean_Space Operator_Norm (* Unsorted *) Line_Segment Derivative Cartesian_Euclidean_Space Weierstrass_Theorems (* Measure and Integration Theory *) Ball_Volume Integral_Test Improper_Integral Equivalence_Measurable_On_Borel Lebesgue_Integral_Substitution Embed_Measure Complete_Measure Radon_Nikodym Fashoda_Theorem Cross3 Homeomorphism Bounded_Continuous_Function Abstract_Topology Product_Topology Lindelof_Spaces Infinite_Products Infinite_Sum Infinite_Set_Sum Polytope Jordan_Curve Poly_Roots Generalised_Binomial_Theorem Gamma_Function Change_Of_Vars Multivariate_Analysis Simplex_Content FPS_Convergence Smooth_Paths Abstract_Euclidean_Space Function_Metric begin end diff --git a/src/HOL/Analysis/FSigma.thy b/src/HOL/Analysis/FSigma.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Analysis/FSigma.thy @@ -0,0 +1,236 @@ +(* Author: L C Paulson, University of Cambridge [ported from HOL Light, metric.ml] *) + +section \$F$-Sigma and $G$-Delta sets in a Topological Space\ + +text \An $F$-sigma set is a countable union of closed sets; a $G$-delta set is the dual.\ + +theory FSigma + imports Abstract_Topology +begin + + +definition fsigma_in + where "fsigma_in X \ countable union_of closedin X" + +definition gdelta_in + where "gdelta_in X \ (countable intersection_of openin X) relative_to topspace X" + +lemma fsigma_in_ascending: + "fsigma_in X S \ (\C. (\n. closedin X (C n)) \ (\n. C n \ C(Suc n)) \ \ (range C) = S)" + unfolding fsigma_in_def + by (metis closedin_Un countable_union_of_ascending closedin_empty) + +lemma gdelta_in_alt: + "gdelta_in X S \ S \ topspace X \ (countable intersection_of openin X) S" +proof - + have "(countable intersection_of openin X) (topspace X)" + by (simp add: countable_intersection_of_inc) + then show ?thesis + unfolding gdelta_in_def + by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset) +qed + +lemma fsigma_in_subset: "fsigma_in X S \ S \ topspace X" + using closedin_subset by (fastforce simp: fsigma_in_def union_of_def subset_iff) + +lemma gdelta_in_subset: "gdelta_in X S \ S \ topspace X" + by (simp add: gdelta_in_alt) + +lemma closed_imp_fsigma_in: "closedin X S \ fsigma_in X S" + by (simp add: countable_union_of_inc fsigma_in_def) + +lemma open_imp_gdelta_in: "openin X S \ gdelta_in X S" + by (simp add: countable_intersection_of_inc gdelta_in_alt openin_subset) + +lemma fsigma_in_empty [iff]: "fsigma_in X {}" + by (simp add: closed_imp_fsigma_in) + +lemma gdelta_in_empty [iff]: "gdelta_in X {}" + by (simp add: open_imp_gdelta_in) + +lemma fsigma_in_topspace [iff]: "fsigma_in X (topspace X)" + by (simp add: closed_imp_fsigma_in) + +lemma gdelta_in_topspace [iff]: "gdelta_in X (topspace X)" + by (simp add: open_imp_gdelta_in) + +lemma fsigma_in_Union: + "\countable T; \S. S \ T \ fsigma_in X S\ \ fsigma_in X (\ T)" + by (simp add: countable_union_of_Union fsigma_in_def) + +lemma fsigma_in_Un: + "\fsigma_in X S; fsigma_in X T\ \ fsigma_in X (S \ T)" + by (simp add: countable_union_of_Un fsigma_in_def) + +lemma fsigma_in_Int: + "\fsigma_in X S; fsigma_in X T\ \ fsigma_in X (S \ T)" + by (simp add: closedin_Int countable_union_of_Int fsigma_in_def) + +lemma gdelta_in_Inter: + "\countable T; T\{}; \S. S \ T \ gdelta_in X S\ \ gdelta_in X (\ T)" + by (simp add: Inf_less_eq countable_intersection_of_Inter gdelta_in_alt) + +lemma gdelta_in_Int: + "\gdelta_in X S; gdelta_in X T\ \ gdelta_in X (S \ T)" + by (simp add: countable_intersection_of_inter gdelta_in_alt le_infI2) + +lemma gdelta_in_Un: + "\gdelta_in X S; gdelta_in X T\ \ gdelta_in X (S \ T)" + by (simp add: countable_intersection_of_union gdelta_in_alt openin_Un) + +lemma fsigma_in_diff: + assumes "fsigma_in X S" "gdelta_in X T" + shows "fsigma_in X (S - T)" +proof - + have [simp]: "S - (S \ T) = S - T" for S T :: "'a set" + by auto + have [simp]: "topspace X - \\ = (\T\\. topspace X - T)" for \ + by auto + have "\\. \countable \; \ \ Collect (openin X)\ \ + (countable union_of closedin X) (\ ((-) (topspace X) ` \))" + by (metis Ball_Collect countable_union_of_UN countable_union_of_inc openin_closedin_eq) + then have "\S. gdelta_in X S \ fsigma_in X (topspace X - S)" + by (simp add: fsigma_in_def gdelta_in_def all_relative_to all_intersection_of del: UN_simps) + then show ?thesis + by (metis Diff_Int2 Diff_Int_distrib2 assms fsigma_in_Int fsigma_in_subset inf.absorb_iff2) +qed + +lemma gdelta_in_diff: + assumes "gdelta_in X S" "fsigma_in X T" + shows "gdelta_in X (S - T)" +proof - + have [simp]: "topspace X - \\ = topspace X \ (\T\\. topspace X - T)" for \ + by auto + have "\\. \countable \; \ \ Collect (closedin X)\ + \ (countable intersection_of openin X relative_to topspace X) + (topspace X \ \ ((-) (topspace X) ` \))" + by (metis Ball_Collect closedin_def countable_intersection_of_INT countable_intersection_of_inc relative_to_inc) + then have "\S. fsigma_in X S \ gdelta_in X (topspace X - S)" + by (simp add: fsigma_in_def gdelta_in_def all_union_of del: INT_simps) + then show ?thesis + by (metis Diff_Int2 Diff_Int_distrib2 assms gdelta_in_Int gdelta_in_alt inf.orderE inf_commute) +qed + +lemma gdelta_in_fsigma_in: + "gdelta_in X S \ S \ topspace X \ fsigma_in X (topspace X - S)" + by (metis double_diff fsigma_in_diff fsigma_in_topspace gdelta_in_alt gdelta_in_diff gdelta_in_topspace) + +lemma fsigma_in_gdelta_in: + "fsigma_in X S \ S \ topspace X \ gdelta_in X (topspace X - S)" + by (metis Diff_Diff_Int fsigma_in_subset gdelta_in_fsigma_in inf.absorb_iff2) + +lemma gdelta_in_descending: + "gdelta_in X S \ (\C. (\n. openin X (C n)) \ (\n. C(Suc n) \ C n) \ \(range C) = S)" (is "?lhs=?rhs") +proof + assume ?lhs + then obtain C where C: "S \ topspace X" "\n. closedin X (C n)" + "\n. C n \ C(Suc n)" "\(range C) = topspace X - S" + by (meson fsigma_in_ascending gdelta_in_fsigma_in) + define D where "D \ \n. topspace X - C n" + have "\n. openin X (D n) \ D (Suc n) \ D n" + by (simp add: Diff_mono C D_def openin_diff) + moreover have "\(range D) = S" + by (simp add: Diff_Diff_Int Int_absorb1 C D_def) + ultimately show ?rhs + by metis +next + assume ?rhs + then obtain C where "S \ topspace X" + and C: "\n. openin X (C n)" "\n. C(Suc n) \ C n" "\(range C) = S" + using openin_subset by fastforce + define D where "D \ \n. topspace X - C n" + have "\n. closedin X (D n) \ D n \ D(Suc n)" + by (simp add: Diff_mono C closedin_diff D_def) + moreover have "\(range D) = topspace X - S" + using C D_def by blast + ultimately show ?lhs + by (metis \S \ topspace X\ fsigma_in_ascending gdelta_in_fsigma_in) +qed + +lemma homeomorphic_map_fsigmaness: + assumes f: "homeomorphic_map X Y f" and "U \ topspace X" + shows "fsigma_in Y (f ` U) \ fsigma_in X U" (is "?lhs=?rhs") +proof - + obtain g where g: "homeomorphic_maps X Y f g" and g: "homeomorphic_map Y X g" + and 1: "(\x \ topspace X. g(f x) = x)" and 2: "(\y \ topspace Y. f(g y) = y)" + using assms homeomorphic_map_maps by (metis homeomorphic_maps_map) + show ?thesis + proof + assume ?lhs + then obtain \ where "countable \" and \: "\ \ Collect (closedin Y)" "\\ = f`U" + by (force simp: fsigma_in_def union_of_def) + define \ where "\ \ image (image g) \" + have "countable \" + using \_def \countable \\ by blast + moreover have "\ \ Collect (closedin X)" + using f g homeomorphic_map_closedness_eq \ unfolding \_def by blast + moreover have "\\ \ U" + unfolding \_def by (smt (verit) assms 1 \ image_Union image_iff in_mono subsetI) + moreover have "U \ \\" + unfolding \_def using assms \ + by (smt (verit, del_insts) "1" imageI image_Union subset_iff) + ultimately show ?rhs + by (metis fsigma_in_def subset_antisym union_of_def) + next + assume ?rhs + then obtain \ where "countable \" and \: "\ \ Collect (closedin X)" "\\ = U" + by (auto simp: fsigma_in_def union_of_def) + define \ where "\ \ image (image f) \" + have "countable \" + using \_def \countable \\ by blast + moreover have "\ \ Collect (closedin Y)" + using f g homeomorphic_map_closedness_eq \ unfolding \_def by blast + moreover have "\\ = f`U" + unfolding \_def using \ by blast + ultimately show ?lhs + by (metis fsigma_in_def union_of_def) + qed +qed + +lemma homeomorphic_map_fsigmaness_eq: + "homeomorphic_map X Y f + \ (fsigma_in X U \ U \ topspace X \ fsigma_in Y (f ` U))" + by (metis fsigma_in_subset homeomorphic_map_fsigmaness) + +lemma homeomorphic_map_gdeltaness: + assumes "homeomorphic_map X Y f" "U \ topspace X" + shows "gdelta_in Y (f ` U) \ gdelta_in X U" +proof - + have "topspace Y - f ` U = f ` (topspace X - U)" + by (metis (no_types, lifting) Diff_subset assms homeomorphic_eq_everything_map inj_on_image_set_diff) + then show ?thesis + using assms homeomorphic_imp_surjective_map + by (fastforce simp: gdelta_in_fsigma_in homeomorphic_map_fsigmaness_eq) +qed + +lemma homeomorphic_map_gdeltaness_eq: + "homeomorphic_map X Y f + \ gdelta_in X U \ U \ topspace X \ gdelta_in Y (f ` U)" + by (meson gdelta_in_subset homeomorphic_map_gdeltaness) + +lemma fsigma_in_relative_to: + "(fsigma_in X relative_to S) = fsigma_in (subtopology X S)" + by (simp add: fsigma_in_def countable_union_of_relative_to closedin_relative_to) + +lemma fsigma_in_subtopology: + "fsigma_in (subtopology X U) S \ (\T. fsigma_in X T \ S = T \ U)" + by (metis fsigma_in_relative_to inf_commute relative_to_def) + +lemma gdelta_in_relative_to: + "(gdelta_in X relative_to S) = gdelta_in (subtopology X S)" + apply (simp add: gdelta_in_def) + by (metis countable_intersection_of_relative_to openin_relative_to subtopology_restrict) + +lemma gdelta_in_subtopology: + "gdelta_in (subtopology X U) S \ (\T. gdelta_in X T \ S = T \ U)" + by (metis gdelta_in_relative_to inf_commute relative_to_def) + +lemma fsigma_in_fsigma_subtopology: + "fsigma_in X S \ (fsigma_in (subtopology X S) T \ fsigma_in X T \ T \ S)" + by (metis fsigma_in_Int fsigma_in_gdelta_in fsigma_in_subtopology inf.orderE topspace_subtopology_subset) + +lemma gdelta_in_gdelta_subtopology: + "gdelta_in X S \ (gdelta_in (subtopology X S) T \ gdelta_in X T \ T \ S)" + by (metis gdelta_in_Int gdelta_in_subset gdelta_in_subtopology inf.orderE topspace_subtopology_subset) + +end diff --git a/src/HOL/Analysis/Product_Topology.thy b/src/HOL/Analysis/Product_Topology.thy --- a/src/HOL/Analysis/Product_Topology.thy +++ b/src/HOL/Analysis/Product_Topology.thy @@ -1,580 +1,580 @@ section\The binary product topology\ theory Product_Topology -imports Function_Topology + imports Function_Topology begin section \Product Topology\ subsection\Definition\ definition prod_topology :: "'a topology \ 'b topology \ ('a \ 'b) topology" where "prod_topology X Y \ topology (arbitrary union_of (\U. U \ {S \ T |S T. openin X S \ openin Y T}))" lemma open_product_open: assumes "open A" shows "\\. \ \ {S \ T |S T. open S \ open T} \ \ \ = A" proof - obtain f g where *: "\u. u \ A \ open (f u) \ open (g u) \ u \ (f u) \ (g u) \ (f u) \ (g u) \ A" using open_prod_def [of A] assms by metis let ?\ = "(\u. f u \ g u) ` A" show ?thesis by (rule_tac x="?\" in exI) (auto simp: dest: *) qed lemma open_product_open_eq: "(arbitrary union_of (\U. \S T. U = S \ T \ open S \ open T)) = open" by (force simp: union_of_def arbitrary_def intro: open_product_open open_Times) lemma openin_prod_topology: "openin (prod_topology X Y) = arbitrary union_of (\U. U \ {S \ T |S T. openin X S \ openin Y T})" unfolding prod_topology_def proof (rule topology_inverse') show "istopology (arbitrary union_of (\U. U \ {S \ T |S T. openin X S \ openin Y T}))" apply (rule istopology_base, simp) by (metis openin_Int Times_Int_Times) qed lemma topspace_prod_topology [simp]: "topspace (prod_topology X Y) = topspace X \ topspace Y" proof - have "topspace(prod_topology X Y) = \ (Collect (openin (prod_topology X Y)))" (is "_ = ?Z") unfolding topspace_def .. also have "\ = topspace X \ topspace Y" proof show "?Z \ topspace X \ topspace Y" apply (auto simp: openin_prod_topology union_of_def arbitrary_def) using openin_subset by force+ next have *: "\A B. topspace X \ topspace Y = A \ B \ openin X A \ openin Y B" by blast show "topspace X \ topspace Y \ ?Z" apply (rule Union_upper) using * by (simp add: openin_prod_topology arbitrary_union_of_inc) qed finally show ?thesis . qed lemma subtopology_Times: shows "subtopology (prod_topology X Y) (S \ T) = prod_topology (subtopology X S) (subtopology Y T)" proof - have "((\U. \S T. U = S \ T \ openin X S \ openin Y T) relative_to S \ T) = (\U. \S' T'. U = S' \ T' \ (openin X relative_to S) S' \ (openin Y relative_to T) T')" by (auto simp: relative_to_def Times_Int_Times fun_eq_iff) metis then show ?thesis by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to) qed lemma prod_topology_subtopology: "prod_topology (subtopology X S) Y = subtopology (prod_topology X Y) (S \ topspace Y)" "prod_topology X (subtopology Y T) = subtopology (prod_topology X Y) (topspace X \ T)" by (auto simp: subtopology_Times) lemma prod_topology_discrete_topology: "discrete_topology (S \ T) = prod_topology (discrete_topology S) (discrete_topology T)" by (auto simp: discrete_topology_unique openin_prod_topology intro: arbitrary_union_of_inc) lemma prod_topology_euclidean [simp]: "prod_topology euclidean euclidean = euclidean" by (simp add: prod_topology_def open_product_open_eq) lemma prod_topology_subtopology_eu [simp]: "prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \ T)" by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times) lemma openin_prod_topology_alt: "openin (prod_topology X Y) S \ (\x y. (x,y) \ S \ (\U V. openin X U \ openin Y V \ x \ U \ y \ V \ U \ V \ S))" apply (auto simp: openin_prod_topology arbitrary_union_of_alt, fastforce) by (metis mem_Sigma_iff) lemma open_map_fst: "open_map (prod_topology X Y) X fst" unfolding open_map_def openin_prod_topology_alt by (force simp: openin_subopen [of X "fst ` _"] intro: subset_fst_imageI) lemma open_map_snd: "open_map (prod_topology X Y) Y snd" unfolding open_map_def openin_prod_topology_alt by (force simp: openin_subopen [of Y "snd ` _"] intro: subset_snd_imageI) lemma openin_prod_Times_iff: "openin (prod_topology X Y) (S \ T) \ S = {} \ T = {} \ openin X S \ openin Y T" proof (cases "S = {} \ T = {}") case False then show ?thesis apply (simp add: openin_prod_topology_alt openin_subopen [of X S] openin_subopen [of Y T] times_subset_iff, safe) apply (meson|force)+ done qed force lemma closure_of_Times: "(prod_topology X Y) closure_of (S \ T) = (X closure_of S) \ (Y closure_of T)" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" by (clarsimp simp: closure_of_def openin_prod_topology_alt) blast show "?rhs \ ?lhs" by (clarsimp simp: closure_of_def openin_prod_topology_alt) (meson SigmaI subsetD) qed lemma closedin_prod_Times_iff: "closedin (prod_topology X Y) (S \ T) \ S = {} \ T = {} \ closedin X S \ closedin Y T" by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq) lemma interior_of_Times: "(prod_topology X Y) interior_of (S \ T) = (X interior_of S) \ (Y interior_of T)" proof (rule interior_of_unique) show "(X interior_of S) \ Y interior_of T \ S \ T" by (simp add: Sigma_mono interior_of_subset) show "openin (prod_topology X Y) ((X interior_of S) \ Y interior_of T)" by (simp add: openin_prod_Times_iff) next show "T' \ (X interior_of S) \ Y interior_of T" if "T' \ S \ T" "openin (prod_topology X Y) T'" for T' proof (clarsimp; intro conjI) fix a :: "'a" and b :: "'b" assume "(a, b) \ T'" with that obtain U V where UV: "openin X U" "openin Y V" "a \ U" "b \ V" "U \ V \ T'" by (metis openin_prod_topology_alt) then show "a \ X interior_of S" using interior_of_maximal_eq that(1) by fastforce show "b \ Y interior_of T" using UV interior_of_maximal_eq that(1) by (metis SigmaI mem_Sigma_iff subset_eq) qed qed subsection \Continuity\ lemma continuous_map_pairwise: "continuous_map Z (prod_topology X Y) f \ continuous_map Z X (fst \ f) \ continuous_map Z Y (snd \ f)" (is "?lhs = ?rhs") proof - let ?g = "fst \ f" and ?h = "snd \ f" have f: "f x = (?g x, ?h x)" for x by auto show ?thesis proof (cases "(\x \ topspace Z. ?g x \ topspace X) \ (\x \ topspace Z. ?h x \ topspace Y)") case True show ?thesis proof safe assume "continuous_map Z (prod_topology X Y) f" then have "openin Z {x \ topspace Z. fst (f x) \ U}" if "openin X U" for U unfolding continuous_map_def using True that apply clarify apply (drule_tac x="U \ topspace Y" in spec) by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong) with True show "continuous_map Z X (fst \ f)" by (auto simp: continuous_map_def) next assume "continuous_map Z (prod_topology X Y) f" then have "openin Z {x \ topspace Z. snd (f x) \ V}" if "openin Y V" for V unfolding continuous_map_def using True that apply clarify apply (drule_tac x="topspace X \ V" in spec) by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong) with True show "continuous_map Z Y (snd \ f)" by (auto simp: continuous_map_def) next assume Z: "continuous_map Z X (fst \ f)" "continuous_map Z Y (snd \ f)" have *: "openin Z {x \ topspace Z. f x \ W}" if "\w. w \ W \ \U V. openin X U \ openin Y V \ w \ U \ V \ U \ V \ W" for W proof (subst openin_subopen, clarify) fix x :: "'a" assume "x \ topspace Z" and "f x \ W" with that [OF \f x \ W\] obtain U V where UV: "openin X U" "openin Y V" "f x \ U \ V" "U \ V \ W" by auto with Z UV show "\T. openin Z T \ x \ T \ T \ {x \ topspace Z. f x \ W}" apply (rule_tac x="{x \ topspace Z. ?g x \ U} \ {x \ topspace Z. ?h x \ V}" in exI) apply (auto simp: \x \ topspace Z\ continuous_map_def) done qed show "continuous_map Z (prod_topology X Y) f" using True by (simp add: continuous_map_def openin_prod_topology_alt mem_Times_iff *) qed qed (auto simp: continuous_map_def) qed lemma continuous_map_paired: "continuous_map Z (prod_topology X Y) (\x. (f x,g x)) \ continuous_map Z X f \ continuous_map Z Y g" by (simp add: continuous_map_pairwise o_def) lemma continuous_map_pairedI [continuous_intros]: "\continuous_map Z X f; continuous_map Z Y g\ \ continuous_map Z (prod_topology X Y) (\x. (f x,g x))" by (simp add: continuous_map_pairwise o_def) lemma continuous_map_fst [continuous_intros]: "continuous_map (prod_topology X Y) X fst" using continuous_map_pairwise [of "prod_topology X Y" X Y id] by (simp add: continuous_map_pairwise) lemma continuous_map_snd [continuous_intros]: "continuous_map (prod_topology X Y) Y snd" using continuous_map_pairwise [of "prod_topology X Y" X Y id] by (simp add: continuous_map_pairwise) lemma continuous_map_fst_of [continuous_intros]: "continuous_map Z (prod_topology X Y) f \ continuous_map Z X (fst \ f)" by (simp add: continuous_map_pairwise) lemma continuous_map_snd_of [continuous_intros]: "continuous_map Z (prod_topology X Y) f \ continuous_map Z Y (snd \ f)" by (simp add: continuous_map_pairwise) lemma continuous_map_prod_fst: "i \ I \ continuous_map (prod_topology (product_topology (\i. Y) I) X) Y (\x. fst x i)" using continuous_map_componentwise_UNIV continuous_map_fst by fastforce lemma continuous_map_prod_snd: "i \ I \ continuous_map (prod_topology X (product_topology (\i. Y) I)) Y (\x. snd x i)" using continuous_map_componentwise_UNIV continuous_map_snd by fastforce lemma continuous_map_if_iff [simp]: "continuous_map X Y (\x. if P then f x else g x) \ continuous_map X Y (if P then f else g)" by simp lemma continuous_map_if [continuous_intros]: "\P \ continuous_map X Y f; ~P \ continuous_map X Y g\ \ continuous_map X Y (\x. if P then f x else g x)" by simp lemma continuous_map_subtopology_fst [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) X fst" using continuous_map_from_subtopology continuous_map_fst by force lemma continuous_map_subtopology_snd [continuous_intros]: "continuous_map (subtopology (prod_topology X Y) Z) Y snd" using continuous_map_from_subtopology continuous_map_snd by force lemma quotient_map_fst [simp]: "quotient_map(prod_topology X Y) X fst \ (topspace Y = {} \ topspace X = {})" by (auto simp: continuous_open_quotient_map open_map_fst continuous_map_fst) lemma quotient_map_snd [simp]: "quotient_map(prod_topology X Y) Y snd \ (topspace X = {} \ topspace Y = {})" by (auto simp: continuous_open_quotient_map open_map_snd continuous_map_snd) lemma retraction_map_fst: "retraction_map (prod_topology X Y) X fst \ (topspace Y = {} \ topspace X = {})" proof (cases "topspace Y = {}") case True then show ?thesis using continuous_map_image_subset_topspace by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty) next case False have "\g. continuous_map X (prod_topology X Y) g \ (\x\topspace X. fst (g x) = x)" if y: "y \ topspace Y" for y by (rule_tac x="\x. (x,y)" in exI) (auto simp: y continuous_map_paired) with False have "retraction_map (prod_topology X Y) X fst" by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst) with False show ?thesis by simp qed lemma retraction_map_snd: "retraction_map (prod_topology X Y) Y snd \ (topspace X = {} \ topspace Y = {})" proof (cases "topspace X = {}") case True then show ?thesis using continuous_map_image_subset_topspace by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst continuous_map_on_empty) next case False have "\g. continuous_map Y (prod_topology X Y) g \ (\y\topspace Y. snd (g y) = y)" if x: "x \ topspace X" for x by (rule_tac x="\y. (x,y)" in exI) (auto simp: x continuous_map_paired) with False have "retraction_map (prod_topology X Y) Y snd" by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_snd) with False show ?thesis by simp qed lemma continuous_map_of_fst: "continuous_map (prod_topology X Y) Z (f \ fst) \ topspace Y = {} \ continuous_map X Z f" proof (cases "topspace Y = {}") case True then show ?thesis by (simp add: continuous_map_on_empty) next case False then show ?thesis by (simp add: continuous_compose_quotient_map_eq) qed lemma continuous_map_of_snd: "continuous_map (prod_topology X Y) Z (f \ snd) \ topspace X = {} \ continuous_map Y Z f" proof (cases "topspace X = {}") case True then show ?thesis by (simp add: continuous_map_on_empty) next case False then show ?thesis by (simp add: continuous_compose_quotient_map_eq) qed lemma continuous_map_prod_top: "continuous_map (prod_topology X Y) (prod_topology X' Y') (\(x,y). (f x, g y)) \ topspace (prod_topology X Y) = {} \ continuous_map X X' f \ continuous_map Y Y' g" proof (cases "topspace (prod_topology X Y) = {}") case True then show ?thesis by (simp add: continuous_map_on_empty) next case False then show ?thesis by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def]) qed lemma in_prod_topology_closure_of: assumes "z \ (prod_topology X Y) closure_of S" shows "fst z \ X closure_of (fst ` S)" "snd z \ Y closure_of (snd ` S)" using assms continuous_map_eq_image_closure_subset continuous_map_fst apply fastforce using assms continuous_map_eq_image_closure_subset continuous_map_snd apply fastforce done proposition compact_space_prod_topology: "compact_space(prod_topology X Y) \ topspace(prod_topology X Y) = {} \ compact_space X \ compact_space Y" proof (cases "topspace(prod_topology X Y) = {}") case True then show ?thesis using compact_space_topspace_empty by blast next case False then have non_mt: "topspace X \ {}" "topspace Y \ {}" by auto have "compact_space X" "compact_space Y" if "compact_space(prod_topology X Y)" proof - have "compactin X (fst ` (topspace X \ topspace Y))" by (metis compact_space_def continuous_map_fst image_compactin that topspace_prod_topology) moreover have "compactin Y (snd ` (topspace X \ topspace Y))" by (metis compact_space_def continuous_map_snd image_compactin that topspace_prod_topology) ultimately show "compact_space X" "compact_space Y" by (simp_all add: non_mt compact_space_def) qed moreover define \ where "\ \ (\V. topspace X \ V) ` Collect (openin Y)" define \ where "\ \ (\U. U \ topspace Y) ` Collect (openin X)" have "compact_space(prod_topology X Y)" if "compact_space X" "compact_space Y" proof (rule Alexander_subbase_alt) show toptop: "topspace X \ topspace Y \ \(\ \ \)" unfolding \_def \_def by auto fix \ :: "('a \ 'b) set set" assume \: "\ \ \ \ \" "topspace X \ topspace Y \ \\" then obtain \' \' where XY: "\' \ \" "\' \ \" and \eq: "\ = \' \ \'" using subset_UnE by metis then have sub: "topspace X \ topspace Y \ \(\' \ \')" using \ by simp obtain \ \ where \: "\U. U \ \ \ openin X U" "\' = (\U. U \ topspace Y) ` \" and \: "\V. V \ \ \ openin Y V" "\' = (\V. topspace X \ V) ` \" using XY by (clarsimp simp add: \_def \_def subset_image_iff) (force simp add: subset_iff) have "\\. finite \ \ \ \ \' \ \' \ topspace X \ topspace Y \ \ \" proof - have "topspace X \ \\ \ topspace Y \ \\" using \ \ \ \eq by auto then have *: "\\. finite \ \ (\x \ \. x \ (\V. topspace X \ V) ` \ \ x \ (\U. U \ topspace Y) ` \) \ (topspace X \ topspace Y \ \\)" proof assume "topspace X \ \\" with \compact_space X\ \ obtain \ where "finite \" "\ \ \" "topspace X \ \\" by (meson compact_space_alt) with that show ?thesis by (rule_tac x="(\D. D \ topspace Y) ` \" in exI) auto next assume "topspace Y \ \\" with \compact_space Y\ \ obtain \ where "finite \" "\ \ \" "topspace Y \ \\" by (meson compact_space_alt) with that show ?thesis by (rule_tac x="(\C. topspace X \ C) ` \" in exI) auto qed then show ?thesis using that \ \ by blast qed then show "\\. finite \ \ \ \ \ \ topspace X \ topspace Y \ \ \" using \ \eq by blast next have "(finite intersection_of (\x. x \ \ \ x \ \) relative_to topspace X \ topspace Y) = (\U. \S T. U = S \ T \ openin X S \ openin Y T)" (is "?lhs = ?rhs") proof - have "?rhs U" if "?lhs U" for U proof - have "topspace X \ topspace Y \ \ T \ {A \ B |A B. A \ Collect (openin X) \ B \ Collect (openin Y)}" if "finite T" "T \ \ \ \" for T using that proof induction case (insert B \) then show ?case unfolding \_def \_def apply (simp add: Int_ac subset_eq image_def) apply (metis (no_types) openin_Int openin_topspace Times_Int_Times) done qed auto then show ?thesis using that by (auto simp: subset_eq elim!: relative_toE intersection_ofE) qed moreover have "?lhs Z" if Z: "?rhs Z" for Z proof - obtain U V where "Z = U \ V" "openin X U" "openin Y V" using Z by blast then have UV: "U \ V = (topspace X \ topspace Y) \ (U \ V)" by (simp add: Sigma_mono inf_absorb2 openin_subset) moreover have "?lhs ((topspace X \ topspace Y) \ (U \ V))" proof (rule relative_to_inc) show "(finite intersection_of (\x. x \ \ \ x \ \)) (U \ V)" apply (simp add: intersection_of_def \_def \_def) apply (rule_tac x="{(U \ topspace Y),(topspace X \ V)}" in exI) using \openin X U\ \openin Y V\ openin_subset UV apply (fastforce simp add:) done qed ultimately show ?thesis using \Z = U \ V\ by auto qed ultimately show ?thesis by meson qed then show "topology (arbitrary union_of (finite intersection_of (\x. x \ \ \ \) relative_to (topspace X \ topspace Y))) = prod_topology X Y" by (simp add: prod_topology_def) qed ultimately show ?thesis using False by blast qed lemma compactin_Times: "compactin (prod_topology X Y) (S \ T) \ S = {} \ T = {} \ compactin X S \ compactin Y T" by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology) subsection\Homeomorphic maps\ lemma homeomorphic_maps_prod: "homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\(x,y). (f x, g y)) (\(x,y). (f' x, g' y)) \ topspace(prod_topology X Y) = {} \ topspace(prod_topology X' Y') = {} \ homeomorphic_maps X X' f f' \ homeomorphic_maps Y Y' g g'" unfolding homeomorphic_maps_def continuous_map_prod_top by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top) lemma homeomorphic_maps_swap: "homeomorphic_maps (prod_topology X Y) (prod_topology Y X) (\(x,y). (y,x)) (\(y,x). (x,y))" by (auto simp: homeomorphic_maps_def case_prod_unfold continuous_map_fst continuous_map_pairedI continuous_map_snd) lemma homeomorphic_map_swap: "homeomorphic_map (prod_topology X Y) (prod_topology Y X) (\(x,y). (y,x))" using homeomorphic_map_maps homeomorphic_maps_swap by metis lemma homeomorphic_space_prod_topology_swap: "(prod_topology X Y) homeomorphic_space (prod_topology Y X)" using homeomorphic_map_swap homeomorphic_space by blast lemma embedding_map_graph: "embedding_map X (prod_topology X Y) (\x. (x, f x)) \ continuous_map X Y f" (is "?lhs = ?rhs") proof assume L: ?lhs have "snd \ (\x. (x, f x)) = f" by force moreover have "continuous_map X Y (snd \ (\x. (x, f x)))" using L unfolding embedding_map_def by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map) ultimately show ?rhs by simp next assume R: ?rhs then show ?lhs unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def by (rule_tac x=fst in exI) (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology continuous_map_fst) qed lemma homeomorphic_space_prod_topology: "\X homeomorphic_space X''; Y homeomorphic_space Y'\ \ prod_topology X Y homeomorphic_space prod_topology X'' Y'" using homeomorphic_maps_prod unfolding homeomorphic_space_def by blast lemma prod_topology_homeomorphic_space_left: "topspace Y = {b} \ prod_topology X Y homeomorphic_space X" unfolding homeomorphic_space_def by (rule_tac x=fst in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps) lemma prod_topology_homeomorphic_space_right: "topspace X = {a} \ prod_topology X Y homeomorphic_space Y" unfolding homeomorphic_space_def by (rule_tac x=snd in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps) lemma homeomorphic_space_prod_topology_sing1: "b \ topspace Y \ X homeomorphic_space (prod_topology X (subtopology Y {b}))" by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_left topspace_subtopology) lemma homeomorphic_space_prod_topology_sing2: "a \ topspace X \ Y homeomorphic_space (prod_topology (subtopology X {a}) Y)" by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_right topspace_subtopology) lemma topological_property_of_prod_component: assumes major: "P(prod_topology X Y)" and X: "\x. \x \ topspace X; P(prod_topology X Y)\ \ P(subtopology (prod_topology X Y) ({x} \ topspace Y))" and Y: "\y. \y \ topspace Y; P(prod_topology X Y)\ \ P(subtopology (prod_topology X Y) (topspace X \ {y}))" and PQ: "\X X'. X homeomorphic_space X' \ (P X \ Q X')" and PR: "\X X'. X homeomorphic_space X' \ (P X \ R X')" shows "topspace(prod_topology X Y) = {} \ Q X \ R Y" proof - have "Q X \ R Y" if "topspace(prod_topology X Y) \ {}" proof - from that obtain a b where a: "a \ topspace X" and b: "b \ topspace Y" by force show ?thesis using X [OF a major] and Y [OF b major] homeomorphic_space_prod_topology_sing1 [OF b, of X] homeomorphic_space_prod_topology_sing2 [OF a, of Y] by (simp add: subtopology_Times) (meson PQ PR homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym) qed then show ?thesis by metis qed lemma limitin_pairwise: "limitin (prod_topology X Y) f l F \ limitin X (fst \ f) (fst l) F \ limitin Y (snd \ f) (snd l) F" (is "?lhs = ?rhs") proof assume ?lhs then obtain a b where ev: "\U. \(a,b) \ U; openin (prod_topology X Y) U\ \ \\<^sub>F x in F. f x \ U" and a: "a \ topspace X" and b: "b \ topspace Y" and l: "l = (a,b)" by (auto simp: limitin_def) moreover have "\\<^sub>F x in F. fst (f x) \ U" if "openin X U" "a \ U" for U proof - have "\\<^sub>F c in F. f c \ U \ topspace Y" using b that ev [of "U \ topspace Y"] by (auto simp: openin_prod_topology_alt) then show ?thesis by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse) qed moreover have "\\<^sub>F x in F. snd (f x) \ U" if "openin Y U" "b \ U" for U proof - have "\\<^sub>F c in F. f c \ topspace X \ U" using a that ev [of "topspace X \ U"] by (auto simp: openin_prod_topology_alt) then show ?thesis by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse) qed ultimately show ?rhs by (simp add: limitin_def) next have "limitin (prod_topology X Y) f (a,b) F" if "limitin X (fst \ f) a F" "limitin Y (snd \ f) b F" for a b using that proof (clarsimp simp: limitin_def) fix Z :: "('a \ 'b) set" assume a: "a \ topspace X" "\U. openin X U \ a \ U \ (\\<^sub>F x in F. fst (f x) \ U)" and b: "b \ topspace Y" "\U. openin Y U \ b \ U \ (\\<^sub>F x in F. snd (f x) \ U)" and Z: "openin (prod_topology X Y) Z" "(a, b) \ Z" then obtain U V where "openin X U" "openin Y V" "a \ U" "b \ V" "U \ V \ Z" using Z by (force simp: openin_prod_topology_alt) then have "\\<^sub>F x in F. fst (f x) \ U" "\\<^sub>F x in F. snd (f x) \ V" by (simp_all add: a b) then show "\\<^sub>F x in F. f x \ Z" by (rule eventually_elim2) (use \U \ V \ Z\ subsetD in auto) qed then show "?rhs \ ?lhs" by (metis prod.collapse) qed end diff --git a/src/HOL/Analysis/Sum_Topology.thy b/src/HOL/Analysis/Sum_Topology.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Analysis/Sum_Topology.thy @@ -0,0 +1,146 @@ +section\Disjoint sum of arbitarily many spaces\ + +theory Sum_Topology + imports Abstract_Topology +begin + + +definition sum_topology :: "('a \ 'b topology) \ 'a set \ ('a \ 'b) topology" where + "sum_topology X I \ + topology (\U. U \ Sigma I (topspace \ X) \ (\i \ I. openin (X i) {x. (i,x) \ U}))" + +lemma is_sum_topology: "istopology (\U. U \ Sigma I (topspace \ X) \ (\i\I. openin (X i) {x. (i, x) \ U}))" +proof - + have 1: "{x. (i, x) \ S \ T} = {x. (i, x) \ S} \ {x::'b. (i, x) \ T}" for S T and i::'a + by auto + have 2: "{x. (i, x) \ \ \} = (\K\\. {x::'b. (i, x) \ K})" for \ and i::'a + by auto + show ?thesis + unfolding istopology_def 1 2 by blast +qed + +lemma openin_sum_topology: + "openin (sum_topology X I) U \ + U \ Sigma I (topspace \ X) \ (\i \ I. openin (X i) {x. (i,x) \ U})" + by (auto simp: sum_topology_def is_sum_topology) + +lemma openin_disjoint_union: + "openin (sum_topology X I) (Sigma I U) \ (\i \ I. openin (X i) (U i))" + using openin_subset by (force simp: openin_sum_topology) + +lemma topspace_sum_topology [simp]: + "topspace(sum_topology X I) = Sigma I (topspace \ X)" + by (metis comp_apply openin_disjoint_union openin_subset openin_sum_topology openin_topspace subset_antisym) + +lemma openin_sum_topology_alt: + "openin (sum_topology X I) U \ (\T. U = Sigma I T \ (\i \ I. openin (X i) (T i)))" + by (bestsimp simp: openin_sum_topology dest: openin_subset) + +lemma forall_openin_sum_topology: + "(\U. openin (sum_topology X I) U \ P U) \ (\T. (\i \ I. openin (X i) (T i)) \ P(Sigma I T))" + by (auto simp: openin_sum_topology_alt) + +lemma exists_openin_sum_topology: + "(\U. openin (sum_topology X I) U \ P U) \ + (\T. (\i \ I. openin (X i) (T i)) \ P(Sigma I T))" + by (auto simp: openin_sum_topology_alt) + +lemma closedin_sum_topology: + "closedin (sum_topology X I) U \ U \ Sigma I (topspace \ X) \ (\i \ I. closedin (X i) {x. (i,x) \ U})" + (is "?lhs = ?rhs") +proof + assume L: ?lhs + then have U: "U \ Sigma I (topspace \ X)" + using closedin_subset by fastforce + then have "\i\I. {x. (i, x) \ U} \ topspace (X i)" + by fastforce + moreover have "openin (X i) (topspace (X i) - {x. (i, x) \ U})" if "i\I" for i + apply (subst openin_subopen) + using L that unfolding closedin_def openin_sum_topology + by (bestsimp simp: o_def subset_iff) + ultimately show ?rhs + by (simp add: U closedin_def) +next + assume R: ?rhs + then have "openin (X i) {x. (i, x) \ topspace (sum_topology X I) - U}" if "i\I" for i + apply (subst openin_subopen) + using that unfolding closedin_def openin_sum_topology + by (bestsimp simp: o_def subset_iff) + then show ?lhs + by (simp add: R closedin_def openin_sum_topology) +qed + +lemma closedin_disjoint_union: + "closedin (sum_topology X I) (Sigma I U) \ (\i \ I. closedin (X i) (U i))" + using closedin_subset by (force simp: closedin_sum_topology) + +lemma closedin_sum_topology_alt: + "closedin (sum_topology X I) U \ (\T. U = Sigma I T \ (\i \ I. closedin (X i) (T i)))" + using closedin_subset unfolding closedin_sum_topology by auto blast + +lemma forall_closedin_sum_topology: + "(\U. closedin (sum_topology X I) U \ P U) \ + (\t. (\i \ I. closedin (X i) (t i)) \ P(Sigma I t))" + by (metis closedin_sum_topology_alt) + +lemma exists_closedin_sum_topology: + "(\U. closedin (sum_topology X I) U \ P U) \ + (\T. (\i \ I. closedin (X i) (T i)) \ P(Sigma I T))" + by (simp add: closedin_sum_topology_alt) blast + +lemma open_map_component_injection: + "i \ I \ open_map (X i) (sum_topology X I) (\x. (i,x))" + unfolding open_map_def openin_sum_topology + using openin_subset openin_subopen by (force simp: image_iff) + +lemma closed_map_component_injection: + assumes "i \ I" + shows "closed_map(X i) (sum_topology X I) (\x. (i,x))" +proof - + have "closedin (X j) {x. j = i \ x \ U}" + if "\U S. closedin U S \ S \ topspace U" and "closedin (X i) U" and "j \ I" for U j + using that by (cases "j=i") auto + then show ?thesis + using closedin_subset assms by (force simp: closed_map_def closedin_sum_topology image_iff) +qed + +lemma continuous_map_component_injection: + "i \ I \ continuous_map(X i) (sum_topology X I) (\x. (i,x))" + apply (clarsimp simp: continuous_map_def openin_sum_topology) + by (smt (verit, best) Collect_cong mem_Collect_eq openin_subset subsetD) + +lemma subtopology_sum_topology: + "subtopology (sum_topology X I) (Sigma I S) = + sum_topology (\i. subtopology (X i) (S i)) I" + unfolding topology_eq +proof (intro strip iffI) + fix T + assume *: "openin (subtopology (sum_topology X I) (Sigma I S)) T" + then obtain U where U: "\i\I. openin (X i) (U i) \ T = Sigma I U \ Sigma I S" + by (auto simp: openin_subtopology openin_sum_topology_alt) + have "T = (SIGMA i:I. U i \ S i)" + proof + show "T \ (SIGMA i:I. U i \ S i)" + by (metis "*" SigmaE Sigma_Int_distrib2 U openin_imp_subset subset_iff) + show "(SIGMA i:I. U i \ S i) \ T" + using U by fastforce + qed + then show "openin (sum_topology (\i. subtopology (X i) (S i)) I) T" + by (simp add: U openin_disjoint_union openin_subtopology_Int) +next + fix T + assume *: "openin (sum_topology (\i. subtopology (X i) (S i)) I) T" + then obtain U where "\i\I. \T. openin (X i) T \ U i = T \ S i" and Teq: "T = Sigma I U" + by (auto simp: openin_subtopology openin_sum_topology_alt) + then obtain B where "\i. i\I \ openin (X i) (B i) \ U i = B i \ S i" + by metis + then show "openin (subtopology (sum_topology X I) (Sigma I S)) T" + by (auto simp: openin_subtopology openin_sum_topology_alt Teq) +qed + +lemma embedding_map_component_injection: + "i \ I \ embedding_map (X i) (sum_topology X I) (\x. (i,x))" + by (metis injective_open_imp_embedding_map continuous_map_component_injection + open_map_component_injection inj_onI prod.inject) + +end