diff -r 9e0c035d026d -r eb9a9690b8f5 src/HOL/Analysis/Abstract_Topological_Spaces.thy --- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon Jul 10 18:48:22 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Tue Jul 11 20:21:58 2023 +0100 @@ -894,7 +894,8 @@ qed subsection \Neigbourhood bases EXTRAS\ -(* Neigbourhood bases (useful for "local" properties of various kind). *) + +text \Neigbourhood bases: useful for "local" properties of various kinds\ lemma openin_topology_neighbourhood_base_unique: "openin X = arbitrary union_of P \ @@ -1192,7 +1193,7 @@ assumes "continuous_map X Y f" "t0_space Y" and x: "x \ topspace X" shows "f (Kolmogorov_quotient X x) = f x" using assms unfolding continuous_map_def t0_space_def - by (smt (verit, ccfv_SIG) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace x mem_Collect_eq) + by (smt (verit, ccfv_threshold) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace PiE mem_Collect_eq) lemma t0_space_Kolmogorov_quotient: "t0_space (subtopology X (Kolmogorov_quotient X ` topspace X))" @@ -1239,7 +1240,7 @@ have "\x y. \x \ S; y \ S; Kolmogorov_quotient X x = Kolmogorov_quotient X y\ \ f x = f y" using assms apply (simp add: Kolmogorov_quotient_eq t0_space_def continuous_map_def Int_absorb1 openin_subtopology) - by (smt (verit, del_insts) Int_iff mem_Collect_eq) + by (smt (verit, del_insts) Int_iff mem_Collect_eq Pi_iff) then obtain g where g: "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g" "g ` (topspace X \ Kolmogorov_quotient X ` S) = f ` S" "\x. x \ S \ g (Kolmogorov_quotient X x) = f x" @@ -1321,7 +1322,7 @@ obtain r where r: "continuous_map X (subtopology X S) r" "\x\S. r x = x" using assms by (meson retract_of_space_def) then have \
: "S = {x \ topspace X. r x = x}" - using S retract_of_space_imp_subset by (force simp: continuous_map_def) + using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff) show ?thesis unfolding \
using r continuous_map_into_fulltopology assms @@ -1345,7 +1346,8 @@ assume ?rhs then show ?lhs unfolding homeomorphic_maps_def - by (smt (verit, ccfv_threshold) continuous_map_eq continuous_map_subtopology_fst embedding_map_def embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.collapse prod.inject) + by (smt (verit, del_insts) continuous_map_eq continuous_map_subtopology_fst embedding_map_def + embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.sel(1)) qed @@ -1663,9 +1665,8 @@ have "continuous_map (subtopology X A) (subtopology Y K) f" if "kc_space X" unfolding continuous_map_closedin proof (intro conjI strip) - show "f x \ topspace (subtopology Y K)" - if "x \ topspace (subtopology X A)" for x - using that A_def K compactin_subset_topspace by auto + show "f \ topspace (subtopology X A) \ topspace (subtopology Y K)" + using A_def K compactin_subset_topspace by fastforce next fix C assume C: "closedin (subtopology Y K) C" @@ -1927,7 +1928,7 @@ using proper_map_paired [OF assms] by (simp add: o_def) lemma proper_map_from_composition_right: - assumes "Hausdorff_space Y" "proper_map X Z (g \ f)" and "continuous_map X Y f" + assumes "Hausdorff_space Y" "proper_map X Z (g \ f)" and contf: "continuous_map X Y f" and contg: "continuous_map Y Z g" shows "proper_map X Y f" proof - @@ -1935,7 +1936,7 @@ have "proper_map X Y (fst \ (\x. (f x, (g \ f) x)))" proof (rule proper_map_compose) have [simp]: "x \ topspace X \ f x \ topspace Y" for x - by (meson assms(3) continuous_map_def) + using contf continuous_map_preimage_topspace by auto show "proper_map X YZ (\x. (f x, (g \ f) x))" unfolding YZ_def using assms @@ -2558,7 +2559,8 @@ using \closed_map X Y f\ \closedin X C\ \openin X U2\ closed_map_def by blast moreover have "f x \ topspace Y - f ` (C - U2)" - using \closedin X C\ \continuous_map X Y f\ \x \ topspace X\ closedin_subset continuous_map_def subV by fastforce + using \closedin X C\ \continuous_map X Y f\ \x \ topspace X\ closedin_subset continuous_map_def subV + by (fastforce simp: Pi_iff) ultimately obtain V1 V2 where VV: "openin Y V1" "openin Y V2" "f x \ V1" and subV2: "f ` (C - U2) \ V2" and "disjnt V1 V2" @@ -3213,7 +3215,7 @@ assume x: "x \ topspace X" then obtain U K where "openin X' U" "compactin X' K" "f x \ U" "U \ K" using assms unfolding locally_compact_space_def perfect_map_def - by (metis (no_types, lifting) continuous_map_closedin) + by (metis (no_types, lifting) continuous_map_closedin Pi_iff) show "\U K. openin X U \ compactin X K \ x \ U \ U \ K" proof (intro exI conjI) have "continuous_map X X' f" @@ -3433,7 +3435,7 @@ by (auto simp: retraction_maps_def) show "S \ {x \ topspace Y. r' x \ U}" "T \ {x \ topspace Y. r' x \ V}" using openin_continuous_map_preimage UV r' \closedin Y S\ \closedin Y T\ - by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff) + by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff Pi_iff) show "disjnt {x \ topspace Y. r' x \ U} {x \ topspace Y. r' x \ V}" using \disjnt U V\ by (auto simp: disjnt_def) qed @@ -4293,7 +4295,7 @@ unfolding quasi_component_of_def proof (intro strip conjI) show "f x \ topspace Y" "f y \ topspace Y" - using assms by (simp_all add: continuous_map_def quasi_component_of_def) + using assms by (simp_all add: continuous_map_def quasi_component_of_def Pi_iff) fix T assume "closedin Y T \ openin Y T" with assms show "(f x \ T) = (f y \ T)"