--- 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