# HG changeset patch
# User immler
# Date 1518086882 -3600
# Node ID 0ac53b6662282f6c2dc90d2bcf923f5a4237b94b
# Parent  b01b22f9e42e7f9874bcbccb9b94324724cf8f49
more elementary proof of connected_Times, earlier

diff -r b01b22f9e42e -r 0ac53b666228 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Feb 08 08:59:28 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Feb 08 11:48:02 2018 +0100
@@ -600,54 +600,6 @@
   apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
   using connected_component_eq_empty by blast
 
-proposition connected_Times:
-  assumes S: "connected S" and T: "connected T"
-  shows "connected (S \<times> T)"
-proof (clarsimp simp add: connected_iff_connected_component)
-  fix x y x' y'
-  assume xy: "x \<in> S" "y \<in> T" "x' \<in> S" "y' \<in> T"
-  with xy obtain U V where U: "connected U" "U \<subseteq> S" "x \<in> U" "x' \<in> U"
-                       and V: "connected V" "V \<subseteq> T" "y \<in> V" "y' \<in> V"
-    using S T \<open>x \<in> S\<close> \<open>x' \<in> S\<close> by blast+
-  show "connected_component (S \<times> T) (x, y) (x', y')"
-    unfolding connected_component_def
-  proof (intro exI conjI)
-    show "connected ((\<lambda>x. (x, y)) ` U \<union> Pair x' ` V)"
-    proof (rule connected_Un)
-      have "continuous_on U (\<lambda>x. (x, y))"
-        by (intro continuous_intros)
-      then show "connected ((\<lambda>x. (x, y)) ` U)"
-        by (rule connected_continuous_image) (rule \<open>connected U\<close>)
-      have "continuous_on V (Pair x')"
-        by (intro continuous_intros)
-      then show "connected (Pair x' ` V)"
-        by (rule connected_continuous_image) (rule \<open>connected V\<close>)
-    qed (use U V in auto)
-  qed (use U V in auto)
-qed
-
-corollary connected_Times_eq [simp]:
-   "connected (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> connected S \<and> connected T"  (is "?lhs = ?rhs")
-proof
-  assume L: ?lhs
-  show ?rhs
-  proof (cases "S = {} \<or> T = {}")
-    case True
-    then show ?thesis by auto
-  next
-    case False
-    have "connected (fst ` (S \<times> T))" "connected (snd ` (S \<times> T))"
-      using continuous_on_fst continuous_on_snd continuous_on_id
-      by (blast intro: connected_continuous_image [OF _ L])+
-    with False show ?thesis
-      by auto
-  qed
-next
-  assume ?rhs
-  then show ?lhs
-    by (auto simp: connected_Times)
-qed
-
 
 subsection \<open>The set of connected components of a set\<close>
 
diff -r b01b22f9e42e -r 0ac53b666228 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Feb 08 08:59:28 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Feb 08 11:48:02 2018 +0100
@@ -3455,6 +3455,46 @@
   by (fact continuous_Pair)
 
 
+subsubsection \<open>Connectedness of products\<close>
+
+proposition connected_Times:
+  assumes S: "connected S" and T: "connected T"
+  shows "connected (S \<times> T)"
+proof (rule connectedI_const)
+  fix P::"'a \<times> 'b \<Rightarrow> bool"
+  assume P[THEN continuous_on_compose2, continuous_intros]: "continuous_on (S \<times> T) P"
+  have "continuous_on S (\<lambda>s. P (s, t))" if "t \<in> T" for t
+    by (auto intro!: continuous_intros that)
+  from connectedD_const[OF S this]
+  obtain c1 where c1: "\<And>s t. t \<in> T \<Longrightarrow> s \<in> S \<Longrightarrow> P (s, t) = c1 t"
+    by metis
+  moreover
+  have "continuous_on T (\<lambda>t. P (s, t))" if "s \<in> S" for s
+    by (auto intro!: continuous_intros that)
+  from connectedD_const[OF T this]
+  obtain c2 where "\<And>s t. t \<in> T \<Longrightarrow> s \<in> S \<Longrightarrow> P (s, t) = c2 s"
+    by metis
+  ultimately show "\<exists>c. \<forall>s\<in>S \<times> T. P s = c"
+    by auto
+qed
+
+corollary connected_Times_eq [simp]:
+   "connected (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> connected S \<and> connected T"  (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  show ?rhs
+  proof cases
+    assume "S \<noteq> {} \<and> T \<noteq> {}"
+    moreover
+    have "connected (fst ` (S \<times> T))" "connected (snd ` (S \<times> T))"
+      using continuous_on_fst continuous_on_snd continuous_on_id
+      by (blast intro: connected_continuous_image [OF _ L])+
+    ultimately show ?thesis
+      by auto
+  qed auto
+qed (auto simp: connected_Times)
+
+
 subsubsection \<open>Separation axioms\<close>
 
 instance prod :: (t0_space, t0_space) t0_space