summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | immler |

Thu, 08 Feb 2018 11:48:02 +0100 | |

changeset 67577 | 0ac53b666228 |

parent 67576 | b01b22f9e42e |

child 67579 | 1a636c22d85c |

more elementary proof of connected_Times, earlier

src/HOL/Analysis/Connected.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Topological_Spaces.thy | file | annotate | diff | comparison | revisions |

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

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