# 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 \ T)" -proof (clarsimp simp add: connected_iff_connected_component) - fix x y x' y' - assume xy: "x \ S" "y \ T" "x' \ S" "y' \ T" - with xy obtain U V where U: "connected U" "U \ S" "x \ U" "x' \ U" - and V: "connected V" "V \ T" "y \ V" "y' \ V" - using S T \x \ S\ \x' \ S\ by blast+ - show "connected_component (S \ T) (x, y) (x', y')" - unfolding connected_component_def - proof (intro exI conjI) - show "connected ((\x. (x, y)) ` U \ Pair x' ` V)" - proof (rule connected_Un) - have "continuous_on U (\x. (x, y))" - by (intro continuous_intros) - then show "connected ((\x. (x, y)) ` U)" - by (rule connected_continuous_image) (rule \connected U\) - have "continuous_on V (Pair x')" - by (intro continuous_intros) - then show "connected (Pair x' ` V)" - by (rule connected_continuous_image) (rule \connected V\) - qed (use U V in auto) - qed (use U V in auto) -qed - -corollary connected_Times_eq [simp]: - "connected (S \ T) \ S = {} \ T = {} \ connected S \ connected T" (is "?lhs = ?rhs") -proof - assume L: ?lhs - show ?rhs - proof (cases "S = {} \ T = {}") - case True - then show ?thesis by auto - next - case False - have "connected (fst ` (S \ T))" "connected (snd ` (S \ 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 \The set of connected components of a set\ 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 \Connectedness of products\ + +proposition connected_Times: + assumes S: "connected S" and T: "connected T" + shows "connected (S \ T)" +proof (rule connectedI_const) + fix P::"'a \ 'b \ bool" + assume P[THEN continuous_on_compose2, continuous_intros]: "continuous_on (S \ T) P" + have "continuous_on S (\s. P (s, t))" if "t \ T" for t + by (auto intro!: continuous_intros that) + from connectedD_const[OF S this] + obtain c1 where c1: "\s t. t \ T \ s \ S \ P (s, t) = c1 t" + by metis + moreover + have "continuous_on T (\t. P (s, t))" if "s \ S" for s + by (auto intro!: continuous_intros that) + from connectedD_const[OF T this] + obtain c2 where "\s t. t \ T \ s \ S \ P (s, t) = c2 s" + by metis + ultimately show "\c. \s\S \ T. P s = c" + by auto +qed + +corollary connected_Times_eq [simp]: + "connected (S \ T) \ S = {} \ T = {} \ connected S \ connected T" (is "?lhs = ?rhs") +proof + assume L: ?lhs + show ?rhs + proof cases + assume "S \ {} \ T \ {}" + moreover + have "connected (fst ` (S \ T))" "connected (snd ` (S \ 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 \Separation axioms\ instance prod :: (t0_space, t0_space) t0_space