--- a/src/HOL/Analysis/Abstract_Topology.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1410,7 +1410,10 @@
by (simp add: Sup_le_iff closure_of_minimal)
-subsection\<open>Continuous maps\<close>
+subsection%important \<open>Continuous maps\<close>
+
+text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
+of type classes, as defined below.\<close>
definition continuous_map where
"continuous_map X Y f \<equiv>
@@ -1717,6 +1720,22 @@
declare continuous_map_id_subt [unfolded id_def, simp]
+lemma%important continuous_map_alt:
+ "continuous_map T1 T2 f
+ = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
+ by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
+
+lemma continuous_map_open [intro]:
+ "continuous_map T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
+ unfolding continuous_map_alt by auto
+
+lemma continuous_map_preimage_topspace [intro]:
+ assumes "continuous_map T1 T2 f"
+ shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
+using assms unfolding continuous_map_def by auto
+
+
+
subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
@@ -1852,7 +1871,7 @@
apply clarify
apply (rename_tac T)
apply (rule_tac x="f ` T" in image_eqI)
- using openin_closedin_eq by force+
+ using openin_closedin_eq by fastforce+
lemma closed_map_restriction:
"\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
@@ -1861,7 +1880,7 @@
apply clarify
apply (rename_tac T)
apply (rule_tac x="f ` T" in image_eqI)
- using closedin_def by force+
+ using closedin_def by fastforce+
subsection\<open>Quotient maps\<close>
@@ -4177,35 +4196,10 @@
qed
qed
-subsubsection%important \<open>Continuity\<close>
-
-text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
-of type classes, as defined below.\<close>
-
-definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
- \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
-
-lemma continuous_on_continuous_on_topo:
- "continuous_on s f \<longleftrightarrow> continuous_on_topo (top_of_set s) euclidean f"
- by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq)
-
-lemma continuous_on_topo_UNIV:
- "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
-using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
-
-lemma continuous_on_topo_open [intro]:
- "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
- unfolding continuous_on_topo_def by auto
-
-lemma continuous_on_topo_topspace [intro]:
- "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
-unfolding continuous_on_topo_def by auto
-
lemma continuous_on_generated_topo_iff:
- "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
+ "continuous_map T1 (topology_generated_by S) f \<longleftrightarrow>
((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
-unfolding continuous_on_topo_def topology_generated_by_topspace
+unfolding continuous_map_alt topology_generated_by_topspace
proof (auto simp add: topology_generated_by_Basis)
assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
fix U assume "openin (topology_generated_by S) U"
@@ -4231,31 +4225,11 @@
lemma continuous_on_generated_topo:
assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
"f`(topspace T1) \<subseteq> (\<Union> S)"
- shows "continuous_on_topo T1 (topology_generated_by S) f"
+ shows "continuous_map T1 (topology_generated_by S) f"
using assms continuous_on_generated_topo_iff by blast
-proposition continuous_on_topo_compose:
- assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
- shows "continuous_on_topo T1 T3 (g o f)"
- using assms unfolding continuous_on_topo_def
-proof (auto)
- fix U :: "'c set"
- assume H: "openin T3 U"
- have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
- using H assms by blast
- moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
- using H assms continuous_on_topo_topspace by fastforce
- ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
- by simp
-qed (blast)
-
-lemma continuous_on_topo_preimage_topspace [intro]:
- assumes "continuous_on_topo T1 T2 f"
- shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
-using assms unfolding continuous_on_topo_def by auto
-
-
-subsubsection%important \<open>Pullback topology\<close>
+
+subsection%important \<open>Pullback topology\<close>
text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
a special case of this notion, pulling back by the identity. We introduce the general notion as
@@ -4289,14 +4263,14 @@
"topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
by (auto simp add: topspace_def openin_pullback_topology)
-proposition continuous_on_topo_pullback [intro]:
- assumes "continuous_on_topo T1 T2 g"
- shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
-unfolding continuous_on_topo_def
+proposition continuous_map_pullback [intro]:
+ assumes "continuous_map T1 T2 g"
+ shows "continuous_map (pullback_topology A f T1) T2 (g o f)"
+unfolding continuous_map_alt
proof (auto)
fix U::"'b set" assume "openin T2 U"
then have "openin T1 (g-`U \<inter> topspace T1)"
- using assms unfolding continuous_on_topo_def by auto
+ using assms unfolding continuous_map_alt by auto
have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
unfolding topspace_pullback_topology by auto
also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
@@ -4310,13 +4284,13 @@
then have "f x \<in> topspace T1"
unfolding topspace_pullback_topology by auto
then show "g (f x) \<in> topspace T2"
- using assms unfolding continuous_on_topo_def by auto
+ using assms unfolding continuous_map_def by auto
qed
-proposition continuous_on_topo_pullback' [intro]:
- assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
- shows "continuous_on_topo T1 (pullback_topology A f T2) g"
-unfolding continuous_on_topo_def
+proposition continuous_map_pullback' [intro]:
+ assumes "continuous_map T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
+ shows "continuous_map T1 (pullback_topology A f T2) g"
+unfolding continuous_map_alt
proof (auto)
fix U assume "openin (pullback_topology A f T2) U"
then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
@@ -4335,7 +4309,7 @@
next
fix x assume "x \<in> topspace T1"
have "(f o g) x \<in> topspace T2"
- using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
+ using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
then have "g x \<in> f-`(topspace T2)"
unfolding comp_def by blast
moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
--- a/src/HOL/Analysis/Abstract_Topology_2.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1231,6 +1231,15 @@
lemma pathin_const:
"pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
by (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)
+
+lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X"
+ by (force simp: pathin_def continuous_map)
+
+lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X"
+ by (force simp: pathin_def continuous_map)
definition path_connected_space :: "'a topology \<Rightarrow> bool"
where "path_connected_space X \<equiv> \<forall>x \<in> topspace X. \<forall> y \<in> topspace X. \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
@@ -1323,6 +1332,19 @@
qed
qed
+lemma path_connectedin_discrete_topology:
+ "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
+ apply safe
+ using path_connectedin_subset_topspace apply fastforce
+ apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
+ using subset_singletonD by fastforce
+
+lemma path_connected_space_discrete_topology:
+ "path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
+ by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
+ subset_singletonD topspace_discrete_topology)
+
+
lemma homeomorphic_path_connected_space_imp:
"\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
unfolding homeomorphic_space_def homeomorphic_maps_def
--- a/src/HOL/Analysis/Binary_Product_Measure.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Thu Mar 21 14:18:37 2019 +0000
@@ -74,11 +74,11 @@
qed
lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^sub>M M2) M1"
- by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+ by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space Times_Int_Times
measurable_def)
lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^sub>M M2) M2"
- by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+ by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space Times_Int_Times
measurable_def)
lemma measurable_Pair_compose_split[measurable_dest]:
@@ -215,7 +215,7 @@
lemma Int_stable_pair_measure_generator: "Int_stable {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
unfolding Int_stable_def
- by safe (auto simp add: times_Int_times)
+ by safe (auto simp add: Times_Int_Times)
lemma (in finite_measure) finite_measure_cut_measurable:
assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^sub>M M)"
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Mar 21 14:18:37 2019 +0000
@@ -779,41 +779,41 @@
qed
lemma strong_operator_topology_continuous_evaluation:
- "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
+ "continuous_map strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
proof -
- have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
- unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
- using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
+ have "continuous_map strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
+ unfolding strong_operator_topology_def apply (rule continuous_map_pullback)
+ using continuous_on_product_coordinates by fastforce
then show ?thesis unfolding comp_def by simp
qed
lemma continuous_on_strong_operator_topo_iff_coordinatewise:
- "continuous_on_topo T strong_operator_topology f
- \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
+ "continuous_map T strong_operator_topology f
+ \<longleftrightarrow> (\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x))"
proof (auto)
fix x::"'b"
- assume "continuous_on_topo T strong_operator_topology f"
- with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
- have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
+ assume "continuous_map T strong_operator_topology f"
+ with continuous_map_compose[OF this strong_operator_topology_continuous_evaluation]
+ have "continuous_map T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
by simp
- then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+ then show "continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
unfolding comp_def by auto
next
- assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
- have "continuous_on_topo T euclidean (blinfun_apply o f)"
+ assume *: "\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+ have "continuous_map T euclidean (blinfun_apply o f)"
unfolding euclidean_product_topology
- apply (rule continuous_on_topo_coordinatewise_then_product, auto)
+ apply (rule continuous_map_coordinatewise_then_product, auto)
using * unfolding comp_def by auto
- show "continuous_on_topo T strong_operator_topology f"
+ show "continuous_map T strong_operator_topology f"
unfolding strong_operator_topology_def
- apply (rule continuous_on_topo_pullback')
- by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
+ apply (rule continuous_map_pullback')
+ by (auto simp add: \<open>continuous_map T euclidean (blinfun_apply o f)\<close>)
qed
lemma strong_operator_topology_weaker_than_euclidean:
- "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
+ "continuous_map euclidean strong_operator_topology (\<lambda>f. f)"
by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
- auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
+ auto simp add: linear_continuous_on)
--- a/src/HOL/Analysis/Function_Topology.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Thu Mar 21 14:18:37 2019 +0000
@@ -3,11 +3,11 @@
*)
theory Function_Topology
-imports Topology_Euclidean_Space
+imports Topology_Euclidean_Space
begin
-section \<open>Function Topology\<close>
+section \<open>Function Topology\<close>
text \<open>We want to define the general product topology.
@@ -42,17 +42,17 @@
Here is an example of a reformulation using topologies. Let
@{text [display]
-\<open>continuous_on_topo T1 T2 f =
+\<open>continuous_map T1 T2 f =
((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
\<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
the current \<open>continuous_on\<close> (with type classes) can be redefined as
@{text [display] \<open>continuous_on s f =
- continuous_on_topo (top_of_set s) (topology euclidean) f\<close>}
+ continuous_map (top_of_set s) (topology euclidean) f\<close>}
-In fact, I need \<open>continuous_on_topo\<close> to express the continuity of the projection on subfactors
+In fact, I need \<open>continuous_map\<close> to express the continuity of the projection on subfactors
for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
-the above equivalence in Lemma~\<open>continuous_on_continuous_on_topo\<close>.
+the above equivalence in Lemma~\<open>continuous_map_iff_continuous\<close>.
I only develop the basics of the product topology in this theory. The most important missing piece
is Tychonov theorem, stating that a product of compact spaces is always compact for the product
@@ -252,7 +252,7 @@
((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
relative_to topspace (product_topology X I))"
apply (subst product_topology)
- apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
+ apply (simp add: topology_inverse' [OF istopology_subbase])
done
lemma subtopology_PiE:
@@ -286,10 +286,9 @@
done
qed
-
lemma product_topology_base_alt:
"finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
- relative_to topspace(product_topology X I) =
+ relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i)) =
(\<lambda>F. (\<exists>U. F = Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
(is "?lhs = ?rhs")
proof -
@@ -340,6 +339,15 @@
by meson
qed
+corollary openin_product_topology_alt:
+ "openin (product_topology X I) S \<longleftrightarrow>
+ (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
+ (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+ unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
+ apply safe
+ apply (drule bspec; blast)+
+ done
+
lemma closure_of_product_topology:
"(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
proof -
@@ -445,9 +453,9 @@
subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
-lemma continuous_on_topo_product_coordinates [simp]:
+lemma continuous_map_product_coordinates [simp]:
assumes "i \<in> I"
- shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
+ shows "continuous_map (product_topology T I) (T i) (\<lambda>x. x i)"
proof -
{
fix U assume "openin (T i) U"
@@ -463,14 +471,14 @@
apply (subst *)
using ** by auto
}
- then show ?thesis unfolding continuous_on_topo_def
- by (auto simp add: assms topspace_product_topology PiE_iff)
+ then show ?thesis unfolding continuous_map_alt
+ by (auto simp add: assms PiE_iff)
qed
-lemma continuous_on_topo_coordinatewise_then_product [intro]:
- assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+lemma continuous_map_coordinatewise_then_product [intro]:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
"\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
- shows "continuous_on_topo T1 (product_topology T I) f"
+ shows "continuous_map T1 (product_topology T I) f"
unfolding product_topology_def
proof (rule continuous_on_generated_topo)
fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
@@ -479,7 +487,7 @@
define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
- using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
+ using that assms(1) by (simp add: continuous_map_preimage_topspace)
then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
using that unfolding J_def by auto
have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
@@ -497,25 +505,25 @@
apply (subst product_topology_def[symmetric])
apply (simp only: topspace_product_topology)
apply (auto simp add: PiE_iff)
- using assms unfolding continuous_on_topo_def by auto
+ using assms unfolding continuous_map_def by auto
qed
-lemma continuous_on_topo_product_then_coordinatewise [intro]:
- assumes "continuous_on_topo T1 (product_topology T I) f"
- shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+lemma continuous_map_product_then_coordinatewise [intro]:
+ assumes "continuous_map T1 (product_topology T I) f"
+ shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
"\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
proof -
fix i assume "i \<in> I"
have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
- also have "continuous_on_topo T1 (T i) (...)"
- apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
+ also have "continuous_map T1 (T i) (...)"
+ apply (rule continuous_map_compose[of _ "product_topology T I"])
using assms \<open>i \<in> I\<close> by auto
- ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+ ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
by simp
next
fix i x assume "i \<notin> I" "x \<in> topspace T1"
have "f x \<in> topspace (product_topology T I)"
- using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
+ using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
using topspace_product_topology by metis
then show "f x i = undefined"
@@ -524,11 +532,11 @@
lemma continuous_on_restrict:
assumes "J \<subseteq> I"
- shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
-proof (rule continuous_on_topo_coordinatewise_then_product)
+ shows "continuous_map (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
+proof (rule continuous_map_coordinatewise_then_product)
fix i assume "i \<in> J"
then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
- then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
+ then show "continuous_map (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
next
fix i assume "i \<notin> J"
@@ -571,7 +579,7 @@
have **: "finite {i. X i \<noteq> UNIV}"
unfolding X_def V_def J_def using assms(1) by auto
have "open (Pi\<^sub>E UNIV X)"
- unfolding open_fun_def
+ unfolding open_fun_def
by (simp_all add: * ** product_topology_basis)
moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
@@ -594,28 +602,28 @@
lemma continuous_on_product_coordinates [simp]:
"continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
- unfolding continuous_on_topo_UNIV euclidean_product_topology
- by (rule continuous_on_topo_product_coordinates, simp)
+ using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
+ by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
shows "continuous_on S f"
- using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
- by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
+ using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
+ by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
lemma continuous_on_product_then_coordinatewise_UNIV:
assumes "continuous_on UNIV f"
shows "continuous_on UNIV (\<lambda>x. f x i)"
-using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
-by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
+ using assms unfolding continuous_map_iff_continuous2 [symmetric] euclidean_product_topology
+ by fastforce
lemma continuous_on_product_then_coordinatewise:
assumes "continuous_on S f"
shows "continuous_on S (\<lambda>x. f x i)"
proof -
have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
- by (metis assms continuous_on_compose continuous_on_id
+ by (metis assms continuous_on_compose continuous_on_id
continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
then show ?thesis
by auto
@@ -1582,4 +1590,166 @@
qed
qed
+subsection \<open>Open Pi-sets in the product topology\<close>
+
+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))"
+ (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
+proof (cases "PiE I S = {}")
+ case False
+ moreover have "?lhs = ?rhs"
+ proof
+ assume L: ?lhs
+ moreover
+ obtain z where z: "z \<in> PiE I S"
+ using False by blast
+ ultimately obtain U where fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+ and "Pi\<^sub>E I U \<noteq> {}"
+ and sub: "Pi\<^sub>E I U \<subseteq> Pi\<^sub>E I S"
+ by (fastforce simp add: openin_product_topology_alt)
+ then have *: "\<And>i. i \<in> I \<Longrightarrow> U i \<subseteq> S i"
+ by (simp add: subset_PiE)
+ show ?rhs
+ proof (intro conjI ballI)
+ show "finite {i \<in> I. S i \<noteq> topspace (X i)}"
+ apply (rule finite_subset [OF _ fin], clarify)
+ using *
+ by (metis False L openin_subset topspace_product_topology subset_PiE subset_antisym)
+ next
+ fix i :: "'a"
+ assume "i \<in> I"
+ then show "openin (X i) (S i)"
+ using open_map_product_projection [of i I X] L
+ apply (simp add: open_map_def)
+ apply (drule_tac x="PiE I S" in spec)
+ apply (simp add: False image_projection_PiE split: if_split_asm)
+ done
+ qed
+ next
+ assume ?rhs
+ then show ?lhs
+ apply (simp only: openin_product_topology)
+ apply (rule arbitrary_union_of_inc)
+ apply (auto simp: product_topology_base_alt)
+ done
+ qed
+ ultimately show ?thesis
+ by simp
+qed simp
+
+
+corollary openin_PiE:
+ "finite I \<Longrightarrow> openin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. openin (X i) (S i))"
+ by (simp add: openin_PiE_gen)
+
+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))"
+ (is "?lhs = ?rhs")
+proof (cases "topspace(product_topology X I) = {}")
+ case False
+ then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
+ by auto
+ show ?thesis
+ proof
+ assume L: ?lhs
+ show ?rhs
+ proof (clarsimp simp add: False compact_space_def)
+ fix i
+ assume "i \<in> I"
+ with L have "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
+ by (simp add: continuous_map_product_projection)
+ moreover
+ have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ using \<open>i \<in> I\<close> z
+ apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
+ done
+ then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
+ using \<open>i \<in> I\<close> z by auto
+ ultimately show "compactin (X i) (topspace (X i))"
+ by (metis L compact_space_def image_compactin topspace_product_topology)
+ qed
+ next
+ assume R: ?rhs
+ show ?lhs
+ proof (cases "I = {}")
+ case True
+ with R show ?thesis
+ by (simp add: compact_space_def)
+ next
+ case False
+ then obtain i where "i \<in> I"
+ by blast
+ show ?thesis
+ using R
+ proof
+ assume com [rule_format]: "\<forall>i\<in>I. compact_space (X i)"
+ let ?\<C> = "{{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
+ show "compact_space (product_topology X I)"
+ proof (rule Alexander_subbase_alt)
+ show "topspace (product_topology X I) \<subseteq> \<Union>?\<C>"
+ unfolding topspace_product_topology using \<open>i \<in> I\<close> by blast
+ next
+ fix C
+ assume Csub: "C \<subseteq> ?\<C>" and UC: "topspace (product_topology X I) \<subseteq> \<Union>C"
+ define \<D> where "\<D> \<equiv> \<lambda>i. {U. openin (X i) U \<and> {f. f i \<in> U} \<in> C}"
+ show "\<exists>C'. finite C' \<and> C' \<subseteq> C \<and> topspace (product_topology X I) \<subseteq> \<Union>C'"
+ proof (cases "\<exists>i. i \<in> I \<and> topspace (X i) \<subseteq> \<Union>(\<D> i)")
+ case True
+ then obtain i where "i \<in> I"
+ and i: "topspace (X i) \<subseteq> \<Union>(\<D> i)"
+ unfolding \<D>_def by blast
+ then have *: "\<And>\<U>. \<lbrakk>Ball \<U> (openin (X i)); topspace (X i) \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow>
+ \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace (X i) \<subseteq> \<Union>\<F>"
+ using com [OF \<open>i \<in> I\<close>] by (auto simp: compact_space_def compactin_def)
+ have "topspace (X i) \<subseteq> \<Union>(\<D> i)"
+ using i by auto
+ with * obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> (\<D> i) \<and> topspace (X i) \<subseteq> \<Union>\<F>"
+ unfolding \<D>_def by fastforce
+ with \<open>i \<in> I\<close> show ?thesis
+ unfolding \<D>_def
+ by (rule_tac x="(\<lambda>U. {x. x i \<in> U}) ` \<F>" in exI) auto
+ next
+ case False
+ then have "\<forall>i \<in> I. \<exists>y. y \<in> topspace (X i) \<and> y \<notin> \<Union>(\<D> i)"
+ by force
+ then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> g i \<in> topspace (X i) \<and> g i \<notin> \<Union>(\<D> i)"
+ by metis
+ then have "(\<lambda>i. if i \<in> I then g i else undefined) \<in> topspace (product_topology X I)"
+ by (simp add: PiE_I)
+ moreover have "(\<lambda>i. if i \<in> I then g i else undefined) \<notin> \<Union>C"
+ using Csub g unfolding \<D>_def by force
+ ultimately show ?thesis
+ using UC by blast
+ qed
+ qed (simp add: product_topology)
+ qed (simp add: compact_space_topspace_empty)
+ qed
+ qed
+qed (simp add: compact_space_topspace_empty)
+
+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)
+
+lemma in_product_topology_closure_of:
+ "z \<in> (product_topology X I) closure_of S
+ \<Longrightarrow> i \<in> I \<Longrightarrow> z i \<in> ((X i) closure_of ((\<lambda>x. x i) ` S))"
+ using continuous_map_product_projection
+ by (force simp: continuous_map_eq_image_closure_subset image_subset_iff)
+
+lemma homeomorphic_space_singleton_product:
+ "product_topology X {k} homeomorphic_space (X k)"
+ unfolding homeomorphic_space
+ apply (rule_tac x="\<lambda>x. x k" in exI)
+ apply (rule bijective_open_imp_homeomorphic_map)
+ apply (simp_all add: continuous_map_product_projection open_map_product_projection)
+ unfolding PiE_over_singleton_iff
+ apply (auto simp: image_iff inj_on_def)
+ done
+
end
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1,4 +1,4 @@
-subsection \<open>Ordered Euclidean Space\<close> (* why not Section? *)
+section \<open>Ordered Euclidean Space\<close>
theory Ordered_Euclidean_Space
imports
--- a/src/HOL/Analysis/Path_Connected.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Mar 21 14:18:37 2019 +0000
@@ -135,6 +135,9 @@
subsection%unimportant\<open>Basic lemmas about paths\<close>
+lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g"
+ by (simp add: pathin_def path_def)
+
lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
using continuous_on_subset path_def by blast
@@ -1468,7 +1471,7 @@
lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
unfolding path_component_def by auto
-lemma path_connected_linepath:
+lemma path_component_linepath:
fixes s :: "'a::real_normed_vector set"
shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
unfolding path_component_def
@@ -1502,6 +1505,10 @@
definition%important "path_connected s \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
+lemma path_connectedin_iff_path_connected_real [simp]:
+ "path_connectedin euclideanreal S \<longleftrightarrow> path_connected S"
+ by (simp add: path_connectedin path_connected_def path_defs)
+
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
unfolding path_connected_def path_component_def by auto
@@ -1818,6 +1825,29 @@
lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
by (simp add: convex_imp_path_connected is_interval_convex)
+lemma path_connectedin_path_image:
+ assumes "pathin X g" shows "path_connectedin X (g ` ({0..1}))"
+ unfolding pathin_def
+proof (rule path_connectedin_continuous_map_image)
+ show "continuous_map (subtopology euclideanreal {0..1}) X g"
+ using assms pathin_def by blast
+qed (auto simp: is_interval_1 is_interval_path_connected)
+
+lemma path_connected_space_subconnected:
+ "path_connected_space X \<longleftrightarrow>
+ (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. path_connectedin X S \<and> x \<in> S \<and> y \<in> S)"
+ unfolding path_connected_space_def Ball_def
+ apply (intro all_cong1 imp_cong refl, safe)
+ using path_connectedin_path_image apply fastforce
+ by (meson path_connectedin)
+
+lemma connectedin_path_image: "pathin X g \<Longrightarrow> connectedin X (g ` ({0..1}))"
+ by (simp add: path_connectedin_imp_connectedin path_connectedin_path_image)
+
+lemma compactin_path_image: "pathin X g \<Longrightarrow> compactin X (g ` ({0..1}))"
+ unfolding pathin_def
+ by (rule image_compactin [of "top_of_set {0..1}"]) auto
+
lemma linear_homeomorphism_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
@@ -1935,6 +1965,372 @@
qed
+subsection\<open>Path components\<close>
+
+definition path_component_of
+ where "path_component_of X x y \<equiv> \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
+
+abbreviation path_component_of_set
+ where "path_component_of_set X x \<equiv> Collect (path_component_of X x)"
+
+definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
+ where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
+
+lemma path_component_in_topspace:
+ "path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
+ by (auto simp: path_component_of_def pathin_def continuous_map_def)
+
+lemma path_component_of_refl:
+ "path_component_of X x x \<longleftrightarrow> x \<in> topspace X"
+ apply (auto simp: path_component_in_topspace)
+ apply (force simp: path_component_of_def pathin_const)
+ done
+
+lemma path_component_of_sym:
+ assumes "path_component_of X x y"
+ shows "path_component_of X y x"
+ using assms
+ apply (clarsimp simp: path_component_of_def pathin_def)
+ apply (rule_tac x="g \<circ> (\<lambda>t. 1 - t)" in exI)
+ apply (auto intro!: continuous_map_compose)
+ apply (force simp: continuous_map_in_subtopology continuous_on_op_minus)
+ done
+
+lemma path_component_of_sym_iff:
+ "path_component_of X x y \<longleftrightarrow> path_component_of X y x"
+ by (metis path_component_of_sym)
+
+lemma path_component_of_trans:
+ assumes "path_component_of X x y" and "path_component_of X y z"
+ shows "path_component_of X x z"
+ unfolding path_component_of_def pathin_def
+proof -
+ let ?T01 = "top_of_set {0..1::real}"
+ obtain g1 g2 where g1: "continuous_map ?T01 X g1" "x = g1 0" "y = g1 1"
+ and g2: "continuous_map ?T01 X g2" "g2 0 = g1 1" "z = g2 1"
+ using assms unfolding path_component_of_def pathin_def by blast
+ let ?g = "\<lambda>x. if x \<le> 1/2 then (g1 \<circ> (\<lambda>t. 2 * t)) x else (g2 \<circ> (\<lambda>t. 2 * t -1)) x"
+ show "\<exists>g. continuous_map ?T01 X g \<and> g 0 = x \<and> g 1 = z"
+ proof (intro exI conjI)
+ show "continuous_map (subtopology euclideanreal {0..1}) X ?g"
+ proof (intro continuous_map_cases_le continuous_map_compose, force, force)
+ show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. x \<le> 1/2}) ?T01 ((*) 2)"
+ by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
+ have "continuous_map
+ (subtopology (top_of_set {0..1}) {x. 0 \<le> x \<and> x \<le> 1 \<and> 1 \<le> x * 2})
+ euclideanreal (\<lambda>t. 2 * t - 1)"
+ by (intro continuous_intros) (force intro: continuous_map_from_subtopology)
+ then show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. 1/2 \<le> x}) ?T01 (\<lambda>t. 2 * t - 1)"
+ by (force simp: continuous_map_in_subtopology)
+ show "(g1 \<circ> (*) 2) x = (g2 \<circ> (\<lambda>t. 2 * t - 1)) x" if "x \<in> topspace ?T01" "x = 1/2" for x
+ using that by (simp add: g2(2) mult.commute continuous_map_from_subtopology)
+ qed (auto simp: g1 g2)
+ qed (auto simp: g1 g2)
+qed
+
+
+lemma path_component_of_mono:
+ "\<lbrakk>path_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> \<Longrightarrow> path_component_of (subtopology X T) x y"
+ unfolding path_component_of_def
+ by (metis subsetD pathin_subtopology)
+
+
+lemma path_component_of:
+ "path_component_of X x y \<longleftrightarrow> (\<exists>T. path_connectedin X T \<and> x \<in> T \<and> y \<in> T)"
+ apply (auto simp: path_component_of_def)
+ using path_connectedin_path_image apply fastforce
+ apply (metis path_connectedin)
+ done
+
+lemma path_component_of_set:
+ "path_component_of X x y \<longleftrightarrow> (\<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y)"
+ by (auto simp: path_component_of_def)
+
+lemma path_component_of_subset_topspace:
+ "Collect(path_component_of X x) \<subseteq> topspace X"
+ using path_component_in_topspace by fastforce
+
+lemma path_component_of_eq_empty:
+ "Collect(path_component_of X x) = {} \<longleftrightarrow> (x \<notin> topspace X)"
+ using path_component_in_topspace path_component_of_refl by fastforce
+
+lemma path_connected_space_iff_path_component:
+ "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. path_component_of X x y)"
+ by (simp add: path_component_of path_connected_space_subconnected)
+
+lemma path_connected_space_imp_path_component_of:
+ "\<lbrakk>path_connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk>
+ \<Longrightarrow> path_component_of X a b"
+ by (simp add: path_connected_space_iff_path_component)
+
+lemma path_connected_space_path_component_set:
+ "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. Collect(path_component_of X x) = topspace X)"
+ using path_component_of_subset_topspace path_connected_space_iff_path_component by fastforce
+
+lemma path_component_of_maximal:
+ "\<lbrakk>path_connectedin X s; x \<in> s\<rbrakk> \<Longrightarrow> s \<subseteq> Collect(path_component_of X x)"
+ using path_component_of by fastforce
+
+lemma path_component_of_equiv:
+ "path_component_of X x y \<longleftrightarrow> x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ apply (simp add: fun_eq_iff path_component_in_topspace)
+ apply (meson path_component_of_sym path_component_of_trans)
+ done
+qed (simp add: path_component_of_refl)
+
+lemma path_component_of_disjoint:
+ "disjnt (Collect (path_component_of X x)) (Collect (path_component_of X y)) \<longleftrightarrow>
+ ~(path_component_of X x y)"
+ by (force simp: disjnt_def path_component_of_eq_empty path_component_of_equiv)
+
+lemma path_component_of_eq:
+ "path_component_of X x = path_component_of X y \<longleftrightarrow>
+ (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
+ x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x y"
+ by (metis Collect_empty_eq_bot path_component_of_eq_empty path_component_of_equiv)
+
+lemma path_connectedin_path_component_of:
+ "path_connectedin X (Collect (path_component_of X x))"
+proof -
+ have "\<And>y. path_component_of X x y
+ \<Longrightarrow> path_component_of (subtopology X (Collect (path_component_of X x))) x y"
+ by (meson path_component_of path_component_of_maximal path_connectedin_subtopology)
+ then show ?thesis
+ apply (simp add: path_connectedin_def path_component_of_subset_topspace path_connected_space_iff_path_component)
+ by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
+qed
+
+lemma Union_path_components_of:
+ "\<Union>(path_components_of X) = topspace X"
+ by (auto simp: path_components_of_def path_component_of_equiv)
+
+lemma path_components_of_maximal:
+ "\<lbrakk>C \<in> path_components_of X; path_connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
+ apply (auto simp: path_components_of_def path_component_of_equiv)
+ using path_component_of_maximal path_connectedin_def apply fastforce
+ by (meson disjnt_subset2 path_component_of_disjoint path_component_of_equiv path_component_of_maximal)
+
+lemma pairwise_disjoint_path_components_of:
+ "pairwise disjnt (path_components_of X)"
+ by (auto simp: path_components_of_def pairwise_def path_component_of_disjoint path_component_of_equiv)
+
+lemma complement_path_components_of_Union:
+ "C \<in> path_components_of X
+ \<Longrightarrow> topspace X - C = \<Union>(path_components_of X - {C})"
+ by (metis Diff_cancel Diff_subset Union_path_components_of cSup_singleton diff_Union_pairwise_disjoint insert_subset pairwise_disjoint_path_components_of)
+
+lemma nonempty_path_components_of:
+ "C \<in> path_components_of X \<Longrightarrow> (C \<noteq> {})"
+ apply (clarsimp simp: path_components_of_def path_component_of_eq_empty)
+ by (meson path_component_of_refl)
+
+lemma path_components_of_subset: "C \<in> path_components_of X \<Longrightarrow> C \<subseteq> topspace X"
+ by (auto simp: path_components_of_def path_component_of_equiv)
+
+lemma path_connectedin_path_components_of:
+ "C \<in> path_components_of X \<Longrightarrow> path_connectedin X C"
+ by (auto simp: path_components_of_def path_connectedin_path_component_of)
+
+lemma path_component_in_path_components_of:
+ "Collect (path_component_of X a) \<in> path_components_of X \<longleftrightarrow> a \<in> topspace X"
+ apply (rule iffI)
+ using nonempty_path_components_of path_component_of_eq_empty apply fastforce
+ by (simp add: path_components_of_def)
+
+lemma path_connectedin_Union:
+ assumes \<A>: "\<And>S. S \<in> \<A> \<Longrightarrow> path_connectedin X S" "\<Inter>\<A> \<noteq> {}"
+ shows "path_connectedin X (\<Union>\<A>)"
+proof -
+ obtain a where "\<And>S. S \<in> \<A> \<Longrightarrow> a \<in> S"
+ using assms by blast
+ then have "\<And>x. x \<in> topspace (subtopology X (\<Union>\<A>)) \<Longrightarrow> path_component_of (subtopology X (\<Union>\<A>)) a x"
+ apply (simp add: topspace_subtopology)
+ by (meson Union_upper \<A> path_component_of path_connectedin_subtopology)
+ then show ?thesis
+ using \<A> unfolding path_connectedin_def
+ by (metis Sup_le_iff path_component_of_equiv path_connected_space_iff_path_component)
+qed
+
+lemma path_connectedin_Un:
+ "\<lbrakk>path_connectedin X S; path_connectedin X T; S \<inter> T \<noteq> {}\<rbrakk>
+ \<Longrightarrow> path_connectedin X (S \<union> T)"
+ by (blast intro: path_connectedin_Union [of "{S,T}", simplified])
+
+lemma path_connected_space_iff_components_eq:
+ "path_connected_space X \<longleftrightarrow>
+ (\<forall>C \<in> path_components_of X. \<forall>C' \<in> path_components_of X. C = C')"
+ unfolding path_components_of_def
+proof (intro iffI ballI)
+ assume "\<forall>C \<in> path_component_of_set X ` topspace X.
+ \<forall>C' \<in> path_component_of_set X ` topspace X. C = C'"
+ then show "path_connected_space X"
+ using path_component_of_refl path_connected_space_iff_path_component by fastforce
+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
+
+lemma path_components_of_empty_space:
+ "topspace X = {} \<Longrightarrow> path_components_of X = {}"
+ by (simp add: path_components_of_eq_empty)
+
+lemma path_components_of_subset_singleton:
+ "path_components_of X \<subseteq> {S} \<longleftrightarrow>
+ path_connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
+proof (cases "topspace X = {}")
+ case True
+ then show ?thesis
+ by (auto simp: path_components_of_empty_space path_connected_space_topspace_empty)
+next
+ case False
+ have "(path_components_of X = {S}) \<longleftrightarrow> (path_connected_space X \<and> topspace X = S)"
+ proof (intro iffI conjI)
+ assume L: "path_components_of X = {S}"
+ then show "path_connected_space X"
+ by (simp add: path_connected_space_iff_components_eq)
+ show "topspace X = S"
+ by (metis L ccpo_Sup_singleton [of S] Union_path_components_of)
+ next
+ assume R: "path_connected_space X \<and> topspace X = S"
+ then show "path_components_of X = {S}"
+ using ccpo_Sup_singleton [of S]
+ by (metis False all_not_in_conv insert_iff mk_disjoint_insert path_component_in_path_components_of path_connected_space_iff_components_eq path_connected_space_path_component_set)
+ qed
+ with False show ?thesis
+ by (simp add: path_components_of_eq_empty subset_singleton_iff)
+qed
+
+lemma path_connected_space_iff_components_subset_singleton:
+ "path_connected_space X \<longleftrightarrow> (\<exists>a. path_components_of X \<subseteq> {a})"
+ by (simp add: path_components_of_subset_singleton)
+
+lemma path_components_of_eq_singleton:
+ "path_components_of X = {S} \<longleftrightarrow> path_connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
+ by (metis cSup_singleton insert_not_empty path_components_of_subset_singleton subset_singleton_iff)
+
+lemma path_components_of_path_connected_space:
+ "path_connected_space X \<Longrightarrow> path_components_of X = (if topspace X = {} then {} else {topspace X})"
+ by (simp add: path_components_of_eq_empty path_components_of_eq_singleton)
+
+lemma path_component_subset_connected_component_of:
+ "path_component_of_set X x \<subseteq> connected_component_of_set X x"
+proof (cases "x \<in> topspace X")
+ case True
+ then show ?thesis
+ by (simp add: connected_component_of_maximal path_component_of_refl path_connectedin_imp_connectedin path_connectedin_path_component_of)
+next
+ case False
+ then show ?thesis
+ using path_component_of_eq_empty by fastforce
+qed
+
+lemma exists_path_component_of_superset:
+ assumes S: "path_connectedin X S" and ne: "topspace X \<noteq> {}"
+ obtains C where "C \<in> path_components_of X" "S \<subseteq> C"
+proof (cases "S = {}")
+ case True
+ then show ?thesis
+ using ne path_components_of_eq_empty that by fastforce
+next
+ case False
+ then obtain a where "a \<in> S"
+ by blast
+ show ?thesis
+ proof
+ show "Collect (path_component_of X a) \<in> path_components_of X"
+ by (meson \<open>a \<in> S\<close> S subsetD path_component_in_path_components_of path_connectedin_subset_topspace)
+ show "S \<subseteq> Collect (path_component_of X a)"
+ by (simp add: S \<open>a \<in> S\<close> path_component_of_maximal)
+ qed
+qed
+
+lemma path_component_of_eq_overlap:
+ "path_component_of X x = path_component_of X y \<longleftrightarrow>
+ (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
+ Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {}"
+ by (metis disjnt_def empty_iff inf_bot_right mem_Collect_eq path_component_of_disjoint path_component_of_eq path_component_of_eq_empty)
+
+lemma path_component_of_nonoverlap:
+ "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) = {} \<longleftrightarrow>
+ (x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or>
+ path_component_of X x \<noteq> path_component_of X y"
+ by (metis inf.idem path_component_of_eq_empty path_component_of_eq_overlap)
+
+lemma path_component_of_overlap:
+ "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {} \<longleftrightarrow>
+ x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
+ by (meson path_component_of_nonoverlap)
+
+lemma path_components_of_disjoint:
+ "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> disjnt C C' \<longleftrightarrow> C \<noteq> C'"
+ by (auto simp: path_components_of_def path_component_of_disjoint path_component_of_equiv)
+
+lemma path_components_of_overlap:
+ "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> C \<inter> C' \<noteq> {} \<longleftrightarrow> C = C'"
+ by (auto simp: path_components_of_def path_component_of_equiv)
+
+lemma path_component_of_unique:
+ "\<lbrakk>x \<in> C; path_connectedin X C; \<And>C'. \<lbrakk>x \<in> C'; path_connectedin X C'\<rbrakk> \<Longrightarrow> C' \<subseteq> C\<rbrakk>
+ \<Longrightarrow> Collect (path_component_of X x) = C"
+ by (meson subsetD eq_iff path_component_of_maximal path_connectedin_path_component_of)
+
+lemma path_component_of_discrete_topology [simp]:
+ "Collect (path_component_of (discrete_topology U) x) = (if x \<in> U then {x} else {})"
+proof -
+ have "\<And>C'. \<lbrakk>x \<in> C'; path_connectedin (discrete_topology U) C'\<rbrakk> \<Longrightarrow> C' \<subseteq> {x}"
+ by (metis path_connectedin_discrete_topology subsetD singletonD)
+ then have "x \<in> U \<Longrightarrow> Collect (path_component_of (discrete_topology U) x) = {x}"
+ by (simp add: path_component_of_unique)
+ then show ?thesis
+ using path_component_in_topspace by fastforce
+qed
+
+lemma path_component_of_discrete_topology_iff [simp]:
+ "path_component_of (discrete_topology U) x y \<longleftrightarrow> x \<in> U \<and> y=x"
+ by (metis empty_iff insertI1 mem_Collect_eq path_component_of_discrete_topology singletonD)
+
+lemma path_components_of_discrete_topology [simp]:
+ "path_components_of (discrete_topology U) = (\<lambda>x. {x}) ` U"
+ by (auto simp: path_components_of_def image_def fun_eq_iff)
+
+lemma homeomorphic_map_path_component_of:
+ assumes f: "homeomorphic_map X Y f" and x: "x \<in> topspace X"
+ shows "Collect (path_component_of Y (f x)) = f ` Collect(path_component_of X x)"
+proof -
+ obtain g where g: "homeomorphic_maps X Y f g"
+ using f homeomorphic_map_maps by blast
+ show ?thesis
+ proof
+ have "Collect (path_component_of Y (f x)) \<subseteq> topspace Y"
+ 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 g x unfolding homeomorphic_maps_def
+ by (metis f homeomorphic_imp_surjective_map imageI mem_Collect_eq path_component_of_maximal path_component_of_refl 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
+ show "f ` Collect (path_component_of X x) \<subseteq> Collect (path_component_of Y (f x))"
+ proof (rule path_component_of_maximal)
+ show "path_connectedin Y (f ` Collect (path_component_of X x))"
+ by (meson f homeomorphic_map_path_connectedness_eq path_connectedin_path_component_of)
+ qed (simp add: path_component_of_refl x)
+ qed
+qed
+
+lemma homeomorphic_map_path_components_of:
+ assumes "homeomorphic_map X Y f"
+ shows "path_components_of Y = (image f) ` (path_components_of X)"
+ unfolding path_components_of_def homeomorphic_imp_surjective_map [OF assms, symmetric]
+ apply safe
+ using assms homeomorphic_map_path_component_of apply fastforce
+ by (metis assms homeomorphic_map_path_component_of imageI)
+
+
subsection \<open>Sphere is path-connected\<close>
lemma path_connected_punctured_universe:
@@ -2078,7 +2474,7 @@
done
}
then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))"
- by (force simp: closed_segment_def intro!: path_connected_linepath)
+ by (force simp: closed_segment_def intro!: path_component_linepath)
define D where "D = B / norm(y - a)" \<comment> \<open>massive duplication with the proof above\<close>
{ fix u
assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \<in> s" and "0 \<le> u" "u \<le> 1"
@@ -2113,7 +2509,7 @@
done
}
then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))"
- by (force simp: closed_segment_def intro!: path_connected_linepath)
+ by (force simp: closed_segment_def intro!: path_component_linepath)
have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))"
apply (rule path_component_of_subset [of "sphere a B"])
using \<open>s \<subseteq> ball a B\<close>
--- a/src/HOL/Analysis/Product_Topology.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1,15 +1,12 @@
+section\<open>The binary product topology\<close>
+
theory Product_Topology
imports Function_Topology
begin
-lemma subset_UnE: (*FIXME MOVE*)
- assumes "C \<subseteq> A \<union> B"
- obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
- by (metis assms Int_Un_distrib inf.order_iff inf_le2)
-
section \<open>Product Topology\<close>
-subsection\<open>A binary product topology where the two types can be different.\<close>
+subsection\<open>Definition\<close>
definition prod_topology :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<times> 'b) topology" where
"prod_topology X Y \<equiv> topology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
@@ -34,7 +31,7 @@
proof (rule topology_inverse')
show "istopology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
apply (rule istopology_base, simp)
- by (metis openin_Int times_Int_times)
+ by (metis openin_Int Times_Int_Times)
qed
lemma topspace_prod_topology [simp]:
@@ -62,7 +59,7 @@
proof -
have "((\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T) relative_to S \<times> T) =
(\<lambda>U. \<exists>S' T'. U = S' \<times> T' \<and> (openin X relative_to S) S' \<and> (openin Y relative_to T) T')"
- by (auto simp: relative_to_def times_Int_times fun_eq_iff) metis
+ by (auto simp: relative_to_def Times_Int_Times fun_eq_iff) metis
then show ?thesis
by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to)
qed
@@ -81,7 +78,7 @@
lemma prod_topology_subtopology_eu [simp]:
"prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)"
- by (simp add: prod_topology_subtopology subtopology_subtopology times_Int_times)
+ by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)
lemma continuous_map_subtopology_eu [simp]:
"continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
@@ -128,6 +125,29 @@
"closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T"
by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)
+lemma interior_of_Times: "(prod_topology X Y) interior_of (S \<times> T) = (X interior_of S) \<times> (Y interior_of T)"
+proof (rule interior_of_unique)
+ show "(X interior_of S) \<times> Y interior_of T \<subseteq> S \<times> T"
+ by (simp add: Sigma_mono interior_of_subset)
+ show "openin (prod_topology X Y) ((X interior_of S) \<times> Y interior_of T)"
+ by (simp add: openin_Times)
+next
+ show "T' \<subseteq> (X interior_of S) \<times> Y interior_of T" if "T' \<subseteq> S \<times> T" "openin (prod_topology X Y) T'" for T'
+ proof (clarsimp; intro conjI)
+ fix a :: "'a" and b :: "'b"
+ assume "(a, b) \<in> T'"
+ with that obtain U V where UV: "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> T'"
+ by (metis openin_prod_topology_alt)
+ then show "a \<in> X interior_of S"
+ using interior_of_maximal_eq that(1) by fastforce
+ show "b \<in> Y interior_of T"
+ using UV interior_of_maximal_eq that(1)
+ by (metis SigmaI mem_Sigma_iff subset_eq)
+ qed
+qed
+
+subsection \<open>Continuity\<close>
+
lemma continuous_map_pairwise:
"continuous_map Z (prod_topology X Y) f \<longleftrightarrow> continuous_map Z X (fst \<circ> f) \<and> continuous_map Z Y (snd \<circ> f)"
(is "?lhs = ?rhs")
@@ -297,37 +317,6 @@
by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def])
qed
-lemma 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') = {} \<or>
- homeomorphic_maps X X' f f' \<and>
- homeomorphic_maps Y Y' g g'"
- unfolding homeomorphic_maps_def continuous_map_prod_top
- by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
-
-lemma embedding_map_graph:
- "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
- (is "?lhs = ?rhs")
-proof
- assume L: ?lhs
- have "snd \<circ> (\<lambda>x. (x, f x)) = f"
- by force
- moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
- using L
- unfolding embedding_map_def
- by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
- ultimately show ?rhs
- by simp
-next
- assume R: ?rhs
- then show ?lhs
- unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
- by (rule_tac x=fst in exI)
- (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
- continuous_map_fst topspace_subtopology)
-qed
-
lemma in_prod_topology_closure_of:
assumes "z \<in> (prod_topology X Y) closure_of S"
shows "fst z \<in> X closure_of (fst ` S)" "snd z \<in> Y closure_of (snd ` S)"
@@ -412,7 +401,7 @@
then show ?case
unfolding \<X>_def \<Y>_def
apply (simp add: Int_ac subset_eq image_def)
- apply (metis (no_types) openin_Int openin_topspace times_Int_times)
+ apply (metis (no_types) openin_Int openin_topspace Times_Int_Times)
done
qed auto
then show ?thesis
@@ -450,10 +439,85 @@
using False by blast
qed
-
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)
+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') = {} \<or>
+ homeomorphic_maps X X' f f' \<and>
+ homeomorphic_maps Y Y' g g'"
+ unfolding homeomorphic_maps_def continuous_map_prod_top
+ by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
+
+lemma embedding_map_graph:
+ "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ have "snd \<circ> (\<lambda>x. (x, f x)) = f"
+ by force
+ moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
+ using L
+ unfolding embedding_map_def
+ by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
+ ultimately show ?rhs
+ by simp
+next
+ assume R: ?rhs
+ then show ?lhs
+ unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
+ by (rule_tac x=fst in exI)
+ (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
+ continuous_map_fst topspace_subtopology)
+qed
+
+lemma homeomorphic_space_prod_topology:
+ "\<lbrakk>X homeomorphic_space X''; Y homeomorphic_space Y'\<rbrakk>
+ \<Longrightarrow> prod_topology X Y homeomorphic_space prod_topology X'' Y'"
+using homeomorphic_maps_prod unfolding homeomorphic_space_def by blast
+
+lemma prod_topology_homeomorphic_space_left:
+ "topspace Y = {b} \<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)
+
+lemma prod_topology_homeomorphic_space_right:
+ "topspace X = {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)
+
+
+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)
+
+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)
+
+lemma topological_property_of_prod_component:
+ assumes major: "P(prod_topology X Y)"
+ and X: "\<And>x. \<lbrakk>x \<in> topspace X; P(prod_topology X Y)\<rbrakk> \<Longrightarrow> P(subtopology (prod_topology X Y) ({x} \<times> topspace Y))"
+ 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"
+proof -
+ have "Q X \<and> R Y" if "topspace(prod_topology X Y) \<noteq> {}"
+ proof -
+ from that obtain a b where a: "a \<in> topspace X" and b: "b \<in> topspace Y"
+ by force
+ show ?thesis
+ using X [OF a major] and Y [OF b major] homeomorphic_space_prod_topology_sing1 [OF b, of X] homeomorphic_space_prod_topology_sing2 [OF a, of Y]
+ by (simp add: subtopology_Times) (meson PQ PR homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym)
+ qed
+ then show ?thesis by metis
+qed
+
end
--- a/src/HOL/Analysis/T1_Spaces.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1,7 +1,7 @@
section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
theory T1_Spaces
-imports Function_Topology
+imports Product_Topology
begin
definition t1_space where
@@ -198,4 +198,20 @@
using False by blast
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) = {}")
+ case True then show ?thesis
+ by (auto simp: t1_space_empty)
+next
+ case False
+ have eq: "{(x,y)} = {x} \<times> {y}" for x y
+ 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_Times eq simp del: insert_Times_insert)
+ with False show ?thesis
+ by simp
+qed
+
end
--- a/src/HOL/Library/FuncSet.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Library/FuncSet.thy Thu Mar 21 14:18:37 2019 +0000
@@ -550,6 +550,11 @@
lemma PiE_eq_singleton: "(\<Pi>\<^sub>E i\<in>I. S i) = {\<lambda>i\<in>I. f i} \<longleftrightarrow> (\<forall>i\<in>I. S i = {f i})"
by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
+lemma PiE_over_singleton_iff: "(\<Pi>\<^sub>E x\<in>{a}. B x) = (\<Union>b \<in> B a. {\<lambda>x \<in> {a}. b})"
+ apply (auto simp: PiE_iff split: if_split_asm)
+ apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
+ done
+
lemma all_PiE_elements:
"(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
proof (cases "PiE I S = {}")
--- a/src/HOL/Product_Type.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1134,7 +1134,7 @@
by (cases "f x") (auto split: prod.split)
qed
-lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
+lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
by auto
lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
--- a/src/HOL/Set.thy Thu Mar 21 14:54:25 2019 +0100
+++ b/src/HOL/Set.thy Thu Mar 21 14:18:37 2019 +0000
@@ -1354,6 +1354,13 @@
lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
by blast
+lemma subset_UnE:
+ assumes "C \<subseteq> A \<union> B"
+ obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
+proof
+ show "C \<inter> A \<subseteq> A" "C \<inter> B \<subseteq> B" "C = (C \<inter> A) \<union> (C \<inter> B)"
+ using assms by blast+
+qed
text \<open>\<^medskip> Set complement\<close>
@@ -1594,6 +1601,9 @@
"\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
by auto
+lemma ex_image_cong_iff [simp, no_atp]:
+ "(\<exists>x. x\<in>f`A) \<longleftrightarrow> A \<noteq> {}" "(\<exists>x. x\<in>f`A \<and> P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
+ by auto
subsubsection \<open>Monotonicity of various operations\<close>