--- 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. \<forall>i\<ge>n. x i = 0}"
by (simp add: Euclidean_space_def)
-lemma nonempty_Euclidean_space: "topspace(Euclidean_space n) \<noteq> {}"
- by (force simp: topspace_Euclidean_space)
+lemma nontrivial_Euclidean_space: "Euclidean_space n \<noteq> trivial_topology"
+ using topspace_Euclidean_space [of n] by force
lemma subset_Euclidean_space [simp]:
"topspace(Euclidean_space m) \<subseteq> topspace(Euclidean_space n) \<longleftrightarrow> m \<le> 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) \<longleftrightarrow> 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\<open>n-dimensional spheres\<close>
@@ -188,8 +189,8 @@
lemma in_topspace_nsphere: "(\<lambda>n. if n = 0 then 1 else 0) \<in> topspace (nsphere n)"
by (simp add: nsphere_def topspace_Euclidean_space power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
-lemma nonempty_nsphere [simp]: "~ (topspace(nsphere n) = {})"
- using in_topspace_nsphere by auto
+lemma nonempty_nsphere [simp]: "(nsphere n) \<noteq> 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 ((\<lambda>x. f x k) \<circ> 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)
--- 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 = {} \<Longrightarrow> 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 @@
\<exists>M d. Metric_space M d \<and> Metric_space.mcomplete M d \<and> X = Metric_space.mtopology M d"
lemma empty_completely_metrizable_space:
- "topspace X = {} \<Longrightarrow> 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) \<longleftrightarrow>
- topspace(prod_topology X Y) = {} \<or> metrizable_space X \<and> metrizable_space Y"
+ (prod_topology X Y) = trivial_topology \<or> metrizable_space X \<and> metrizable_space Y"
(is "?lhs \<longleftrightarrow> ?rhs")
-proof (cases "topspace(prod_topology X Y) = {}")
+proof (cases "(prod_topology X Y) = trivial_topology")
case False
then obtain x y where "x \<in> topspace X" "y \<in> topspace Y"
- by auto
+ by fastforce
show ?thesis
proof
show "?rhs \<Longrightarrow> ?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) \<longleftrightarrow>
- topspace(prod_topology X Y) = {} \<or>
+ (prod_topology X Y) = trivial_topology \<or>
completely_metrizable_space X \<and> completely_metrizable_space Y"
(is "?lhs \<longleftrightarrow> ?rhs")
-proof (cases "topspace(prod_topology X Y) = {}")
+proof (cases "(prod_topology X Y) = trivial_topology")
case False
then obtain x y where "x \<in> topspace X" "y \<in> topspace Y"
- by auto
+ by fastforce
show ?thesis
proof
show "?rhs \<Longrightarrow> ?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 \<open>The "atin-within" filter for topologies\<close>
@@ -4809,12 +4812,12 @@
lemma metrizable_topology_A:
assumes "metrizable_space (product_topology X I)"
- shows "topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. metrizable_space (X i))"
+ shows "(product_topology X I) = trivial_topology \<or> (\<forall>i \<in> 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) = {} \<or> (\<forall>i \<in> I. completely_metrizable_space (X i))"
+ shows "(product_topology X I) = trivial_topology \<or> (\<forall>i \<in> 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) \<longleftrightarrow>
- topspace (product_topology X I) = {} \<or>
+ (product_topology X I) = trivial_topology \<or>
countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
(\<forall>i \<in> 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) \<longleftrightarrow>
- topspace (product_topology X I) = {} \<or>
+ (product_topology X I) = trivial_topology \<or>
countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
(\<forall>i \<in> 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:
--- 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) \<longleftrightarrow> topspace (prod_topology X Y) = {} \<or> t0_space X \<and> t0_space Y" (is "?lhs=?rhs")
+ "t0_space (prod_topology X Y) \<longleftrightarrow> prod_topology X Y = trivial_topology \<or> t0_space X \<and> 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) \<longleftrightarrow>
- topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t0_space (X i))" (is "?lhs=?rhs")
+ "t0_space (product_topology X I) \<longleftrightarrow> product_topology X I = trivial_topology \<or> (\<forall>i \<in> 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') (\<lambda>(x,y). (f x, g y)) \<longleftrightarrow>
- topspace(prod_topology X Y) = {} \<or> proper_map X X' f \<and> proper_map Y Y' g"
+ (prod_topology X Y) = trivial_topology \<or> proper_map X X' f \<and> proper_map Y Y' g"
(is "?lhs \<longleftrightarrow> _ \<or> ?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 \<noteq> {}" "topspace Y \<noteq> {}"
@@ -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 = {} \<Longrightarrow> 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 \<and> Hausdorff_space X \<longleftrightarrow>
neighbourhood_base_of (\<lambda>C. closedin X C \<and> Hausdorff_space(subtopology X C)) X" (is "?lhs=?rhs")
@@ -2181,7 +2176,7 @@
lemma regular_space_prod_topology:
"regular_space (prod_topology X Y) \<longleftrightarrow>
- topspace X = {} \<or> topspace Y = {} \<or> regular_space X \<and> regular_space Y" (is "?lhs=?rhs")
+ X = trivial_topology \<or> Y = trivial_topology \<or> regular_space X \<and> 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 = {} \<or> topspace Y = {}")
- case True
- then show ?thesis
- by (simp add: regular_space_topspace_empty)
+ proof (cases "X = trivial_topology \<or> 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) \<longleftrightarrow>
- topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. regular_space (X i))" (is "?lhs=?rhs")
+ (product_topology X I) = trivial_topology \<or> (\<forall>i \<in> 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 \<in> topspace (product_topology X I)"
- by blast
+ by (meson ex_in_conv null_topspace_iff_trivial)
define \<F> where "\<F> \<equiv> {Pi\<^sub>E I U |U. finite {i \<in> I. U i \<noteq> topspace (X i)}
\<and> (\<forall>i\<in>I. openin (X i) (U i))}"
have oo: "openin (product_topology X I) = arbitrary union_of (\<lambda>W. W \<in> \<F>)"
@@ -2957,20 +2950,20 @@
lemma locally_compact_space_prod_topology:
"locally_compact_space (prod_topology X Y) \<longleftrightarrow>
- topspace (prod_topology X Y) = {} \<or>
+ (prod_topology X Y) = trivial_topology \<or>
locally_compact_space X \<and> 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 \<in> topspace X" "z \<in> 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) \<longleftrightarrow>
- topspace(product_topology X I) = {} \<or>
+ product_topology X I = trivial_topology \<or>
finite {i \<in> I. \<not> compact_space(X i)} \<and> (\<forall>i \<in> 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 \<in> 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 \<in> U" "U \<subseteq> C"
by (meson locally_compact_space_def)
then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}" and "\<forall>i \<in> 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 = {} \<longleftrightarrow> topspace X = {}"
+ "quasi_components_of X = {} \<longleftrightarrow> X = trivial_topology"
by (simp add: quasi_components_of_def)
-lemma quasi_components_of_empty_space:
- "topspace X = {} \<Longrightarrow> 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 \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
+ "quasi_components_of X \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (X = trivial_topology \<or> 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} \<longleftrightarrow>
- connected_space X \<and> \<not> (topspace X = {}) \<and> S = topspace X"
- by (metis ccpo_Sup_singleton insert_not_empty quasi_components_of_subset_sing subset_singleton_iff)
+ connected_space X \<and> \<not> (X = trivial_topology) \<and> 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
- \<Longrightarrow> quasi_components_of X = (if topspace X = {} then {} else {topspace X})"
+ \<Longrightarrow> 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 \<in> connected_components_of (subtopology X K)" and "C \<subseteq> 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"
--- 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} \<longleftrightarrow> topspace X = {a}"
by (metis discrete_topology_unique openin_topspace singletonD)
+abbreviation trivial_topology where "trivial_topology \<equiv> discrete_topology {}"
+
+lemma null_topspace_iff_trivial [simp]: "topspace X = {} \<longleftrightarrow> X = trivial_topology"
+ by (simp add: subtopology_eq_discrete_topology_empty)
subsection \<open>Subspace topology\<close>
@@ -316,6 +320,9 @@
unfolding openin_subtopology
by auto (metis IntD1 in_mono openin_subset)
+lemma subtopology_trivial_iff: "subtopology X S = trivial_topology \<longleftrightarrow> X = trivial_topology \<or> topspace X \<inter> S = {}"
+ by (auto simp flip: null_topspace_iff_trivial)
+
lemma subtopology_subtopology:
"subtopology (subtopology X S) T = subtopology X (S \<inter> 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 \<inter> S) = subtopology X S"
by (metis subtopology_subtopology subtopology_topspace)
@@ -372,11 +382,11 @@
"closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
-lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
+lemma closedin_topspace_empty [simp]: "closedin trivial_topology S \<longleftrightarrow> S = {}"
by (simp add: closedin_def)
-lemma open_in_topspace_empty:
- "topspace X = {} \<Longrightarrow> openin X S \<longleftrightarrow> S = {}"
+lemma openin_topspace_empty [simp]:
+ "openin trivial_topology S \<longleftrightarrow> 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 \<noteq> trivial_topology"
+ by (simp add: subtopology_eq_discrete_topology_empty)
+
+
subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>
abbreviation euclideanreal :: "real topology"
@@ -1470,11 +1484,11 @@
"continuous_map X Y f \<Longrightarrow> f \<in> topspace X \<rightarrow> topspace Y"
by (auto simp: continuous_map_def)
-lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> 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 = {} \<Longrightarrow> continuous_map X Y f \<longleftrightarrow> topspace X = {}"
- by (auto simp: continuous_map_def)
+lemma continuous_map_on_empty2 [simp]: "continuous_map X trivial_topology f \<longleftrightarrow> X = trivial_topology"
+ using continuous_map_image_subset_topspace by fastforce
lemma continuous_map_closedin:
"continuous_map X Y f \<longleftrightarrow>
@@ -1633,9 +1647,9 @@
qed
lemma continuous_map_const [simp]:
- "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
-proof (cases "topspace X = {}")
- case False
+ "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> X = trivial_topology \<or> C \<in> topspace Y"
+proof (cases "X = trivial_topology")
+ case nontriv: False
show ?thesis
proof (cases "C \<in> 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 \<Longrightarrow> f \<in> (topspace X1) \<rightarrow> topspace X2"
unfolding open_map_def using openin_subset by fastforce
-lemma open_map_on_empty:
- "topspace X = {} \<Longrightarrow> 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 = {} \<Longrightarrow> 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 (\<lambda>x. c) \<longleftrightarrow> topspace X = {} \<or> closedin Y {c}"
- by (metis closed_map_def closed_map_on_empty closedin_empty closedin_topspace image_constant_conv)
+ "closed_map X Y (\<lambda>x. c) \<longleftrightarrow> X = trivial_topology \<or> 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:
"\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f \<in> S \<rightarrow> topspace X2"
@@ -3063,14 +3076,14 @@
using homeomorphic_space_def by blast
lemma homeomorphic_empty_space:
- "X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
- by (metis homeomorphic_eq_everything_map homeomorphic_space image_is_empty)
+ "X homeomorphic_space Y \<Longrightarrow> X = trivial_topology \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 = {} \<Longrightarrow> 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} \<longleftrightarrow> a \<in> 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 = {} \<Longrightarrow> 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 \<longleftrightarrow>
(\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
(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 \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
by (auto simp: ex_finite_subset_image \<V>_def)
moreover have "\<F> \<noteq> {}"
- using \<F> \<open>topspace X \<noteq> {}\<close> by blast
+ using \<F> False by force
ultimately show "False"
using * [of \<F>]
by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
@@ -3736,7 +3746,7 @@
fix \<U> :: "'a set set"
define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
assume "\<forall>C\<in>\<U>. openin X C" and "topspace X \<subseteq> \<Union>\<U>"
- with \<open>topspace X \<noteq> {}\<close> have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
+ with False have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
by (auto simp: \<V>_def)
show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>"
proof (rule ccontr; simp)
@@ -4965,8 +4975,7 @@
qed
qed (simp add: proper_imp_closed_map)
-lemma proper_map_on_empty:
- "topspace X = {} \<Longrightarrow> 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 (\<lambda>x. c) \<longleftrightarrow> compact_space X \<and> (topspace X = {} \<or> closedin Y {c})"
-proof (cases "topspace X = {}")
+ "proper_map X Y (\<lambda>x. c) \<longleftrightarrow> compact_space X \<and> (X = trivial_topology \<or> 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 \<in> topspace X. c = y}" if "compact_space X" for y
--- 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 \<longleftrightarrow> topspace X = {}"
- by (auto simp: continuous_map_def retract_of_space_def)
+ "{} retract_of_space X \<longleftrightarrow> X = trivial_topology"
+ by (auto simp: retract_of_space_def)
lemma retract_of_space_singleton [simp]:
"{a} retract_of_space X \<longleftrightarrow> a \<in> 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 = {} \<Longrightarrow> topspace X = {}"
+ assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> 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 \<union> T = topspace X" and "S = {} \<Longrightarrow> topspace X = {}"
+ assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \<union> T = topspace X" and "S = {} \<Longrightarrow> X = trivial_topology"
shows "S retract_of_space X"
proof (rule retract_of_space_clopen)
have "S \<inter> T = {}"
@@ -1230,10 +1230,9 @@
"pathin (subtopology X S) g \<longleftrightarrow> pathin X g \<and> (\<forall>x \<in> {0..1}. g x \<in> S)"
by (auto simp: pathin_def continuous_map_in_subtopology)
-lemma pathin_const:
- "pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
- by (simp add: pathin_def)
-
+lemma pathin_const [simp]: "pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
+ using pathin_subtopology by (fastforce simp add: pathin_def)
+
lemma path_start_in_topspace: "pathin X g \<Longrightarrow> g 0 \<in> 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 = {} \<Longrightarrow> 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 = {} \<longleftrightarrow> topspace X = {}"
+ "connected_components_of X = {} \<longleftrightarrow> X = trivial_topology"
by (simp add: connected_components_of_def)
lemma connected_components_of_empty_space:
- "topspace X = {} \<Longrightarrow> 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 \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
-proof (cases "topspace X = {}")
+ "connected_components_of X \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (X = trivial_topology \<or> 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 "\<lbrakk>connected_components_of X \<subseteq> {S}\<rbrakk> \<Longrightarrow> 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}
-\<longleftrightarrow> connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
- by (metis ccpo_Sup_singleton connected_components_of_subset_sing insert_not_empty subset_singleton_iff)
+ "connected_components_of X = {S} \<longleftrightarrow> connected_space X \<and> X \<noteq> trivial_topology \<and> 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 \<Longrightarrow> connected_components_of X = (if topspace X = {} then {} else {topspace X})"
+ "connected_space X \<Longrightarrow> 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 \<noteq> {}"
+ assumes "connectedin X S" and ne: "X \<noteq> trivial_topology"
shows "\<exists>C. C \<in> connected_components_of X \<and> S \<subseteq> 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
--- 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 \<longleftrightarrow> (\<exists>i \<in> 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 \<in> extensional I. \<forall>i \<in> I. x i \<in> 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) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
proof -
let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
@@ -1132,19 +1136,20 @@
lemma retraction_map_product_projection:
assumes "i \<in> I"
shows "(retraction_map (product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
- (topspace (product_topology X I) = {}) \<longrightarrow> topspace (X i) = {})"
+ ((product_topology X I) = trivial_topology) \<longrightarrow> (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 *: "\<exists>g. continuous_map (X i) (product_topology X I) g \<and> (\<forall>x\<in>topspace (X i). g x i = x)"
@@ -1156,9 +1161,8 @@
using \<open>i \<in> I\<close> that
by (rule_tac x="\<lambda>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 \<open>i \<in> I\<close> False
- by (auto simp: retraction_map_def retraction_maps_def assms continuous_map_product_projection *)
+ with \<open>i \<in> I\<close> 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) \<longleftrightarrow>
PiE I S = {} \<or>
- finite {i \<in> I. ~(S i = topspace(X i))} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
+ finite {i \<in> I. S i \<noteq> topspace (X i)} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
(is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
proof (cases "PiE I S = {}")
case False
@@ -1216,12 +1220,12 @@
proposition compact_space_product_topology:
"compact_space(product_topology X I) \<longleftrightarrow>
- topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. compact_space(X i))"
+ (product_topology X I) = trivial_topology \<or> (\<forall>i \<in> 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 \<in> (\<Pi>\<^sub>E i\<in>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) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> 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 \<in> (product_topology X I) closure_of S
@@ -1324,7 +1328,7 @@
proposition connected_space_product_topology:
"connected_space(product_topology X I) \<longleftrightarrow>
- (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
+ (\<exists>i \<in> I. X i = trivial_topology) \<or> (\<forall>i \<in> I. connected_space(X i))"
(is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
proof (cases ?eq)
case False
@@ -1339,7 +1343,7 @@
by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
show ?thesis
using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
- 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) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> 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) \<longleftrightarrow>
@@ -1509,7 +1514,7 @@
by (simp add: \<open>i \<in> I\<close> 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 \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
+ by (metis \<open>i \<in> I\<close> 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) \<longleftrightarrow>
PiE I S = {} \<or> (\<forall>i \<in> 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 \<open>Projections from a function topology to a component\<close>
lemma quotient_map_product_projection:
assumes "i \<in> I"
shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
- (topspace(product_topology X I) = {} \<longrightarrow> 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 \<longrightarrow> (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 \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
shows "product_topology X I homeomorphic_space (X i)"
proof -
have "quotient_map (product_topology X I) (X i) (\<lambda>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 (\<lambda>x. x i) (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
using assms by (auto simp: inj_on_def PiE_iff) (metis extensionalityI singletonD)
@@ -1566,15 +1573,15 @@
\<Longrightarrow> P(subtopology (product_topology X I) (PiE I (\<lambda>j. if j = i then topspace(X i) else {z j})))"
(is "\<And>z i. \<lbrakk>_; _; _\<rbrakk> \<Longrightarrow> P (?SX z i)")
and PQ: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
- shows "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. Q(X i))"
+ shows "(\<exists>i\<in>I. (X i) = trivial_topology) \<or> (\<forall>i \<in> I. Q(X i))"
proof -
- have "Q(X i)" if "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<noteq> {}" "i \<in> I" for i
+ have "Q(X i)" if "\<forall>i\<in>I. (X i) \<noteq> trivial_topology" "i \<in> I" for i
proof -
from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>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 \<open>i \<in> I\<close>, of "\<lambda>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 \<open>i \<in> I\<close>] PQ by auto
qed
--- 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 "(\<forall>c\<in>components (- S). \<not> bounded c)"
@@ -3767,8 +3770,9 @@
have "S = {} \<or> 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 (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. 1) (\<lambda>x. c)"
- by (simp add: homotopic_constant_maps)
+ with subtopology_empty_iff_trivial
+ have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. 1) (\<lambda>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 "\<Union>\<F> = {}")
case True
with that show ?thesis
- by force
+ using homotopic_with_canon_on_empty by fastforce
next
case False
then obtain C where "C \<in> \<F>" "C \<noteq> {}"
@@ -5503,7 +5507,7 @@
using T \<open>a \<in> T\<close> 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
--- 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 = {} \<Longrightarrow> (homotopic_with P X X' f g \<longleftrightarrow> P f \<and> P g)"
+ "(homotopic_with P trivial_topology X f g \<longleftrightarrow> P f \<and> P g)"
using homotopic_on_emptyI homotopic_with_imp_property by metis
-lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\<lambda>x. True) {} t f g"
+lemma homotopic_with_canon_on_empty: "homotopic_with_canon (\<lambda>x. True) {} t f g"
by (auto intro: homotopic_with_equal)
lemma homotopic_constant_maps:
"homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow>
- topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
-proof (cases "topspace X = {}")
+ X = trivial_topology \<or> path_component_of X' a b" (is "?lhs = ?rhs")
+proof (cases "X = trivial_topology")
case False
then obtain c where c: "c \<in> topspace X"
- by blast
+ by fastforce
have "\<exists>g. continuous_map (top_of_set {0..1::real}) X' g \<and> g 0 = a \<and> g 1 = b"
if "x \<in> topspace X" and hom: "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b)" for x
proof -
@@ -310,7 +310,7 @@
and h: "\<And>x. h (0, x) = a" "\<And>x. h (1, x) = b"
using hom by (auto simp: homotopic_with_def)
have cont: "continuous_map (top_of_set {0..1}) X' (h \<circ> (\<lambda>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 (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>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 "\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f \<in> S \<rightarrow> T" for f
@@ -1274,7 +1276,7 @@
obtain a where a: "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
using assms by (force simp: contractible_def)
then have "a \<in> 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 "\<forall>p. path p \<and>
path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<longrightarrow>
homotopic_loops S p (linepath a a)"
@@ -1344,11 +1346,12 @@
next
case False
with c1 c2 have "c1 \<in> U" "c2 \<in> U"
- using homotopic_with_imp_continuous_maps by fastforce+
+ using homotopic_with_imp_continuous_maps
+ by (metis PiE equals0I homotopic_with_imp_funspace2)+
with \<open>path_connected U\<close> show ?thesis by blast
qed
then have "homotopic_with_canon (\<lambda>h. True) S U (\<lambda>x. c2) (\<lambda>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) \<longleftrightarrow> contractible S"
by (auto simp: contractible_space_def contractible_def)
-lemma contractible_space_empty:
- "topspace X = {} \<Longrightarrow> 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="\<lambda>(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} \<Longrightarrow> 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="\<lambda>(t,x). if t = 0 then x else a" in exI)
@@ -3493,17 +3496,17 @@
lemma contractible_space_subset_singleton:
"topspace X \<subseteq> {a} \<Longrightarrow> 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 \<longleftrightarrow>
- topspace X = {} \<or>
+ X = trivial_topology \<or>
(\<exists>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>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 \<in> 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 (\<lambda>x. True) X X (\<lambda>x. a) (\<lambda>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 @@
\<Longrightarrow> homotopic_with (\<lambda>h. True) X Z (g \<circ> f) (g' \<circ> 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 \<and> continuous_map X Y g \<and>
@@ -3640,8 +3643,8 @@
lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
"contractible_space X \<longleftrightarrow>
- topspace X = {} \<or> (\<exists>a \<in> topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")
-proof (cases "topspace X = {}")
+ X = trivial_topology \<or> (\<exists>a \<in> 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) \<longleftrightarrow>
- topspace X = {} \<or> topspace Y = {} \<or> contractible_space X \<and> contractible_space Y"
-proof (cases "topspace X = {} \<or> topspace Y = {}")
+ X = trivial_topology \<or> Y = trivial_topology \<or> contractible_space X \<and> contractible_space Y"
+proof (cases "X = trivial_topology \<or> 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) \<longleftrightarrow>
- topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
-proof (cases "topspace (product_topology X I) = {}")
+ (product_topology X I) = trivial_topology \<or> (\<forall>i \<in> 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 \<in> 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 \<in> S" "b \<in> 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} \<longleftrightarrow> S \<noteq> {} \<and> 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"
--- 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 = {} \<Longrightarrow> 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 \<U>: "countable \<U>" and lin: "\<And>U. U \<in> \<U> \<Longrightarrow> Lindelof_space (subtopology X U)"
@@ -200,7 +200,7 @@
have UU_eq: "\<Union>\<U> = topspace X"
by (meson UU fin locally_finite_in_def subset_antisym)
obtain T where T: "\<And>x. x \<in> topspace X \<Longrightarrow> openin X (T x) \<and> x \<in> T x \<and> finite {U \<in> \<U>. U \<inter> T x \<noteq> {}}"
- 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 \<subseteq> topspace X" and I: "topspace X \<subseteq> \<Union>(T ` I)"
using X unfolding Lindelof_space_alt
by (drule_tac x="image T (topspace X)" in spec) (auto simp: ex_countable_subset_image)
--- 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) \<longleftrightarrow>
- topspace(product_topology X I) = {} \<or>
+ (product_topology X I) = trivial_topology \<or>
finite {i. i \<in> I \<and> ~path_connected_space(X i)} \<and>
(\<forall>i \<in> I. locally_path_connected_space(X i))"
(is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
@@ -350,7 +350,7 @@
next
case False
then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>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) \<longleftrightarrow>
- topspace (prod_topology X Y) = {} \<or>
+ (prod_topology X Y) = trivial_topology \<or>
locally_path_connected_space X \<and> 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 \<noteq> {}" "topspace Y \<noteq> {}"
+ then have ne: "X \<noteq> trivial_topology" "Y \<noteq> 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) \<longleftrightarrow>
- topspace (prod_topology X Y) = {} \<or>
+ (prod_topology X Y) = trivial_topology \<or>
locally_connected_space X \<and> 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 \<noteq> {}" "topspace Y \<noteq> {}"
+ then have ne: "X \<noteq> trivial_topology" "Y \<noteq> 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) \<longleftrightarrow>
- topspace(product_topology X I) = {} \<or>
+ (product_topology X I) = trivial_topology \<or>
finite {i. i \<in> I \<and> ~connected_space(X i)} \<and>
(\<forall>i \<in> I. locally_connected_space(X i))"
(is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
@@ -843,7 +843,7 @@
next
case False
then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>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 \<longleftrightarrow> topspace X = {}"
+inductive_simps dim_le_minus2 [simp]: "X dim_le -2"
+
+lemma dimension_le_eq_empty [simp]:
+ "X dim_le -1 \<longleftrightarrow> 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 \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. closedin X U \<and> 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
--- 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 = {} \<longleftrightarrow> topspace X = {}"
- using Union_path_components_of nonempty_path_components_of by fastforce
+ "path_components_of X = {} \<longleftrightarrow> 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 = {} \<Longrightarrow> 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)) \<subseteq> 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)) \<subseteq> 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:
--- 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 \<longleftrightarrow> X = trivial_topology \<or> 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 \<times> T) = prod_topology (subtopology X S) (subtopology Y T)"
proof -
@@ -142,11 +146,11 @@
text \<open>Missing the opposite direction. Does it hold? A converse is proved for proper maps, a stronger condition\<close>
lemma closed_map_prod:
assumes "closed_map (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y))"
- shows "topspace(prod_topology X Y) = {} \<or> closed_map X X' f \<and> closed_map Y Y' g"
-proof (cases "topspace(prod_topology X Y) = {}")
+ shows "(prod_topology X Y) = trivial_topology \<or> closed_map X X' f \<and> closed_map Y Y' g"
+proof (cases "(prod_topology X Y) = trivial_topology")
case False
then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
- 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 @@
\<Longrightarrow> continuous_map X Y (\<lambda>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 \<longleftrightarrow> (topspace Y = {} \<longrightarrow> topspace X = {})"
- by (auto simp: continuous_open_quotient_map open_map_fst continuous_map_fst)
+ "quotient_map(prod_topology X Y) X fst \<longleftrightarrow> (Y = trivial_topology \<longrightarrow> 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 \<longleftrightarrow> (topspace X = {} \<longrightarrow> topspace Y = {})"
- by (auto simp: continuous_open_quotient_map open_map_snd continuous_map_snd)
+ "quotient_map(prod_topology X Y) Y snd \<longleftrightarrow> (X = trivial_topology \<longrightarrow> 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 \<longleftrightarrow> (topspace Y = {} \<longrightarrow> topspace X = {})"
-proof (cases "topspace Y = {}")
+ "retraction_map (prod_topology X Y) X fst \<longleftrightarrow> (Y = trivial_topology \<longrightarrow> 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 "\<exists>g. continuous_map X (prod_topology X Y) g \<and> (\<forall>x\<in>topspace X. fst (g x) = x)"
@@ -304,12 +316,12 @@
qed
lemma retraction_map_snd:
- "retraction_map (prod_topology X Y) Y snd \<longleftrightarrow> (topspace X = {} \<longrightarrow> topspace Y = {})"
-proof (cases "topspace X = {}")
+ "retraction_map (prod_topology X Y) Y snd \<longleftrightarrow> (X = trivial_topology \<longrightarrow> 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 "\<exists>g. continuous_map Y (prod_topology X Y) g \<and> (\<forall>y\<in>topspace Y. snd (g y) = y)"
@@ -323,8 +335,8 @@
lemma continuous_map_of_fst:
- "continuous_map (prod_topology X Y) Z (f \<circ> fst) \<longleftrightarrow> topspace Y = {} \<or> continuous_map X Z f"
-proof (cases "topspace Y = {}")
+ "continuous_map (prod_topology X Y) Z (f \<circ> fst) \<longleftrightarrow> Y = trivial_topology \<or> 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 \<circ> snd) \<longleftrightarrow> topspace X = {} \<or> continuous_map Y Z f"
-proof (cases "topspace X = {}")
+ "continuous_map (prod_topology X Y) Z (f \<circ> snd) \<longleftrightarrow> X = trivial_topology \<or> 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') (\<lambda>(x,y). (f x, g y)) \<longleftrightarrow>
- topspace (prod_topology X Y) = {} \<or> continuous_map X X' f \<and> 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 \<or> continuous_map X X' f \<and> 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 \<in> (prod_topology X Y) closure_of S"
@@ -368,11 +377,11 @@
proposition compact_space_prod_topology:
- "compact_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> compact_space X \<and> compact_space Y"
-proof (cases "topspace(prod_topology X Y) = {}")
+ "compact_space(prod_topology X Y) \<longleftrightarrow> (prod_topology X Y) = trivial_topology \<or> compact_space X \<and> 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 \<noteq> {}" "topspace Y \<noteq> {}"
@@ -385,7 +394,7 @@
have "compactin Y (snd ` (topspace X \<times> 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 \<X> where "\<X> \<equiv> (\<lambda>V. topspace X \<times> V) ` Collect (openin Y)"
@@ -483,28 +492,26 @@
lemma compactin_Times:
"compactin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> compactin X S \<and> 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\<open>Homeomorphic maps\<close>
lemma homeomorphic_maps_prod:
"homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow>
- topspace(prod_topology X Y) = {} \<and> topspace(prod_topology X' Y') = {}
+ (prod_topology X Y) = trivial_topology \<and> (prod_topology X' Y') = trivial_topology
\<or> homeomorphic_maps X X' f f' \<and> homeomorphic_maps Y Y' g g'" (is "?lhs = ?rhs")
proof
show "?lhs \<Longrightarrow> ?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 \<Longrightarrow> ?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)
- (\<lambda>(x,y). (y,x)) (\<lambda>(y,x). (x,y))"
+ "homeomorphic_maps (prod_topology X Y) (prod_topology Y X) (\<lambda>(x,y). (y,x)) (\<lambda>(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} \<Longrightarrow> prod_topology X Y homeomorphic_space X"
+ "Y = discrete_topology {b} \<Longrightarrow> 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} \<Longrightarrow> prod_topology X Y homeomorphic_space Y"
+ "X = discrete_topology {a} \<Longrightarrow> 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 \<in> topspace Y \<Longrightarrow> 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 \<in> topspace X \<Longrightarrow> 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: "\<And>y. \<lbrakk>y \<in> topspace Y; P(prod_topology X Y)\<rbrakk> \<Longrightarrow> P(subtopology (prod_topology X Y) (topspace X \<times> {y}))"
and PQ: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
and PR: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> R X')"
- shows "topspace(prod_topology X Y) = {} \<or> Q X \<and> R Y"
+ shows "(prod_topology X Y) = trivial_topology \<or> Q X \<and> R Y"
proof -
have "Q X \<and> R Y" if "topspace(prod_topology X Y) \<noteq> {}"
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) \<longleftrightarrow>
- topspace(prod_topology X Y) = {} \<or> connected_space X \<and> connected_space Y" (is "?lhs=?rhs")
-proof (cases "topspace(prod_topology X Y) = {}")
+ (prod_topology X Y) = trivial_topology \<or> connected_space X \<and> 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 \<noteq> {}" "topspace Y \<noteq> {}"
@@ -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 \<times> T) \<longleftrightarrow>
S = {} \<or> T = {} \<or> connectedin X S \<and> 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
--- 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"
--- 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 \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. closedin X U \<and> x \<in> U \<and> y \<notin> U))"
by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)
-lemma t1_space_empty: "topspace X = {} \<Longrightarrow> 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)
-\<longleftrightarrow> topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t1_space (X i))"
-proof (cases "topspace(product_topology X I) = {}")
+\<longleftrightarrow> (product_topology X I) = trivial_topology \<or> (\<forall>i \<in> 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 \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
- by fastforce
+ using discrete_topology_unique by (fastforce iff: null_topspace_iff_trivial)
have "t1_space (product_topology X I) \<longleftrightarrow> (\<forall>i\<in>I. t1_space (X i))"
proof (intro iffI ballI)
show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \<in> I" for i
@@ -210,17 +210,19 @@
qed
lemma t1_space_prod_topology:
- "t1_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> t1_space X \<and> t1_space Y"
-proof (cases "topspace (prod_topology X Y) = {}")
+ "t1_space(prod_topology X Y) \<longleftrightarrow> (prod_topology X Y) = trivial_topology \<or> t1_space X \<and> 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} \<times> {y}" for x y
+ have eq: "{(x,y)} = {x} \<times> {y}" for x::'a and y::'b
by simp
have "t1_space (prod_topology X Y) \<longleftrightarrow> (t1_space X \<and> 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 @@
"\<lbrakk>Hausdorff_space X; topspace X = topspace Y; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> Hausdorff_space Y"
by (metis Hausdorff_space_def)
-lemma Hausdorff_space_topspace_empty:
- "topspace X = {} \<Longrightarrow> 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) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> Hausdorff_space X \<and> Hausdorff_space Y"
+ "Hausdorff_space(prod_topology X Y) \<longleftrightarrow> (prod_topology X Y) = trivial_topology \<or> Hausdorff_space X \<and> Hausdorff_space Y"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -655,7 +656,7 @@
then show "x = x' \<and> 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 "(\<Pi>\<^sub>E i\<in>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 "\<exists>U V. openin (product_topology X I) U \<and> openin (product_topology X I) V \<and> f \<in> U \<and> g \<in> V \<and> disjnt U V"
--- 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) \<longleftrightarrow>
- topspace (prod_topology X Y) = {} \<or>
+ (prod_topology X Y) = trivial_topology \<or>
completely_regular_space X \<and> 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) \<longleftrightarrow>
- (\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. completely_regular_space (X i))"
+ (\<exists>i\<in>I. X i = trivial_topology) \<or> (\<forall>i \<in> I. completely_regular_space (X i))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs then show ?rhs
@@ -1215,7 +1215,7 @@
next
assume R: ?rhs
show ?lhs
- proof (cases "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {}")
+ proof (cases "\<exists>i\<in>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 \<inter> 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 \<le> B" and B: "\<And>x. x \<in> topspace X \<Longrightarrow> mdist m (f x) (g x) \<le> B"
shows "mdist (cfunspace X m) f g \<le> B"
-proof (cases "topspace X = {}")
+proof (cases "X = trivial_topology")
case True
then show ?thesis
by (simp add: Metric_space.fdist_empty \<open>B\<ge>0\<close> 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 (\<sigma> N x0) (g x0) \<le> \<epsilon>/3" if "x0 \<in> topspace X" for x0
proof -
- have "bdd_above ((\<lambda>x. d (\<sigma> N x) (g x)) ` topspace X)"
- by (metis F.limit_metric_sequentially False N bdd_above_dist g order_refl)
+ have "g \<in> fspace (topspace X)"
+ using F.limit_metric_sequentially g by blast
+ with N that have "bdd_above ((\<lambda>x. d (\<sigma> N x) (g x)) ` topspace X)"
+ by (force intro: bdd_above_dist)
then have "d (\<sigma> N x0) (g x0) \<le> Sup ((\<lambda>x. d (\<sigma> N x) (g x)) ` topspace X)"
by (simp add: cSup_upper that)
also have "\<dots> \<le> \<epsilon>/3"
- by (smt (verit) F.limit_metric_sequentially False N Sup.SUP_cong fdist_def g order_refl)
+ using g False N \<open>g \<in> fspace (topspace X)\<close>
+ by (fastforce simp: F.limit_metric_sequentially fdist_def)
finally show ?thesis .
qed
have "d (g x) (g y) \<le> d (g x) (\<sigma> N x) + d (\<sigma> N x) (g y)"
@@ -4880,11 +4883,11 @@
by (metis top closedin_topspace)
have "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space mtopology"
by (simp add: True product_topology_empty_discrete)
- also have "\<dots> 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 "\<dots> homeomorphic_space (prod_topology mtopology (discrete_topology {\<lambda>x. undefined}))"
+ by (meson homeomorphic_space_sym prod_topology_homeomorphic_space_left)
finally
show "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space subtopology (prod_topology mtopology (powertop_real I)) (M \<times> {(\<lambda>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\<le>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 \<noteq> {}" "n=1"
+ by (fastforce simp add: connected_components_of_def)+
+ then have "{} \<notin> {topspace X}"
+ by blast
+ with \<open>n=1\<close> show ?thesis
+ by (simp add: eqpoll_iff_finite_card card_Suc_eq flip: ex_simps)
next
case False
then have "n-1 \<noteq> 0"
--- 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 \<cong> integer_group"
proof -
obtain a where a: "a \<in> topspace X"
- using assms by auto
+ using assms by blast
have "singular_simplex 0 X (restrict (\<lambda>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
--- 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) \<inter> equator n \<noteq> {}"
- 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
= \<one>\<^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 \<in> S"
--- 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 \<longleftrightarrow> singular_chain p X c \<and> 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:
"\<lbrakk>singular_relcycle p (subtopology X T) {} c; T \<subseteq> S\<rbrakk>
@@ -428,11 +428,11 @@
lemma singular_boundary:
"singular_relboundary p X {} c \<longleftrightarrow>
(\<exists>d. singular_chain (Suc p) X d \<and> 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 \<Longrightarrow> 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:
"\<lbrakk>T \<subseteq> S; singular_relboundary p (subtopology X T) {} c\<rbrakk>