# HG changeset patch # User paulson # Date 1689460482 -3600 # Node ID 6bae28577994d59365a178b8f36d93816b1da0df # Parent 19c617950a8eadc3697267a59bcafa7c1ca8991f trivial_topology diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Abstract_Euclidean_Space.thy --- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Sat Jul 15 23:34:42 2023 +0100 @@ -16,8 +16,8 @@ "topspace(Euclidean_space n) = {x. \i\n. x i = 0}" by (simp add: Euclidean_space_def) -lemma nonempty_Euclidean_space: "topspace(Euclidean_space n) \ {}" - by (force simp: topspace_Euclidean_space) +lemma nontrivial_Euclidean_space: "Euclidean_space n \ trivial_topology" + using topspace_Euclidean_space [of n] by force lemma subset_Euclidean_space [simp]: "topspace(Euclidean_space m) \ topspace(Euclidean_space n) \ m \ n" @@ -166,9 +166,10 @@ locally_path_connected_space_product_topology) using locally_path_connected_space_euclideanreal by auto -lemma compact_Euclidean_space: +lemma compact_Euclidean_space [simp]: "compact_space (Euclidean_space n) \ n = 0" - by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology) + using homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] + by (auto simp: product_topology_trivial_iff compact_space_product_topology) subsection\n-dimensional spheres\ @@ -188,8 +189,8 @@ lemma in_topspace_nsphere: "(\n. if n = 0 then 1 else 0) \ topspace (nsphere n)" by (simp add: nsphere_def topspace_Euclidean_space power2_eq_square if_distrib [where f = "\x. x * _"] cong: if_cong) -lemma nonempty_nsphere [simp]: "~ (topspace(nsphere n) = {})" - using in_topspace_nsphere by auto +lemma nonempty_nsphere [simp]: "(nsphere n) \ trivial_topology" + by (metis discrete_topology_unique empty_iff in_topspace_nsphere) lemma subtopology_nsphere_equator: "subtopology (nsphere (Suc n)) {x. x(Suc n) = 0} = nsphere n" @@ -344,7 +345,7 @@ proof (rule continuous_map_compose) have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal ((\x. f x k) \ snd)" for k unfolding nsphere - apply (simp add: continuous_map_of_snd) + apply (simp add: continuous_map_of_snd flip: null_topspace_iff_trivial) apply (rule continuous_map_compose [of _ "nsphere p" f, unfolded o_def]) using f apply (simp add: nsphere) by (simp add: continuous_map_nsphere_projection) diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Abstract_Metric_Spaces.thy --- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sat Jul 15 23:34:42 2023 +0100 @@ -675,12 +675,12 @@ lemma compactin_mtopology_eq_compact [simp]: "compactin Met_TC.mtopology = compact" by (simp add: compactin_def compact_eq_Heine_Borel fun_eq_iff) meson -lemma metrizable_space_discrete_topology: +lemma metrizable_space_discrete_topology [simp]: "metrizable_space(discrete_topology U)" by (metis discrete_metric.mtopology_discrete_metric metric_M_dd metrizable_space_def) -lemma empty_metrizable_space: "topspace X = {} \ metrizable_space X" - by (metis metrizable_space_discrete_topology subtopology_eq_discrete_topology_empty) +lemma empty_metrizable_space: "metrizable_space trivial_topology" + by simp lemma metrizable_space_subtopology: assumes "metrizable_space X" @@ -2757,7 +2757,7 @@ \M d. Metric_space M d \ Metric_space.mcomplete M d \ X = Metric_space.mtopology M d" lemma empty_completely_metrizable_space: - "topspace X = {} \ completely_metrizable_space X" + "completely_metrizable_space trivial_topology" unfolding completely_metrizable_space_def subtopology_eq_discrete_topology_empty [symmetric] by (metis Metric_space.mcomplete_empty_mspace discrete_metric.mtopology_discrete_metric metric_M_dd) @@ -3300,12 +3300,12 @@ lemma metrizable_space_prod_topology: "metrizable_space (prod_topology X Y) \ - topspace(prod_topology X Y) = {} \ metrizable_space X \ metrizable_space Y" + (prod_topology X Y) = trivial_topology \ metrizable_space X \ metrizable_space Y" (is "?lhs \ ?rhs") -proof (cases "topspace(prod_topology X Y) = {}") +proof (cases "(prod_topology X Y) = trivial_topology") case False then obtain x y where "x \ topspace X" "y \ topspace Y" - by auto + by fastforce show ?thesis proof show "?rhs \ ?lhs" @@ -3326,18 +3326,18 @@ ultimately show ?rhs by (simp add: homeomorphic_metrizable_space) qed -qed (simp add: empty_metrizable_space) +qed auto lemma completely_metrizable_space_prod_topology: "completely_metrizable_space (prod_topology X Y) \ - topspace(prod_topology X Y) = {} \ + (prod_topology X Y) = trivial_topology \ completely_metrizable_space X \ completely_metrizable_space Y" (is "?lhs \ ?rhs") -proof (cases "topspace(prod_topology X Y) = {}") +proof (cases "(prod_topology X Y) = trivial_topology") case False then obtain x y where "x \ topspace X" "y \ topspace Y" - by auto + by fastforce show ?thesis proof show "?rhs \ ?lhs" @@ -3365,7 +3365,10 @@ ultimately show ?rhs by (simp add: homeomorphic_completely_metrizable_space) qed -qed (simp add: empty_completely_metrizable_space) +next + case True then show ?thesis + using empty_completely_metrizable_space by auto +qed subsection \The "atin-within" filter for topologies\ @@ -4809,12 +4812,12 @@ lemma metrizable_topology_A: assumes "metrizable_space (product_topology X I)" - shows "topspace (product_topology X I) = {} \ (\i \ I. metrizable_space (X i))" + shows "(product_topology X I) = trivial_topology \ (\i \ I. metrizable_space (X i))" by (meson assms metrizable_space_retraction_map_image retraction_map_product_projection) lemma metrizable_topology_C: assumes "completely_metrizable_space (product_topology X I)" - shows "topspace (product_topology X I) = {} \ (\i \ I. completely_metrizable_space (X i))" + shows "(product_topology X I) = trivial_topology \ (\i \ I. completely_metrizable_space (X i))" by (meson assms completely_metrizable_space_retraction_map_image retraction_map_product_projection) lemma metrizable_topology_B: @@ -5109,17 +5112,17 @@ proposition metrizable_space_product_topology: "metrizable_space (product_topology X I) \ - topspace (product_topology X I) = {} \ + (product_topology X I) = trivial_topology \ countable {i \ I. \ (\a. topspace(X i) \ {a})} \ (\i \ I. metrizable_space (X i))" - by (metis (mono_tags, lifting) empty_metrizable_space metrizable_topology_A metrizable_topology_B metrizable_topology_D) + by (metis (mono_tags, lifting) empty_metrizable_space metrizable_topology_A metrizable_topology_B metrizable_topology_D subtopology_eq_discrete_topology_empty) proposition completely_metrizable_space_product_topology: "completely_metrizable_space (product_topology X I) \ - topspace (product_topology X I) = {} \ + (product_topology X I) = trivial_topology \ countable {i \ I. \ (\a. topspace(X i) \ {a})} \ (\i \ I. completely_metrizable_space (X i))" - by (metis (mono_tags, lifting) completely_metrizable_imp_metrizable_space empty_completely_metrizable_space metrizable_topology_B metrizable_topology_C metrizable_topology_E) + by (smt (verit, del_insts) Collect_cong completely_metrizable_imp_metrizable_space empty_completely_metrizable_space metrizable_topology_B metrizable_topology_C metrizable_topology_E subtopology_eq_discrete_topology_empty) lemma completely_metrizable_Euclidean_space: diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Abstract_Topological_Spaces.thy --- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Sat Jul 15 23:34:42 2023 +0100 @@ -1050,16 +1050,16 @@ lemma t0_space_prod_topology_iff: - "t0_space (prod_topology X Y) \ topspace (prod_topology X Y) = {} \ t0_space X \ t0_space Y" (is "?lhs=?rhs") + "t0_space (prod_topology X Y) \ prod_topology X Y = trivial_topology \ t0_space X \ t0_space Y" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs - by (metis Sigma_empty1 Sigma_empty2 retraction_map_fst retraction_map_snd t0_space_retraction_map_image topspace_prod_topology) -qed (metis empty_iff t0_space_def t0_space_prod_topologyI) + by (metis prod_topology_trivial_iff retraction_map_fst retraction_map_snd t0_space_retraction_map_image) +qed (metis t0_space_discrete_topology t0_space_prod_topologyI) proposition t0_space_product_topology: - "t0_space (product_topology X I) \ - topspace(product_topology X I) = {} \ (\i \ I. t0_space (X i))" (is "?lhs=?rhs") + "t0_space (product_topology X I) \ product_topology X I = trivial_topology \ (\i \ I. t0_space (X i))" + (is "?lhs=?rhs") proof assume ?lhs then show ?rhs @@ -1067,7 +1067,7 @@ next assume R: ?rhs show ?lhs - proof (cases "topspace(product_topology X I) = {}") + proof (cases "product_topology X I = trivial_topology") case True then show ?thesis by (simp add: t0_space_def) @@ -1762,12 +1762,10 @@ lemma proper_map_prod: "proper_map (prod_topology X Y) (prod_topology X' Y') (\(x,y). (f x, g y)) \ - topspace(prod_topology X Y) = {} \ proper_map X X' f \ proper_map Y Y' g" + (prod_topology X Y) = trivial_topology \ proper_map X X' f \ proper_map Y Y' g" (is "?lhs \ _ \ ?rhs") -proof (cases "topspace(prod_topology X Y) = {}") - case True - then show ?thesis - by (simp add: proper_map_on_empty) +proof (cases "(prod_topology X Y) = trivial_topology") + case True then show ?thesis by auto next case False then have ne: "topspace X \ {}" "topspace Y \ {}" @@ -2060,7 +2058,7 @@ finally show ?thesis . qed -lemma regular_space_discrete_topology: +lemma regular_space_discrete_topology [simp]: "regular_space (discrete_topology S)" using neighbourhood_base_of_closedin neighbourhood_base_of_discrete_topology by fastforce @@ -2103,9 +2101,6 @@ by (metis closedin_compact_space compactin_sing disjnt_empty1 insert_subset disjnt_insert1) qed -lemma regular_space_topspace_empty: "topspace X = {} \ regular_space X" - by (simp add: Hausdorff_space_topspace_empty compact_Hausdorff_imp_regular_space compact_space_topspace_empty) - lemma neighbourhood_base_of_closed_Hausdorff_space: "regular_space X \ Hausdorff_space X \ neighbourhood_base_of (\C. closedin X C \ Hausdorff_space(subtopology X C)) X" (is "?lhs=?rhs") @@ -2181,7 +2176,7 @@ lemma regular_space_prod_topology: "regular_space (prod_topology X Y) \ - topspace X = {} \ topspace Y = {} \ regular_space X \ regular_space Y" (is "?lhs=?rhs") + X = trivial_topology \ Y = trivial_topology \ regular_space X \ regular_space Y" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs @@ -2189,10 +2184,8 @@ next assume R: ?rhs show ?lhs - proof (cases "topspace X = {} \ topspace Y = {}") - case True - then show ?thesis - by (simp add: regular_space_topspace_empty) + proof (cases "X = trivial_topology \ Y = trivial_topology") + case True then show ?thesis by auto next case False then have "regular_space X" "regular_space Y" @@ -2223,7 +2216,7 @@ lemma regular_space_product_topology: "regular_space (product_topology X I) \ - topspace (product_topology X I) = {} \ (\i \ I. regular_space (X i))" (is "?lhs=?rhs") + (product_topology X I) = trivial_topology \ (\i \ I. regular_space (X i))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs @@ -2231,14 +2224,14 @@ next assume R: ?rhs show ?lhs - proof (cases "topspace(product_topology X I) = {}") + proof (cases "product_topology X I = trivial_topology") case True then show ?thesis - by (simp add: regular_space_topspace_empty) + by auto next case False then obtain x where x: "x \ topspace (product_topology X I)" - by blast + by (meson ex_in_conv null_topspace_iff_trivial) define \ where "\ \ {Pi\<^sub>E I U |U. finite {i \ I. U i \ topspace (X i)} \ (\i\I. openin (X i) (U i))}" have oo: "openin (product_topology X I) = arbitrary union_of (\W. W \ \)" @@ -2957,20 +2950,20 @@ lemma locally_compact_space_prod_topology: "locally_compact_space (prod_topology X Y) \ - topspace (prod_topology X Y) = {} \ + (prod_topology X Y) = trivial_topology \ locally_compact_space X \ locally_compact_space Y" (is "?lhs=?rhs") -proof (cases "topspace (prod_topology X Y) = {}") +proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis - unfolding locally_compact_space_def by blast + using locally_compact_space_discrete_topology by force next case False then obtain w z where wz: "w \ topspace X" "z \ topspace Y" - by auto + by fastforce show ?thesis proof assume L: ?lhs then show ?rhs - by (metis wz empty_iff locally_compact_space_retraction_map_image retraction_map_fst retraction_map_snd) + by (metis locally_compact_space_retraction_map_image prod_topology_trivial_iff retraction_map_fst retraction_map_snd) next assume R: ?rhs show ?lhs @@ -2999,9 +2992,9 @@ lemma locally_compact_space_product_topology: "locally_compact_space(product_topology X I) \ - topspace(product_topology X I) = {} \ + product_topology X I = trivial_topology \ finite {i \ I. \ compact_space(X i)} \ (\i \ I. locally_compact_space(X i))" (is "?lhs=?rhs") -proof (cases "topspace (product_topology X I) = {}") +proof (cases "(product_topology X I) = trivial_topology") case True then show ?thesis by (simp add: locally_compact_space_def) @@ -3011,7 +3004,8 @@ proof assume L: ?lhs obtain z where z: "z \ topspace (product_topology X I)" - using False by auto + using False + by (meson ex_in_conv null_topspace_iff_trivial) with L z obtain U C where "openin (product_topology X I) U" "compactin (product_topology X I) C" "z \ U" "U \ C" by (meson locally_compact_space_def) then obtain V where finV: "finite {i \ I. V i \ topspace (X i)}" and "\i \ I. openin (X i) (V i)" @@ -3968,11 +3962,11 @@ by (metis (no_types, lifting) image_iff quasi_component_of_eq_empty quasi_components_of_def) lemma quasi_components_of_eq_empty [simp]: - "quasi_components_of X = {} \ topspace X = {}" + "quasi_components_of X = {} \ X = trivial_topology" by (simp add: quasi_components_of_def) -lemma quasi_components_of_empty_space: - "topspace X = {} \ quasi_components_of X = {}" +lemma quasi_components_of_empty_space [simp]: + "quasi_components_of trivial_topology = {}" by simp lemma quasi_component_of_set: @@ -4098,16 +4092,16 @@ by (metis connected_space_iff_quasi_component mem_Collect_eq quasi_component_of_equiv) lemma quasi_components_of_subset_sing: - "quasi_components_of X \ {S} \ connected_space X \ (topspace X = {} \ topspace X = S)" + "quasi_components_of X \ {S} \ connected_space X \ (X = trivial_topology \ topspace X = S)" proof (cases "quasi_components_of X = {}") case True then show ?thesis - by (simp add: connected_space_topspace_empty subset_singleton_iff) + by (simp add: subset_singleton_iff) next case False then show ?thesis apply (simp add: connected_space_iff_quasi_components_eq subset_iff Ball_def) - by (metis quasi_components_of_subset subsetI subset_antisym subset_empty topspace_imp_quasi_components_of) + by (metis False Union_quasi_components_of ccpo_Sup_singleton insert_iff is_singletonE is_singletonI') qed lemma connected_space_iff_quasi_components_subset_sing: @@ -4116,12 +4110,12 @@ lemma quasi_components_of_eq_singleton: "quasi_components_of X = {S} \ - connected_space X \ \ (topspace X = {}) \ S = topspace X" - by (metis ccpo_Sup_singleton insert_not_empty quasi_components_of_subset_sing subset_singleton_iff) + connected_space X \ \ (X = trivial_topology) \ S = topspace X" + by (metis empty_not_insert quasi_components_of_eq_empty quasi_components_of_subset_sing subset_singleton_iff) lemma quasi_components_of_connected_space: "connected_space X - \ quasi_components_of X = (if topspace X = {} then {} else {topspace X})" + \ quasi_components_of X = (if X = trivial_topology then {} else {topspace X})" by (simp add: quasi_components_of_eq_singleton) lemma separated_between_singletons: @@ -4745,7 +4739,9 @@ using locally_compact_space_compact_closed_compact [of "subtopology X (U - {a})"] assms by (smt (verit, del_insts) Diff_empty compactin_subtopology open_in_Hausdorff_delete openin_open_subtopology subset_Diff_insert) then obtain D where D: "D \ connected_components_of (subtopology X K)" and "C \ D" - using C by (metis bot.extremum_unique connectedin_subtopology order.trans exists_connected_component_of_superset subtopology_topspace) + using C + by (metis compactin_subset_topspace connected_component_in_connected_components_of + connected_component_of_maximal connectedin_subtopology subset_empty subset_eq topspace_subtopology_subset) show thesis proof have cloD: "closedin (subtopology X K) D" diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Topology.thy Sat Jul 15 23:34:42 2023 +0100 @@ -227,6 +227,10 @@ "X = discrete_topology {a} \ topspace X = {a}" by (metis discrete_topology_unique openin_topspace singletonD) +abbreviation trivial_topology where "trivial_topology \ discrete_topology {}" + +lemma null_topspace_iff_trivial [simp]: "topspace X = {} \ X = trivial_topology" + by (simp add: subtopology_eq_discrete_topology_empty) subsection \Subspace topology\ @@ -316,6 +320,9 @@ unfolding openin_subtopology by auto (metis IntD1 in_mono openin_subset) +lemma subtopology_trivial_iff: "subtopology X S = trivial_topology \ X = trivial_topology \ topspace X \ S = {}" + by (auto simp flip: null_topspace_iff_trivial) + lemma subtopology_subtopology: "subtopology (subtopology X S) T = subtopology X (S \ T)" proof - @@ -356,6 +363,9 @@ lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" by (simp add: subtopology_superset) +lemma subtopology_empty_iff_trivial [simp]: "subtopology X {} = trivial_topology" + by (simp add: subtopology_eq_discrete_topology_empty) + lemma subtopology_restrict: "subtopology X (topspace X \ S) = subtopology X S" by (metis subtopology_subtopology subtopology_topspace) @@ -372,11 +382,11 @@ "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 = {})" +lemma closedin_topspace_empty [simp]: "closedin trivial_topology S \ S = {}" by (simp add: closedin_def) -lemma open_in_topspace_empty: - "topspace X = {} \ openin X S \ S = {}" +lemma openin_topspace_empty [simp]: + "openin trivial_topology S \ S = {}" by (simp add: openin_closedin_eq) lemma openin_imp_subset: @@ -441,6 +451,10 @@ lemma openin_subtopology_self [simp]: "openin (top_of_set S) S" by (metis openin_topspace topspace_euclidean_subtopology) +lemma euclidean_nontrivial [simp]: "euclidean \ trivial_topology" + by (simp add: subtopology_eq_discrete_topology_empty) + + subsubsection\The most basic facts about the usual topology and metric on R\ abbreviation euclideanreal :: "real topology" @@ -1470,11 +1484,11 @@ "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" +lemma continuous_map_on_empty [simp]: "continuous_map trivial_topology Y f" by (auto simp: continuous_map_def) -lemma continuous_map_on_empty2: "topspace Y = {} \ continuous_map X Y f \ topspace X = {}" - by (auto simp: continuous_map_def) +lemma continuous_map_on_empty2 [simp]: "continuous_map X trivial_topology f \ X = trivial_topology" + using continuous_map_image_subset_topspace by fastforce lemma continuous_map_closedin: "continuous_map X Y f \ @@ -1633,9 +1647,9 @@ qed lemma continuous_map_const [simp]: - "continuous_map X Y (\x. C) \ topspace X = {} \ C \ topspace Y" -proof (cases "topspace X = {}") - case False + "continuous_map X Y (\x. C) \ X = trivial_topology \ C \ topspace Y" +proof (cases "X = trivial_topology") + case nontriv: False show ?thesis proof (cases "C \ topspace Y") case True @@ -1643,10 +1657,10 @@ by (auto simp: continuous_map_def) next case False - then show ?thesis - unfolding continuous_map_def by fastforce + with nontriv show ?thesis + using continuous_map_image_subset_topspace discrete_topology_unique image_subset_iff by fastforce qed -qed (auto simp: continuous_map_on_empty) +qed auto declare continuous_map_const [THEN iffD2, continuous_intros] @@ -1788,17 +1802,16 @@ "open_map X1 X2 f \ f \ (topspace X1) \ topspace X2" unfolding open_map_def using openin_subset by fastforce -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 open_map_on_empty [simp]: "open_map trivial_topology Y f" + by (simp add: open_map_def) lemma closed_map_on_empty: - "topspace X = {} \ closed_map X Y f" + "closed_map trivial_topology 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) + "closed_map X Y (\x. c) \ X = trivial_topology \ closedin Y {c}" + by (metis closed_map_def closed_map_on_empty closedin_topspace discrete_topology_unique equals0D image_constant_conv) lemma open_map_imp_subset: "\open_map X1 X2 f; S \ topspace X1\ \ f \ S \ topspace X2" @@ -3063,14 +3076,14 @@ using homeomorphic_space_def by blast lemma homeomorphic_empty_space: - "X homeomorphic_space Y \ topspace X = {} \ topspace Y = {}" - by (metis homeomorphic_eq_everything_map homeomorphic_space image_is_empty) + "X homeomorphic_space Y \ X = trivial_topology \ Y = trivial_topology" + by (meson continuous_map_on_empty2 homeomorphic_maps_def homeomorphic_space_def) lemma homeomorphic_empty_space_eq: - assumes "topspace X = {}" - shows "X homeomorphic_space Y \ topspace Y = {}" - using assms - by (auto simp: homeomorphic_maps_def homeomorphic_space_def continuous_map_def) + assumes "X = trivial_topology" + shows "X homeomorphic_space Y \ Y = trivial_topology" + using assms funcset_mem + by (fastforce simp: homeomorphic_maps_def homeomorphic_space_def continuous_map_def) lemma homeomorphic_space_unfold: assumes "X homeomorphic_space Y" @@ -3193,8 +3206,7 @@ lemma connectedin_empty [simp]: "connectedin X {}" by (simp add: connectedin) -lemma connected_space_topspace_empty: - "topspace X = {} \ connected_space X" +lemma connected_space_trivial_topology [simp]: "connected_space trivial_topology" using connectedin_topspace by fastforce lemma connectedin_sing [simp]: "connectedin X {a} \ a \ topspace X" @@ -3558,8 +3570,7 @@ lemma compactin_empty [iff]: "compactin X {}" by (simp add: finite_imp_compactin) -lemma compact_space_topspace_empty: - "topspace X = {} \ compact_space X" +lemma compact_space_trivial_topology [simp]: "compact_space trivial_topology" by (simp add: compact_space_def) lemma finite_imp_compactin_eq: @@ -3705,11 +3716,10 @@ "compact_space X \ (\\. (\C\\. closedin X C) \ (\\. finite \ \ \ \ \ \ \\ \ {}) \ \\ \ {})" (is "_ = ?rhs") -proof (cases "topspace X = {}") +proof (cases "X = trivial_topology") 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) + by (metis Pow_iff closedin_topspace_empty compact_space_trivial_topology finite.emptyI finite_Pow_iff finite_subset subsetI) next case False show ?thesis @@ -3724,7 +3734,7 @@ ultimately obtain \ where \: "finite \" "\ \ \" "topspace X \ topspace X - \\" by (auto simp: ex_finite_subset_image \_def) moreover have "\ \ {}" - using \ \topspace X \ {}\ by blast + using \ False by force ultimately show "False" using * [of \] by auto (metis Diff_iff Inter_iff clo closedin_def subsetD) @@ -3736,7 +3746,7 @@ 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" "\ \ {}" + with False have *: "\V \ \. closedin X V" "\ \ {}" by (auto simp: \_def) show "\\. finite \ \ \ \ \ \ topspace X \ \\" proof (rule ccontr; simp) @@ -4965,8 +4975,7 @@ qed qed (simp add: proper_imp_closed_map) -lemma proper_map_on_empty: - "topspace X = {} \ proper_map X Y f" +lemma proper_map_on_empty [simp]: "proper_map trivial_topology Y f" by (auto simp: proper_map_def closed_map_on_empty) lemma proper_map_id [simp]: @@ -5001,11 +5010,11 @@ qed lemma proper_map_const: - "proper_map X Y (\x. c) \ compact_space X \ (topspace X = {} \ closedin Y {c})" -proof (cases "topspace X = {}") + "proper_map X Y (\x. c) \ compact_space X \ (X = trivial_topology \ closedin Y {c})" +proof (cases "X = trivial_topology") case True then show ?thesis - by (simp add: compact_space_topspace_empty proper_map_on_empty) + by simp next case False have *: "compactin X {x \ topspace X. c = y}" if "compact_space X" for y diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Abstract_Topology_2.thy --- a/src/HOL/Analysis/Abstract_Topology_2.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy Sat Jul 15 23:34:42 2023 +0100 @@ -1128,8 +1128,8 @@ using retract_of_space_def by force lemma retract_of_space_empty [simp]: - "{} retract_of_space X \ topspace X = {}" - by (auto simp: continuous_map_def retract_of_space_def) + "{} retract_of_space X \ X = trivial_topology" + by (auto simp: retract_of_space_def) lemma retract_of_space_singleton [simp]: "{a} retract_of_space X \ a \ topspace X" @@ -1155,7 +1155,7 @@ by (metis continuous_map_from_subtopology inf.absorb2 subtopology_subtopology) lemma retract_of_space_clopen: - assumes "openin X S" "closedin X S" "S = {} \ topspace X = {}" + assumes "openin X S" "closedin X S" "S = {} \ X = trivial_topology" shows "S retract_of_space X" proof (cases "S = {}") case False @@ -1181,7 +1181,7 @@ qed (use assms in auto) lemma retract_of_space_disjoint_union: - assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \ T = topspace X" and "S = {} \ topspace X = {}" + assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \ T = topspace X" and "S = {} \ X = trivial_topology" shows "S retract_of_space X" proof (rule retract_of_space_clopen) have "S \ T = {}" @@ -1230,10 +1230,9 @@ "pathin (subtopology X S) g \ pathin X g \ (\x \ {0..1}. g x \ S)" by (auto simp: pathin_def continuous_map_in_subtopology) -lemma pathin_const: - "pathin X (\x. a) \ a \ topspace X" - by (simp add: pathin_def) - +lemma pathin_const [simp]: "pathin X (\x. a) \ a \ topspace X" + using pathin_subtopology by (fastforce simp add: pathin_def) + lemma path_start_in_topspace: "pathin X g \ g 0 \ topspace X" by (force simp: pathin_def continuous_map) @@ -1293,7 +1292,7 @@ by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def) lemma path_connected_space_topspace_empty: - "topspace X = {} \ path_connected_space X" + "path_connected_space trivial_topology" by (simp add: path_connected_space_def) lemma path_connectedin_empty [simp]: "path_connectedin X {}" @@ -1524,23 +1523,23 @@ qed lemma connected_components_of_eq_empty: - "connected_components_of X = {} \ topspace X = {}" + "connected_components_of X = {} \ X = trivial_topology" by (simp add: connected_components_of_def) lemma connected_components_of_empty_space: - "topspace X = {} \ connected_components_of X = {}" + "connected_components_of trivial_topology = {}" by (simp add: connected_components_of_eq_empty) lemma connected_components_of_subset_sing: - "connected_components_of X \ {S} \ connected_space X \ (topspace X = {} \ topspace X = S)" -proof (cases "topspace X = {}") + "connected_components_of X \ {S} \ connected_space X \ (X = trivial_topology \ topspace X = S)" +proof (cases "X = trivial_topology") case True then show ?thesis - by (simp add: connected_components_of_empty_space connected_space_topspace_empty) + by (simp add: connected_components_of_empty_space) next case False then have "\connected_components_of X \ {S}\ \ topspace X = S" - by (metis Sup_empty Union_connected_components_of ccpo_Sup_singleton subset_singleton_iff) + using Union_connected_components_of connected_components_of_eq_empty by fastforce with False show ?thesis unfolding connected_components_of_def by (metis connected_space_connected_component_set empty_iff image_subset_iff insert_iff) @@ -1551,21 +1550,20 @@ by (simp add: connected_components_of_subset_sing) lemma connected_components_of_eq_singleton: - "connected_components_of X = {S} -\ connected_space X \ topspace X \ {} \ S = topspace X" - by (metis ccpo_Sup_singleton connected_components_of_subset_sing insert_not_empty subset_singleton_iff) + "connected_components_of X = {S} \ connected_space X \ X \ trivial_topology \ S = topspace X" + by (metis connected_components_of_eq_empty connected_components_of_subset_sing insert_not_empty subset_singleton_iff) lemma connected_components_of_connected_space: - "connected_space X \ connected_components_of X = (if topspace X = {} then {} else {topspace X})" + "connected_space X \ connected_components_of X = (if X = trivial_topology then {} else {topspace X})" by (simp add: connected_components_of_eq_empty connected_components_of_eq_singleton) lemma exists_connected_component_of_superset: - assumes "connectedin X S" and ne: "topspace X \ {}" + assumes "connectedin X S" and ne: "X \ trivial_topology" shows "\C. C \ connected_components_of X \ S \ C" proof (cases "S = {}") case True then show ?thesis - using ne connected_components_of_def by blast + using ne connected_components_of_eq_empty by fastforce next case False then show ?thesis diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Function_Topology.thy Sat Jul 15 23:34:42 2023 +0100 @@ -194,6 +194,10 @@ unfolding product_topology_def using PiE_def by (auto) qed +lemma product_topology_trivial_iff: + "product_topology X I = trivial_topology \ (\i \ I. X i = trivial_topology)" + by (auto simp: PiE_eq_empty_iff simp flip: null_topspace_iff_trivial) + lemma topspace_product_topology_alt: "topspace (product_topology X I) = {x \ extensional I. \i \ I. x i \ topspace(X i)}" by (fastforce simp: PiE_iff) @@ -251,7 +255,7 @@ relative_to topspace (product_topology X I))" by (simp add: istopology_subbase product_topology) -lemma subtopology_PiE: +lemma subtopology_product_topology: "subtopology (product_topology X I) (\\<^sub>E i\I. (S i)) = product_topology (\i. subtopology (X i) (S i)) I" proof - let ?P = "\F. \i U. F = {f. f i \ U} \ i \ I \ openin (X i) U" @@ -1132,19 +1136,20 @@ lemma retraction_map_product_projection: assumes "i \ I" shows "(retraction_map (product_topology X I) (X i) (\x. x i) \ - (topspace (product_topology X I) = {}) \ topspace (X i) = {})" + ((product_topology X I) = trivial_topology) \ (X i) = trivial_topology)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs - using retraction_imp_surjective_map by force + using retraction_imp_surjective_map + by (metis image_empty subtopology_eq_discrete_topology_empty) next assume R: ?rhs show ?lhs - proof (cases "topspace (product_topology X I) = {}") + proof (cases "(product_topology X I) = trivial_topology") case True then show ?thesis - using R by (auto simp: retraction_map_def retraction_maps_def continuous_map_on_empty) + using R by (auto simp: retraction_map_def retraction_maps_def) next case False have *: "\g. continuous_map (X i) (product_topology X I) g \ (\x\topspace (X i). g x i = x)" @@ -1156,9 +1161,8 @@ using \i \ I\ that by (rule_tac x="\x j. if j = i then x else z j" in exI) (auto simp: continuous_map_componentwise PiE_iff extensional_def cm) qed - show ?thesis - using \i \ I\ False - by (auto simp: retraction_map_def retraction_maps_def assms continuous_map_product_projection *) + with \i \ I\ False assms show ?thesis + by (auto simp: retraction_map_def retraction_maps_def simp flip: null_topspace_iff_trivial) qed qed @@ -1167,7 +1171,7 @@ proposition openin_PiE_gen: "openin (product_topology X I) (PiE I S) \ PiE I S = {} \ - finite {i \ I. ~(S i = topspace(X i))} \ (\i \ I. openin (X i) (S i))" + finite {i \ I. S i \ topspace (X i)} \ (\i \ I. openin (X i) (S i))" (is "?lhs \ _ \ ?rhs") proof (cases "PiE I S = {}") case False @@ -1216,12 +1220,12 @@ proposition compact_space_product_topology: "compact_space(product_topology X I) \ - topspace(product_topology X I) = {} \ (\i \ I. compact_space(X i))" + (product_topology X I) = trivial_topology \ (\i \ I. compact_space(X i))" (is "?lhs = ?rhs") -proof (cases "topspace(product_topology X I) = {}") +proof (cases "(product_topology X I) = trivial_topology") case False then obtain z where z: "z \ (\\<^sub>E i\I. topspace(X i))" - by auto + by (auto simp flip: null_topspace_iff_trivial) show ?thesis proof assume L: ?lhs @@ -1293,16 +1297,16 @@ using UC by blast qed qed (simp add: product_topology) - qed (simp add: compact_space_topspace_empty) + qed simp qed qed -qed (simp add: compact_space_topspace_empty) +qed auto corollary compactin_PiE: "compactin (product_topology X I) (PiE I S) \ PiE I S = {} \ (\i \ I. compactin (X i) (S i))" - by (auto simp: compactin_subspace subtopology_PiE subset_PiE compact_space_product_topology - PiE_eq_empty_iff) + by (fastforce simp add: compactin_subspace subtopology_product_topology compact_space_product_topology + subset_PiE product_topology_trivial_iff subtopology_trivial_iff) lemma in_product_topology_closure_of: "z \ (product_topology X I) closure_of S @@ -1324,7 +1328,7 @@ proposition connected_space_product_topology: "connected_space(product_topology X I) \ - (\\<^sub>E i\I. topspace (X i)) = {} \ (\i \ I. connected_space(X i))" + (\i \ I. X i = trivial_topology) \ (\i \ I. connected_space(X i))" (is "?lhs \ ?eq \ ?rhs") proof (cases ?eq) case False @@ -1339,7 +1343,7 @@ by (simp add: \i \ I\ continuous_map_product_projection) show ?thesis using connectedin_continuous_map_image [OF cm ci] \i \ I\ - by (simp add: False image_projection_PiE) + by (simp add: False image_projection_PiE PiE_eq_empty_iff) qed ultimately show ?rhs by (meson connectedin_topspace) @@ -1484,13 +1488,14 @@ qed ultimately show ?thesis by simp -qed (simp add: connected_space_topspace_empty) +qed (metis connected_space_trivial_topology product_topology_trivial_iff) lemma connectedin_PiE: "connectedin (product_topology X I) (PiE I S) \ PiE I S = {} \ (\i \ I. connectedin (X i) (S i))" - by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff) + by (auto simp: connectedin_def subtopology_product_topology connected_space_product_topology subset_PiE + PiE_eq_empty_iff subtopology_trivial_iff) lemma path_connected_space_product_topology: "path_connected_space(product_topology X I) \ @@ -1509,7 +1514,7 @@ by (simp add: \i \ I\ continuous_map_product_projection) show "path_connectedin (X i) (topspace (X i))" using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]] - by (metis \i \ I\ False retraction_imp_surjective_map retraction_map_product_projection) + by (metis \i \ I\ False retraction_imp_surjective_map retraction_map_product_projection topspace_discrete_topology) qed next assume R [rule_format]: ?rhs @@ -1530,28 +1535,30 @@ qed ultimately show ?thesis by simp -qed (simp add: path_connected_space_topspace_empty) +next +qed (force simp: path_connected_space_topspace_empty iff: null_topspace_iff_trivial) lemma path_connectedin_PiE: "path_connectedin (product_topology X I) (PiE I S) \ PiE I S = {} \ (\i \ I. path_connectedin (X i) (S i))" - by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset) + by (fastforce simp add: path_connectedin_def subtopology_product_topology path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset) subsection \Projections from a function topology to a component\ lemma quotient_map_product_projection: assumes "i \ I" shows "quotient_map(product_topology X I) (X i) (\x. x i) \ - (topspace(product_topology X I) = {} \ topspace(X i) = {})" - by (metis assms image_empty quotient_imp_surjective_map retraction_imp_quotient_map - retraction_map_product_projection) + ((product_topology X I) = trivial_topology \ (X i) = trivial_topology)" + by (metis (no_types) assms image_is_empty null_topspace_iff_trivial quotient_imp_surjective_map + retraction_imp_quotient_map retraction_map_product_projection) lemma product_topology_homeomorphic_component: assumes "i \ I" "\j. \j \ I; j \ i\ \ \a. topspace(X j) = {a}" shows "product_topology X I homeomorphic_space (X i)" proof - have "quotient_map (product_topology X I) (X i) (\x. x i)" - using assms by (force simp add: quotient_map_product_projection PiE_eq_empty_iff) + using assms by (metis (full_types) discrete_topology_unique empty_not_insert + product_topology_trivial_iff quotient_map_product_projection) moreover have "inj_on (\x. x i) (\\<^sub>E i\I. topspace (X i))" using assms by (auto simp: inj_on_def PiE_iff) (metis extensionalityI singletonD) @@ -1566,15 +1573,15 @@ \ P(subtopology (product_topology X I) (PiE I (\j. if j = i then topspace(X i) else {z j})))" (is "\z i. \_; _; _\ \ P (?SX z i)") and PQ: "\X X'. X homeomorphic_space X' \ (P X \ Q X')" - shows "(\\<^sub>E i\I. topspace(X i)) = {} \ (\i \ I. Q(X i))" + shows "(\i\I. (X i) = trivial_topology) \ (\i \ I. Q(X i))" proof - - have "Q(X i)" if "(\\<^sub>E i\I. topspace(X i)) \ {}" "i \ I" for i + have "Q(X i)" if "\i\I. (X i) \ trivial_topology" "i \ I" for i proof - from that obtain f where f: "f \ (\\<^sub>E i\I. topspace (X i))" - by force + by (meson null_topspace_iff_trivial PiE_eq_empty_iff ex_in_conv) have "?SX f i homeomorphic_space X i" using f product_topology_homeomorphic_component [OF \i \ I\, of "\j. subtopology (X j) (if j = i then topspace (X i) else {f j})"] - by (force simp add: subtopology_PiE) + by (force simp add: subtopology_product_topology) then show ?thesis using minor [OF f major \i \ I\] PQ by auto qed diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Further_Topology.thy Sat Jul 15 23:34:42 2023 +0100 @@ -312,14 +312,16 @@ proof (cases "S = {}") case True then show ?thesis - by (simp add: that) + using homotopic_with_canon_on_empty that by auto next case False then show ?thesis proof (cases "T = {}") case True + then have "rel_frontier S = {}" "rel_frontier T = {}" + using fim by fastforce+ then show ?thesis - using fim that by (simp add: Pi_iff) + using that by (simp add: homotopic_on_emptyI) next case False obtain T':: "'a set" @@ -1729,7 +1731,8 @@ show ?rhs proof (cases "S = {}") case True - then show ?thesis by auto + then show ?thesis + using homotopic_with_canon_on_empty by blast next case False then have "(\c\components (- S). \ bounded c)" @@ -3767,8 +3770,9 @@ have "S = {} \ path_component (sphere 0 1) 1 c" using homotopic_with_imp_subset2 [OF that] path_connected_sphere [of "0::complex" 1] by (auto simp: path_connected_component) - then have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. 1) (\x. c)" - by (simp add: homotopic_constant_maps) + with subtopology_empty_iff_trivial + have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. 1) (\x. c)" + by (force simp add: homotopic_constant_maps) then show ?thesis using homotopic_with_symD homotopic_with_trans that by blast qed @@ -5474,7 +5478,7 @@ proof (cases "\\ = {}") case True with that show ?thesis - by force + using homotopic_with_canon_on_empty by fastforce next case False then obtain C where "C \ \" "C \ {}" @@ -5503,7 +5507,7 @@ using T \a \ T\ by (simp add: homotopic_constant_maps path_connected_component) then show ?thesis using c homotopic_with_symD homotopic_with_trans by blast - qed auto + qed (simp add: homotopic_on_empty) qed then show ?thesis .. qed diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Homotopy.thy Sat Jul 15 23:34:42 2023 +0100 @@ -284,24 +284,24 @@ by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id) lemma homotopic_on_emptyI: - assumes "topspace X = {}" "P f" "P g" - shows "homotopic_with P X X' f g" - by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal) + assumes "P f" "P g" + shows "homotopic_with P trivial_topology X f g" + by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal topspace_discrete_topology) lemma homotopic_on_empty: - "topspace X = {} \ (homotopic_with P X X' f g \ P f \ P g)" + "(homotopic_with P trivial_topology X f g \ P f \ P g)" using homotopic_on_emptyI homotopic_with_imp_property by metis -lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\x. True) {} t f g" +lemma homotopic_with_canon_on_empty: "homotopic_with_canon (\x. True) {} t f g" by (auto intro: homotopic_with_equal) lemma homotopic_constant_maps: "homotopic_with (\x. True) X X' (\x. a) (\x. b) \ - topspace X = {} \ path_component_of X' a b" (is "?lhs = ?rhs") -proof (cases "topspace X = {}") + X = trivial_topology \ path_component_of X' a b" (is "?lhs = ?rhs") +proof (cases "X = trivial_topology") case False then obtain c where c: "c \ topspace X" - by blast + by fastforce have "\g. continuous_map (top_of_set {0..1::real}) X' g \ g 0 = a \ g 1 = b" if "x \ topspace X" and hom: "homotopic_with (\x. True) X X' (\x. a) (\x. b)" for x proof - @@ -310,7 +310,7 @@ and h: "\x. h (0, x) = a" "\x. h (1, x) = b" using hom by (auto simp: homotopic_with_def) have cont: "continuous_map (top_of_set {0..1}) X' (h \ (\t. (t, c)))" - by (rule continuous_map_compose [OF _ conth] continuous_intros c | simp)+ + by (rule continuous_map_compose [OF _ conth] continuous_intros | simp add: c)+ then show ?thesis by (force simp: h) qed @@ -320,7 +320,8 @@ unfolding homotopic_with_def by (force intro!: continuous_map_compose continuous_intros c that) ultimately show ?thesis - using False by (auto simp: path_component_of_def pathin_def) + using False + by (metis c path_component_of_set pathin_def) qed (simp add: homotopic_on_empty) proposition homotopic_with_eq: @@ -423,7 +424,8 @@ have "homotopic_with_canon (\x. True) S T (\x. a) (\x. b)" by (simp add: LHS image_subset_iff that) then show ?thesis - using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto + using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] + by (metis path_component_of_canon_iff topspace_discrete_topology topspace_euclidean_subtopology) qed moreover have "\c. homotopic_with_canon (\x. True) S T f (\x. c)" if "continuous_on S f" "f \ S \ T" for f @@ -1274,7 +1276,7 @@ obtain a where a: "homotopic_with_canon (\x. True) S S id (\x. a)" using assms by (force simp: contractible_def) then have "a \ S" - by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology) + using False homotopic_with_imp_funspace2 by fastforce have "\p. path p \ path_image p \ S \ pathfinish p = pathstart p \ homotopic_loops S p (linepath a a)" @@ -1344,11 +1346,12 @@ next case False with c1 c2 have "c1 \ U" "c2 \ U" - using homotopic_with_imp_continuous_maps by fastforce+ + using homotopic_with_imp_continuous_maps + by (metis PiE equals0I homotopic_with_imp_funspace2)+ with \path_connected U\ show ?thesis by blast qed then have "homotopic_with_canon (\h. True) S U (\x. c2) (\x. c1)" - by (simp add: path_component homotopic_constant_maps) + by (auto simp add: path_component homotopic_constant_maps) then show ?thesis using c1 c2 homotopic_with_symD homotopic_with_trans by blast qed @@ -3475,16 +3478,16 @@ lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S) \ contractible S" by (auto simp: contractible_space_def contractible_def) -lemma contractible_space_empty: - "topspace X = {} \ contractible_space X" +lemma contractible_space_empty [simp]: + "contractible_space trivial_topology" unfolding contractible_space_def homotopic_with_def apply (rule_tac x=undefined in exI) apply (rule_tac x="\(t,x). if t = 0 then x else undefined" in exI) apply (auto simp: continuous_map_on_empty) done -lemma contractible_space_singleton: - "topspace X = {a} \ contractible_space X" +lemma contractible_space_singleton [simp]: + "contractible_space (discrete_topology{a})" unfolding contractible_space_def homotopic_with_def apply (rule_tac x=a in exI) apply (rule_tac x="\(t,x). if t = 0 then x else a" in exI) @@ -3493,17 +3496,17 @@ lemma contractible_space_subset_singleton: "topspace X \ {a} \ contractible_space X" - by (meson contractible_space_empty contractible_space_singleton subset_singletonD) - -lemma contractible_space_subtopology_singleton: - "contractible_space(subtopology X {a})" + by (metis contractible_space_empty contractible_space_singleton null_topspace_iff_trivial subset_singletonD subtopology_eq_discrete_topology_sing) + +lemma contractible_space_subtopology_singleton [simp]: + "contractible_space (subtopology X {a})" by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI) lemma contractible_space: "contractible_space X \ - topspace X = {} \ + X = trivial_topology \ (\a \ topspace X. homotopic_with (\x. True) X X id (\x. a))" -proof (cases "topspace X = {}") +proof (cases "X = trivial_topology") case False then show ?thesis using homotopic_with_imp_continuous_maps by (fastforce simp: contractible_space_def) @@ -3511,7 +3514,7 @@ lemma contractible_imp_path_connected_space: assumes "contractible_space X" shows "path_connected_space X" -proof (cases "topspace X = {}") +proof (cases "X = trivial_topology") case False have *: "path_connected_space X" if "a \ topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h" @@ -3552,13 +3555,13 @@ proof (rule homotopic_with_trans [OF a]) show "homotopic_with (\x. True) X X (\x. a) (\x. b)" using homotopic_constant_maps path_connected_space_imp_path_component_of - by (metis (full_types) X a continuous_map_const contractible_imp_path_connected_space homotopic_with_imp_continuous_maps that) + by (metis X a contractible_imp_path_connected_space homotopic_with_sym homotopic_with_trans path_component_of_equiv that) qed qed next assume R: ?rhs then show ?lhs - unfolding contractible_space_def by (metis equals0I homotopic_on_emptyI) + using contractible_space_def by fastforce qed @@ -3623,8 +3626,8 @@ \ homotopic_with (\h. True) X Z (g \ f) (g' \ f')" using nullhomotopic_through_contractible_space [of X Y f Z g] using nullhomotopic_through_contractible_space [of X Y f' Z g'] - by (metis continuous_map_const homotopic_constant_maps homotopic_with_imp_continuous_maps - homotopic_with_trans path_connected_space_iff_path_component homotopic_with_sym) + by (smt (verit) continuous_map_const homotopic_constant_maps homotopic_with_imp_continuous_maps + homotopic_with_symD homotopic_with_trans path_connected_space_imp_path_component_of) lemma homotopic_from_contractible_space: "continuous_map X Y f \ continuous_map X Y g \ @@ -3640,8 +3643,8 @@ lemma contractible_eq_homotopy_equivalent_singleton_subtopology: "contractible_space X \ - topspace X = {} \ (\a \ topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs") -proof (cases "topspace X = {}") + X = trivial_topology \ (\a \ topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs") +proof (cases "X = trivial_topology") case False show ?thesis proof @@ -3684,10 +3687,10 @@ lemma contractible_space_prod_topology: "contractible_space(prod_topology X Y) \ - topspace X = {} \ topspace Y = {} \ contractible_space X \ contractible_space Y" -proof (cases "topspace X = {} \ topspace Y = {}") + X = trivial_topology \ Y = trivial_topology \ contractible_space X \ contractible_space Y" +proof (cases "X = trivial_topology \ Y = trivial_topology") case True - then have "topspace (prod_topology X Y) = {}" + then have "(prod_topology X Y) = trivial_topology" by simp then show ?thesis by (auto simp: contractible_space_empty) @@ -3726,8 +3729,8 @@ lemma contractible_space_product_topology: "contractible_space(product_topology X I) \ - topspace (product_topology X I) = {} \ (\i \ I. contractible_space(X i))" -proof (cases "topspace (product_topology X I) = {}") + (product_topology X I) = trivial_topology \ (\i \ I. contractible_space(X i))" +proof (cases "(product_topology X I) = trivial_topology") case False have 1: "contractible_space (X i)" if XI: "contractible_space (product_topology X I)" and "i \ I" @@ -3749,8 +3752,8 @@ by (auto simp: contractible_space_def) qed show ?thesis - using False 1 2 by blast -qed (simp add: contractible_space_empty) + using False 1 2 by (meson equals0I subtopology_eq_discrete_topology_empty) +qed auto lemma contractible_space_subtopology_euclideanreal [simp]: @@ -3960,7 +3963,7 @@ shows "S homotopy_eqv T" proof (cases "S = {}") case True with assms show ?thesis - by (simp add: homeomorphic_imp_homotopy_eqv) + using homeomorphic_imp_homotopy_eqv by fastforce next case False with assms obtain a b where "a \ S" "b \ T" @@ -3978,7 +3981,7 @@ proof assume ?lhs then show ?rhs by (metis continuous_map_subtopology_eu empty_iff equalityI homotopy_equivalent_space_def image_subset_iff subsetI) -qed (simp add: homotopy_eqv_contractible_sets) +qed (use homeomorphic_imp_homotopy_eqv in force) lemma homotopy_eqv_empty2 [simp]: fixes S :: "'a::real_normed_vector set" @@ -3993,10 +3996,7 @@ lemma homotopy_eqv_sing: fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector" shows "S homotopy_eqv {a} \ S \ {} \ contractible S" -proof (cases "S = {}") - case False then show ?thesis - by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets) -qed simp + by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets homotopy_eqv_empty2) lemma homeomorphic_contractible_eq: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Lindelof_Spaces.thy --- a/src/HOL/Analysis/Lindelof_Spaces.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Lindelof_Spaces.thy Sat Jul 15 23:34:42 2023 +0100 @@ -28,7 +28,7 @@ lemma Lindelof_space_topspace_empty: "topspace X = {} \ Lindelof_space X" - using compact_imp_Lindelof_space compact_space_topspace_empty by blast + using compact_imp_Lindelof_space compact_space_trivial_topology by force lemma Lindelof_space_Union: assumes \: "countable \" and lin: "\U. U \ \ \ Lindelof_space (subtopology X U)" @@ -200,7 +200,7 @@ have UU_eq: "\\ = topspace X" by (meson UU fin locally_finite_in_def subset_antisym) obtain T where T: "\x. x \ topspace X \ openin X (T x) \ x \ T x \ finite {U \ \. U \ T x \ {}}" - using fin unfolding locally_finite_in_def by metis + using fin unfolding locally_finite_in_def by meson then obtain I where "countable I" "I \ topspace X" and I: "topspace X \ \(T ` I)" using X unfolding Lindelof_space_alt by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image) diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Locally.thy --- a/src/HOL/Analysis/Locally.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Locally.thy Sat Jul 15 23:34:42 2023 +0100 @@ -339,7 +339,7 @@ lemma locally_path_connected_space_product_topology: "locally_path_connected_space(product_topology X I) \ - topspace(product_topology X I) = {} \ + (product_topology X I) = trivial_topology \ finite {i. i \ I \ ~path_connected_space(X i)} \ (\i \ I. locally_path_connected_space(X i))" (is "?lhs \ ?empty \ ?rhs") @@ -350,7 +350,7 @@ next case False then obtain z where z: "z \ (\\<^sub>E i\I. topspace (X i))" - by auto + using discrete_topology_unique_derived_set by (fastforce iff: null_topspace_iff_trivial) have ?rhs if L: ?lhs proof - obtain U C where U: "openin (product_topology X I) U" @@ -474,20 +474,20 @@ lemma locally_path_connected_space_prod_topology: "locally_path_connected_space (prod_topology X Y) \ - topspace (prod_topology X Y) = {} \ + (prod_topology X Y) = trivial_topology \ locally_path_connected_space X \ locally_path_connected_space Y" (is "?lhs=?rhs") -proof (cases "topspace(prod_topology X Y) = {}") +proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis - by (metis equals0D locally_path_connected_space_def neighbourhood_base_of_def) + using locally_path_connected_space_discrete_topology by force next case False - then have ne: "topspace X \ {}" "topspace Y \ {}" + then have ne: "X \ trivial_topology" "Y \ trivial_topology" by simp_all show ?thesis proof assume ?lhs then show ?rhs - by (metis ne locally_path_connected_space_retraction_map_image retraction_map_fst retraction_map_snd) + by (meson locally_path_connected_space_quotient_map_image ne(1) ne(2) quotient_map_fst quotient_map_snd) next assume ?rhs with False have X: "locally_path_connected_space X" and Y: "locally_path_connected_space Y" @@ -789,15 +789,15 @@ (*Similar proof to locally_connected_space_prod_topology*) lemma locally_connected_space_prod_topology: "locally_connected_space (prod_topology X Y) \ - topspace (prod_topology X Y) = {} \ + (prod_topology X Y) = trivial_topology \ locally_connected_space X \ locally_connected_space Y" (is "?lhs=?rhs") -proof (cases "topspace(prod_topology X Y) = {}") +proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis using locally_connected_space_iff_weak by force next case False - then have ne: "topspace X \ {}" "topspace Y \ {}" + then have ne: "X \ trivial_topology" "Y \ trivial_topology" by simp_all show ?thesis proof @@ -832,7 +832,7 @@ (*Same proof as locally_path_connected_space_product_topology*) lemma locally_connected_space_product_topology: "locally_connected_space(product_topology X I) \ - topspace(product_topology X I) = {} \ + (product_topology X I) = trivial_topology \ finite {i. i \ I \ ~connected_space(X i)} \ (\i \ I. locally_connected_space(X i))" (is "?lhs \ ?empty \ ?rhs") @@ -843,7 +843,7 @@ next case False then obtain z where z: "z \ (\\<^sub>E i\I. topspace (X i))" - by auto + using discrete_topology_unique_derived_set by (fastforce iff: null_topspace_iff_trivial) have ?rhs if L: ?lhs proof - obtain U C where U: "openin (product_topology X I) U" @@ -1000,14 +1000,16 @@ qed qed -lemma dimension_le_eq_empty: - "X dim_le -1 \ topspace X = {}" +inductive_simps dim_le_minus2 [simp]: "X dim_le -2" + +lemma dimension_le_eq_empty [simp]: + "X dim_le -1 \ X = trivial_topology" proof - assume "X dim_le (-1)" - then show "topspace X = {}" - by (smt (verit, ccfv_threshold) Diff_empty Diff_eq_empty_iff dimension_le.cases openin_topspace subset_eq) + assume L: "X dim_le (-1)" + show "X = trivial_topology" + by (force intro: dimension_le.cases [OF L]) next - assume "topspace X = {}" + assume "X = trivial_topology" then show "X dim_le (-1)" using dimension_le.simps openin_subset by fastforce qed @@ -1015,9 +1017,10 @@ lemma dimension_le_0_neighbourhood_base_of_clopen: "X dim_le 0 \ neighbourhood_base_of (\U. closedin X U \ openin X U) X" proof - - have "(subtopology X (X frontier_of U) dim_le -1) = - closedin X U" if "openin X U" for U - by (metis dimension_le_eq_empty frontier_of_eq_empty frontier_of_subset_topspace openin_subset that topspace_subtopology_subset) + have "(subtopology X (X frontier_of U) dim_le -1) = closedin X U" + if "openin X U" for U + using that clopenin_eq_frontier_of openin_subset + by (fastforce simp add: subtopology_trivial_iff frontier_of_subset_topspace Int_absorb1) then show ?thesis by (smt (verit, del_insts) dimension_le.simps open_neighbourhood_base_of) qed diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Sat Jul 15 23:34:42 2023 +0100 @@ -2181,11 +2181,11 @@ qed (auto simp: path_connected_space_path_component_set) lemma path_components_of_eq_empty: - "path_components_of X = {} \ topspace X = {}" - using Union_path_components_of nonempty_path_components_of by fastforce + "path_components_of X = {} \ X = trivial_topology" + by (metis image_is_empty path_components_of_def subtopology_eq_discrete_topology_empty) lemma path_components_of_empty_space: - "topspace X = {} \ path_components_of X = {}" + "path_components_of trivial_topology = {}" by (simp add: path_components_of_eq_empty) lemma path_components_of_subset_singleton: @@ -2294,7 +2294,8 @@ by (simp add: path_component_of_subset_topspace) moreover have "g ` Collect(path_component_of Y (f x)) \ Collect (path_component_of X (g (f x)))" using f g x unfolding homeomorphic_maps_def - by (metis image_Collect_subsetI image_eqI mem_Collect_eq path_component_of_equiv path_component_of_maximal path_connectedin_continuous_map_image path_connectedin_path_component_of) + by (metis image_Collect_subsetI image_eqI mem_Collect_eq path_component_of_equiv path_component_of_maximal + path_connectedin_continuous_map_image path_connectedin_path_component_of) ultimately show "Collect (path_component_of Y (f x)) \ f ` Collect (path_component_of X x)" using g x unfolding homeomorphic_maps_def continuous_map_def image_iff subset_iff by metis @@ -2329,7 +2330,7 @@ proof (cases "topspace(prod_topology X Y) = {}") case True then show ?thesis - by (simp add: path_connected_space_topspace_empty) + using path_connected_space_topspace_empty by force next case False have "path_connected_space (prod_topology X Y)" @@ -2352,8 +2353,8 @@ qed qed then show ?thesis - by (metis False Sigma_empty1 Sigma_empty2 topspace_prod_topology path_connected_space_retraction_map_image - retraction_map_fst retraction_map_snd) + by (metis False path_connected_space_quotient_map_image prod_topology_trivial1 prod_topology_trivial2 + quotient_map_fst quotient_map_snd topspace_discrete_topology) qed lemma path_connectedin_Times: diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Product_Topology.thy --- a/src/HOL/Analysis/Product_Topology.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Product_Topology.thy Sat Jul 15 23:34:42 2023 +0100 @@ -54,6 +54,10 @@ finally show ?thesis . qed +lemma prod_topology_trivial_iff [simp]: + "prod_topology X Y = trivial_topology \ X = trivial_topology \ Y = trivial_topology" + by (metis (full_types) Sigma_empty1 null_topspace_iff_trivial subset_empty times_subset_iff topspace_prod_topology) + lemma subtopology_Times: shows "subtopology (prod_topology X Y) (S \ T) = prod_topology (subtopology X S) (subtopology Y T)" proof - @@ -142,11 +146,11 @@ text \Missing the opposite direction. Does it hold? A converse is proved for proper maps, a stronger condition\ lemma closed_map_prod: assumes "closed_map (prod_topology X Y) (prod_topology X' Y') (\(x,y). (f x, g y))" - shows "topspace(prod_topology X Y) = {} \ closed_map X X' f \ closed_map Y Y' g" -proof (cases "topspace(prod_topology X Y) = {}") + shows "(prod_topology X Y) = trivial_topology \ closed_map X X' f \ closed_map Y Y' g" +proof (cases "(prod_topology X Y) = trivial_topology") case False then have ne: "topspace X \ {}" "topspace Y \ {}" - by auto + by (auto simp flip: null_topspace_iff_trivial) have "closed_map X X' f" unfolding closed_map_def proof (intro strip) @@ -271,6 +275,12 @@ \ continuous_map X Y (\x. if P then f x else g x)" by simp +lemma prod_topology_trivial1 [simp]: "prod_topology trivial_topology Y = trivial_topology" + using continuous_map_fst continuous_map_on_empty2 by blast + +lemma prod_topology_trivial2 [simp]: "prod_topology X trivial_topology = trivial_topology" + using continuous_map_snd continuous_map_on_empty2 by blast + 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 @@ -278,20 +288,22 @@ 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) + "quotient_map(prod_topology X Y) X fst \ (Y = trivial_topology \ X = trivial_topology)" + apply (simp add: continuous_open_quotient_map open_map_fst continuous_map_fst) + by (metis null_topspace_iff_trivial) 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) + "quotient_map(prod_topology X Y) Y snd \ (X = trivial_topology \ Y = trivial_topology)" + apply (simp add: continuous_open_quotient_map open_map_snd continuous_map_snd) + by (metis null_topspace_iff_trivial) lemma retraction_map_fst: - "retraction_map (prod_topology X Y) X fst \ (topspace Y = {} \ topspace X = {})" -proof (cases "topspace Y = {}") + "retraction_map (prod_topology X Y) X fst \ (Y = trivial_topology \ X = trivial_topology)" +proof (cases "Y = trivial_topology") 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) + by (auto simp: retraction_map_def retraction_maps_def continuous_map_pairwise) next case False have "\g. continuous_map X (prod_topology X Y) g \ (\x\topspace X. fst (g x) = x)" @@ -304,12 +316,12 @@ qed lemma retraction_map_snd: - "retraction_map (prod_topology X Y) Y snd \ (topspace X = {} \ topspace Y = {})" -proof (cases "topspace X = {}") + "retraction_map (prod_topology X Y) Y snd \ (X = trivial_topology \ Y = trivial_topology)" +proof (cases "X = trivial_topology") 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) + by (fastforce simp: retraction_map_def retraction_maps_def continuous_map_fst) next case False have "\g. continuous_map Y (prod_topology X Y) g \ (\y\topspace Y. snd (g y) = y)" @@ -323,8 +335,8 @@ 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 = {}") + "continuous_map (prod_topology X Y) Z (f \ fst) \ Y = trivial_topology \ continuous_map X Z f" +proof (cases "Y = trivial_topology") case True then show ?thesis by (simp add: continuous_map_on_empty) @@ -335,8 +347,8 @@ 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 = {}") + "continuous_map (prod_topology X Y) Z (f \ snd) \ X = trivial_topology \ continuous_map Y Z f" +proof (cases "X = trivial_topology") case True then show ?thesis by (simp add: continuous_map_on_empty) @@ -348,16 +360,13 @@ 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 + (prod_topology X Y) = trivial_topology \ continuous_map X X' f \ continuous_map Y Y' g" +proof (cases "(prod_topology X Y) = trivial_topology") 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 + by (auto simp: continuous_map_paired case_prod_unfold + continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def]) +qed auto lemma in_prod_topology_closure_of: assumes "z \ (prod_topology X Y) closure_of S" @@ -368,11 +377,11 @@ 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) = {}") + "compact_space(prod_topology X Y) \ (prod_topology X Y) = trivial_topology \ compact_space X \ compact_space Y" +proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis - using compact_space_topspace_empty by blast + by fastforce next case False then have non_mt: "topspace X \ {}" "topspace Y \ {}" @@ -385,7 +394,7 @@ 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) + using non_mt by (auto simp: compact_space_def) qed moreover define \ where "\ \ (\V. topspace X \ V) ` Collect (openin Y)" @@ -483,28 +492,26 @@ 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) + by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology subtopology_trivial_iff) + 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') = {} + (prod_topology X Y) = trivial_topology \ (prod_topology X' Y') = trivial_topology \ homeomorphic_maps X X' f f' \ homeomorphic_maps Y Y' g g'" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" - unfolding homeomorphic_maps_def continuous_map_prod_top - by (auto simp: continuous_map_on_empty continuous_map_on_empty2 ball_conj_distrib) + by (fastforce simp: homeomorphic_maps_def continuous_map_prod_top ball_conj_distrib) next show "?rhs \ ?lhs" - unfolding homeomorphic_maps_def - by (auto simp: continuous_map_prod_top continuous_map_on_empty continuous_map_on_empty2) + by (auto simp: homeomorphic_maps_def continuous_map_prod_top) qed lemma homeomorphic_maps_swap: - "homeomorphic_maps (prod_topology X Y) (prod_topology Y X) - (\(x,y). (y,x)) (\(y,x). (x,y))" + "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: @@ -542,23 +549,25 @@ 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" + "Y = discrete_topology {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) + apply (rule_tac x=fst in exI) + apply (simp add: homeomorphic_map_def inj_on_def discrete_topology_unique flip: homeomorphic_map_maps) + done lemma prod_topology_homeomorphic_space_right: - "topspace X = {a} \ prod_topology X Y homeomorphic_space Y" + "X = discrete_topology {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) + by (meson homeomorphic_space_def homeomorphic_space_prod_topology_swap homeomorphic_space_trans prod_topology_homeomorphic_space_left) 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) + by (metis empty_subsetI homeomorphic_space_sym insert_subset prod_topology_homeomorphic_space_left subtopology_eq_discrete_topology_sing topspace_subtopology_subset) 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) + by (metis empty_subsetI homeomorphic_space_sym insert_subset prod_topology_homeomorphic_space_right subtopology_eq_discrete_topology_sing topspace_subtopology_subset) lemma topological_property_of_prod_component: assumes major: "P(prod_topology X Y)" @@ -566,7 +575,7 @@ 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" + shows "(prod_topology X Y) = trivial_topology \ Q X \ R Y" proof - have "Q X \ R Y" if "topspace(prod_topology X Y) \ {}" proof - @@ -576,7 +585,7 @@ 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 + then show ?thesis by force qed lemma limitin_pairwise: @@ -625,11 +634,11 @@ proposition connected_space_prod_topology: "connected_space(prod_topology X Y) \ - topspace(prod_topology X Y) = {} \ connected_space X \ connected_space Y" (is "?lhs=?rhs") -proof (cases "topspace(prod_topology X Y) = {}") + (prod_topology X Y) = trivial_topology \ connected_space X \ connected_space Y" (is "?lhs=?rhs") +proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis - using connected_space_topspace_empty by blast + by auto next case False then have nonempty: "topspace X \ {}" "topspace Y \ {}" @@ -638,7 +647,8 @@ proof assume ?lhs then show ?rhs - by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd) + by (metis connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd + subtopology_eq_discrete_topology_empty) next assume ?rhs then have conX: "connected_space X" and conY: "connected_space Y" @@ -684,7 +694,7 @@ lemma connectedin_Times: "connectedin (prod_topology X Y) (S \ T) \ S = {} \ T = {} \ connectedin X S \ connectedin Y T" - by (force simp: connectedin_def subtopology_Times connected_space_prod_topology) + by (auto simp: connectedin_def subtopology_Times connected_space_prod_topology subtopology_trivial_iff) end diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Retracts.thy --- a/src/HOL/Analysis/Retracts.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Retracts.thy Sat Jul 15 23:34:42 2023 +0100 @@ -1910,7 +1910,7 @@ (is "?lhs = ?rhs") proof (cases "S = {}") case True then show ?thesis - by simp + by (simp add: homotopic_on_emptyI) next case False have "closed S" "bounded S" diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/T1_Spaces.thy --- a/src/HOL/Analysis/T1_Spaces.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/T1_Spaces.thy Sat Jul 15 23:34:42 2023 +0100 @@ -17,7 +17,7 @@ "t1_space X \ (\x \ topspace X. \y \ topspace X. x\y \ (\U. closedin X U \ x \ U \ y \ U))" by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def) -lemma t1_space_empty: "topspace X = {} \ t1_space X" +lemma t1_space_empty [iff]: "t1_space trivial_topology" by (simp add: t1_space_def) lemma t1_space_derived_set_of_singleton: @@ -176,15 +176,15 @@ proposition t1_space_product_topology: "t1_space (product_topology X I) -\ topspace(product_topology X I) = {} \ (\i \ I. t1_space (X i))" -proof (cases "topspace(product_topology X I) = {}") +\ (product_topology X I) = trivial_topology \ (\i \ I. t1_space (X i))" +proof (cases "(product_topology X I) = trivial_topology") case True then show ?thesis - using True t1_space_empty by blast + using True t1_space_empty by force next case False then obtain f where f: "f \ (\\<^sub>E i\I. topspace(X i))" - by fastforce + using discrete_topology_unique by (fastforce iff: null_topspace_iff_trivial) have "t1_space (product_topology X I) \ (\i\I. t1_space (X i))" proof (intro iffI ballI) show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \ I" for i @@ -210,17 +210,19 @@ qed lemma t1_space_prod_topology: - "t1_space(prod_topology X Y) \ topspace(prod_topology X Y) = {} \ t1_space X \ t1_space Y" -proof (cases "topspace (prod_topology X Y) = {}") + "t1_space(prod_topology X Y) \ (prod_topology X Y) = trivial_topology \ t1_space X \ t1_space Y" +proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis - by (auto simp: t1_space_empty) + by auto next case False - have eq: "{(x,y)} = {x} \ {y}" for x y + have eq: "{(x,y)} = {x} \ {y}" for x::'a and y::'b by simp have "t1_space (prod_topology X Y) \ (t1_space X \ t1_space Y)" - using False - by (force simp: t1_space_closedin_singleton closedin_prod_Times_iff eq simp del: insert_Times_insert) + using False + apply(simp add: t1_space_closedin_singleton closedin_prod_Times_iff eq + del: insert_Times_insert flip: null_topspace_iff_trivial ex_in_conv) + by blast with False show ?thesis by simp qed @@ -237,8 +239,7 @@ "\Hausdorff_space X; topspace X = topspace Y; \U. openin X U \ openin Y U\ \ Hausdorff_space Y" by (metis Hausdorff_space_def) -lemma Hausdorff_space_topspace_empty: - "topspace X = {} \ Hausdorff_space X" +lemma Hausdorff_space_topspace_empty [iff]: "Hausdorff_space trivial_topology" by (simp add: Hausdorff_space_def) lemma Hausdorff_imp_t1_space: @@ -604,7 +605,7 @@ by (metis (mono_tags, lifting) Pair_inject inj_onI) lemma Hausdorff_space_prod_topology: - "Hausdorff_space(prod_topology X Y) \ topspace(prod_topology X Y) = {} \ Hausdorff_space X \ Hausdorff_space Y" + "Hausdorff_space(prod_topology X Y) \ (prod_topology X Y) = trivial_topology \ Hausdorff_space X \ Hausdorff_space Y" (is "?lhs = ?rhs") proof assume ?lhs @@ -655,7 +656,7 @@ then show "x = x' \ y = y'" by blast qed - qed (simp add: Hausdorff_space_topspace_empty) + qed force qed @@ -665,16 +666,15 @@ proof assume ?lhs then show ?rhs - apply (rule topological_property_of_product_component) - apply (blast dest: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)+ - done + by (simp add: Hausdorff_space_subtopology PiE_eq_empty_iff homeomorphic_Hausdorff_space + topological_property_of_product_component) next assume R: ?rhs show ?lhs proof (cases "(\\<^sub>E i\I. topspace(X i)) = {}") case True then show ?thesis - by (simp add: Hausdorff_space_topspace_empty) + by (simp add: Hausdorff_space_def) next case False have "\U V. openin (product_topology X I) U \ openin (product_topology X I) V \ f \ U \ g \ V \ disjnt U V" diff -r 19c617950a8e -r 6bae28577994 src/HOL/Analysis/Urysohn.thy --- a/src/HOL/Analysis/Urysohn.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Analysis/Urysohn.thy Sat Jul 15 23:34:42 2023 +0100 @@ -1152,7 +1152,7 @@ lemma completely_regular_space_prod_topology: "completely_regular_space (prod_topology X Y) \ - topspace (prod_topology X Y) = {} \ + (prod_topology X Y) = trivial_topology \ completely_regular_space X \ completely_regular_space Y" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs @@ -1161,7 +1161,7 @@ next assume R: ?rhs show ?lhs - proof (cases "topspace(prod_topology X Y) = {}") + proof (cases "(prod_topology X Y) = trivial_topology") case False then have X: "completely_regular_space X" and Y: "completely_regular_space Y" using R by blast+ @@ -1206,7 +1206,7 @@ proposition completely_regular_space_product_topology: "completely_regular_space (product_topology X I) \ - (\\<^sub>E i\I. topspace(X i)) = {} \ (\i \ I. completely_regular_space (X i))" + (\i\I. X i = trivial_topology) \ (\i \ I. completely_regular_space (X i))" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs @@ -1215,7 +1215,7 @@ next assume R: ?rhs show ?lhs - proof (cases "(\\<^sub>E i\I. topspace(X i)) = {}") + proof (cases "\i\I. X i = trivial_topology") case False show ?thesis unfolding completely_regular_space_alt' @@ -2062,9 +2062,9 @@ by (simp add: Hausdorff_space_def) next case False - then have "kc_space X" + with R True have "kc_space X" using kc_space_retraction_map_image [of "prod_topology X (subtopology X (topspace X - {a}))" X fst] - by (metis Diff_subset R True insert_Diff retraction_map_fst topspace_subtopology_subset) + by (metis Diff_subset insert_Diff retraction_map_fst topspace_discrete_topology topspace_subtopology_subset) have "closedin (subtopology (prod_topology X (subtopology X (topspace X - {a}))) K) (K \ D)" if "compactin (prod_topology X (subtopology X (topspace X - {a}))) K" for K proof (intro closedin_subtopology_Int_subset[where V=K] closedin_subset_topspace) @@ -3198,7 +3198,7 @@ lemma mdist_cfunspace_le: assumes "0 \ B" and B: "\x. x \ topspace X \ mdist m (f x) (g x) \ B" shows "mdist (cfunspace X m) f g \ B" -proof (cases "topspace X = {}") +proof (cases "X = trivial_topology") case True then show ?thesis by (simp add: Metric_space.fdist_empty \B\0\ cfunspace_def) @@ -3236,7 +3236,7 @@ by (metis cfunspace_subset_funspace mdist_Self mspace_Self mspace_funspace) qed show ?thesis - proof (cases "topspace X = {}") + proof (cases "X = trivial_topology") case True then show ?thesis by (simp add: mcomplete_of_def mcomplete_trivial_singleton mdist_cfunspace_eq_mdist_funspace cong: conj_cong) @@ -3272,12 +3272,15 @@ proof - have *: "d (\ N x0) (g x0) \ \/3" if "x0 \ topspace X" for x0 proof - - have "bdd_above ((\x. d (\ N x) (g x)) ` topspace X)" - by (metis F.limit_metric_sequentially False N bdd_above_dist g order_refl) + have "g \ fspace (topspace X)" + using F.limit_metric_sequentially g by blast + with N that have "bdd_above ((\x. d (\ N x) (g x)) ` topspace X)" + by (force intro: bdd_above_dist) then have "d (\ N x0) (g x0) \ Sup ((\x. d (\ N x) (g x)) ` topspace X)" by (simp add: cSup_upper that) also have "\ \ \/3" - by (smt (verit) F.limit_metric_sequentially False N Sup.SUP_cong fdist_def g order_refl) + using g False N \g \ fspace (topspace X)\ + by (fastforce simp: F.limit_metric_sequentially fdist_def) finally show ?thesis . qed have "d (g x) (g y) \ d (g x) (\ N x) + d (\ N x) (g y)" @@ -4880,11 +4883,11 @@ by (metis top closedin_topspace) have "subtopology mtopology (\(S ` I)) homeomorphic_space mtopology" by (simp add: True product_topology_empty_discrete) - also have "\ homeomorphic_space (prod_topology mtopology (powertop_real {}))" - by (metis PiE_empty_domain homeomorphic_space_sym prod_topology_homeomorphic_space_left topspace_product_topology) + also have "\ homeomorphic_space (prod_topology mtopology (discrete_topology {\x. undefined}))" + by (meson homeomorphic_space_sym prod_topology_homeomorphic_space_left) finally show "subtopology mtopology (\(S ` I)) homeomorphic_space subtopology (prod_topology mtopology (powertop_real I)) (M \ {(\x. undefined)})" - by (smt (verit) True subtopology_topspace top) + by (smt (verit, ccfv_SIG) True product_topology_empty_discrete subtopology_topspace top) qed next case False @@ -5461,8 +5464,12 @@ show ?case proof (cases "n\1") case True - with less.prems connected_components_of_empty_space show ?thesis - by (force simp add: le_Suc_eq eqpoll_iff_finite_card card_Suc_eq simp flip: ex_simps) + with less.prems have "topspace X \ {}" "n=1" + by (fastforce simp add: connected_components_of_def)+ + then have "{} \ {topspace X}" + by blast + with \n=1\ show ?thesis + by (simp add: eqpoll_iff_finite_card card_Suc_eq flip: ex_simps) next case False then have "n-1 \ 0" diff -r 19c617950a8e -r 6bae28577994 src/HOL/Homology/Homology_Groups.thy --- a/src/HOL/Homology/Homology_Groups.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Homology/Homology_Groups.thy Sat Jul 15 23:34:42 2023 +0100 @@ -1709,7 +1709,7 @@ shows "homology_group 0 X \ integer_group" proof - obtain a where a: "a \ topspace X" - using assms by auto + using assms by blast have "singular_simplex 0 X (restrict (\x. a) (standard_simplex 0))" by (simp add: singular_simplex_def a) then show ?thesis @@ -2084,7 +2084,7 @@ using that by auto show "inj_on (hom_induced p (subtopology X {}) {} X {} id) (carrier (homology_group p (subtopology X {})))" - by auto + by (meson inj_on_hom_induced_inclusion) show "hom_induced p X {} X {} id ` carrier (homology_group p X) = carrier (homology_group p X)" by (metis epi_hom_induced_relativization) next diff -r 19c617950a8e -r 6bae28577994 src/HOL/Homology/Invariance_of_Domain.thy --- a/src/HOL/Homology/Invariance_of_Domain.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Homology/Invariance_of_Domain.thy Sat Jul 15 23:34:42 2023 +0100 @@ -358,7 +358,7 @@ have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = ?hi_ee f u" proof - have ne: "topspace (nsphere n) \ equator n \ {}" - by (metis equ(1) nonempty_nsphere topspace_subtopology) + using False equator_def in_topspace_nsphere by fastforce have eq1: "hom_boundary n (nsphere n) (equator n) u = \\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>" using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force @@ -2132,7 +2132,7 @@ proof (cases "S = {}") case True with assms show ?thesis - using homeomorphic_empty_space nonempty_Euclidean_space by fastforce + using homeomorphic_empty_space nontrivial_Euclidean_space by fastforce next case False then obtain a where "a \ S" diff -r 19c617950a8e -r 6bae28577994 src/HOL/Homology/Simplices.thy --- a/src/HOL/Homology/Simplices.thy Wed Jul 12 23:11:59 2023 +0100 +++ b/src/HOL/Homology/Simplices.thy Sat Jul 15 23:34:42 2023 +0100 @@ -389,7 +389,7 @@ lemma singular_cycle: "singular_relcycle p X {} c \ singular_chain p X c \ chain_boundary p c = 0" - by (simp add: singular_relcycle_def) + using mod_subset_empty by (auto simp: singular_relcycle_def) lemma singular_cycle_mono: "\singular_relcycle p (subtopology X T) {} c; T \ S\ @@ -428,11 +428,11 @@ lemma singular_boundary: "singular_relboundary p X {} c \ (\d. singular_chain (Suc p) X d \ chain_boundary (Suc p) d = c)" - by (simp add: singular_relboundary_def) + by (meson mod_subset_empty singular_relboundary_def) lemma singular_boundary_imp_chain: "singular_relboundary p X {} c \ singular_chain p X c" - by (auto simp: singular_relboundary singular_chain_boundary_alt singular_chain_empty topspace_subtopology) + by (auto simp: singular_relboundary singular_chain_boundary_alt singular_chain_empty) lemma singular_boundary_mono: "\T \ S; singular_relboundary p (subtopology X T) {} c\