1 (* Author: L C Paulson, University of Cambridge |
1 (* Author: L C Paulson, University of Cambridge |
2 Material split off from Topology_Euclidean_Space |
2 Material split off from Topology_Euclidean_Space |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Connected Components, Homeomorphisms, Baire property, etc\<close> |
5 section \<open>Connected Components\<close> |
6 |
6 |
7 theory Connected |
7 theory Connected |
8 imports |
8 imports |
9 Topology_Euclidean_Space |
9 Abstract_Topology_2 |
10 begin |
10 begin |
11 |
11 |
12 subsection%unimportant \<open>Connectedness\<close> |
12 subsection%unimportant \<open>Connectedness\<close> |
13 |
13 |
14 lemma connected_local: |
14 lemma connected_local: |
64 by blast |
64 by blast |
65 then show ?thesis |
65 then show ?thesis |
66 by (simp add: th0 th1) |
66 by (simp add: th0 th1) |
67 qed |
67 qed |
68 |
68 |
69 lemma connected_linear_image: |
|
70 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
71 assumes "linear f" and "connected s" |
|
72 shows "connected (f ` s)" |
|
73 using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast |
|
74 |
|
75 subsection \<open>Connected components, considered as a connectedness relation or a set\<close> |
69 subsection \<open>Connected components, considered as a connectedness relation or a set\<close> |
76 |
70 |
77 definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t" |
71 definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t" |
78 |
72 |
79 abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)" |
73 abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)" |
322 "connected t \<and> t \<subseteq> s \<and> c1 \<in> components s \<and> c2 \<in> components s \<and> c1 \<inter> t \<noteq> {} \<and> c2 \<inter> t \<noteq> {} \<Longrightarrow> c1 = c2" |
316 "connected t \<and> t \<subseteq> s \<and> c1 \<in> components s \<and> c2 \<in> components s \<and> c1 \<inter> t \<noteq> {} \<and> c2 \<inter> t \<noteq> {} \<Longrightarrow> c1 = c2" |
323 by (metis (full_types) components_iff joinable_connected_component_eq) |
317 by (metis (full_types) components_iff joinable_connected_component_eq) |
324 |
318 |
325 lemma closed_components: "\<lbrakk>closed s; c \<in> components s\<rbrakk> \<Longrightarrow> closed c" |
319 lemma closed_components: "\<lbrakk>closed s; c \<in> components s\<rbrakk> \<Longrightarrow> closed c" |
326 by (metis closed_connected_component components_iff) |
320 by (metis closed_connected_component components_iff) |
327 |
|
328 lemma compact_components: |
|
329 fixes s :: "'a::heine_borel set" |
|
330 shows "\<lbrakk>compact s; c \<in> components s\<rbrakk> \<Longrightarrow> compact c" |
|
331 by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed) |
|
332 |
321 |
333 lemma components_nonoverlap: |
322 lemma components_nonoverlap: |
334 "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c \<inter> c' = {}) \<longleftrightarrow> (c \<noteq> c')" |
323 "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c \<inter> c' = {}) \<longleftrightarrow> (c \<noteq> c')" |
335 apply (auto simp: in_components_nonempty components_iff) |
324 apply (auto simp: in_components_nonempty components_iff) |
336 using connected_component_refl apply blast |
325 using connected_component_refl apply blast |
720 } |
709 } |
721 with False show ?thesis |
710 with False show ?thesis |
722 unfolding constant_on_def by blast |
711 unfolding constant_on_def by blast |
723 qed |
712 qed |
724 |
713 |
725 lemma discrete_subset_disconnected: |
|
726 fixes S :: "'a::topological_space set" |
|
727 fixes t :: "'b::real_normed_vector set" |
|
728 assumes conf: "continuous_on S f" |
|
729 and no: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" |
|
730 shows "f ` S \<subseteq> {y. connected_component_set (f ` S) y = {y}}" |
|
731 proof - |
|
732 { fix x assume x: "x \<in> S" |
|
733 then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> S; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)" |
|
734 using conf no [OF x] by auto |
|
735 then have e2: "0 \<le> e / 2" |
|
736 by simp |
|
737 have "f y = f x" if "y \<in> S" and ccs: "f y \<in> connected_component_set (f ` S) (f x)" for y |
|
738 apply (rule ccontr) |
|
739 using connected_closed [of "connected_component_set (f ` S) (f x)"] \<open>e>0\<close> |
|
740 apply (simp add: del: ex_simps) |
|
741 apply (drule spec [where x="cball (f x) (e / 2)"]) |
|
742 apply (drule spec [where x="- ball(f x) e"]) |
|
743 apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in) |
|
744 apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less) |
|
745 using centre_in_cball connected_component_refl_eq e2 x apply blast |
|
746 using ccs |
|
747 apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> S\<close>]) |
|
748 done |
|
749 moreover have "connected_component_set (f ` S) (f x) \<subseteq> f ` S" |
|
750 by (auto simp: connected_component_in) |
|
751 ultimately have "connected_component_set (f ` S) (f x) = {f x}" |
|
752 by (auto simp: x) |
|
753 } |
|
754 with assms show ?thesis |
|
755 by blast |
|
756 qed |
|
757 |
714 |
758 text\<open>This proof requires the existence of two separate values of the range type.\<close> |
715 text\<open>This proof requires the existence of two separate values of the range type.\<close> |
759 lemma finite_range_constant_imp_connected: |
716 lemma finite_range_constant_imp_connected: |
760 assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
717 assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
761 \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> f constant_on S" |
718 \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> f constant_on S" |
779 } |
736 } |
780 then show ?thesis |
737 then show ?thesis |
781 by (simp add: connected_closedin_eq) |
738 by (simp add: connected_closedin_eq) |
782 qed |
739 qed |
783 |
740 |
784 lemma continuous_disconnected_range_constant_eq: |
|
785 "(connected S \<longleftrightarrow> |
|
786 (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
|
787 \<forall>t. continuous_on S f \<and> f ` S \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y}) |
|
788 \<longrightarrow> f constant_on S))" (is ?thesis1) |
|
789 and continuous_discrete_range_constant_eq: |
|
790 "(connected S \<longleftrightarrow> |
|
791 (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
|
792 continuous_on S f \<and> |
|
793 (\<forall>x \<in> S. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> S \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x))) |
|
794 \<longrightarrow> f constant_on S))" (is ?thesis2) |
|
795 and continuous_finite_range_constant_eq: |
|
796 "(connected S \<longleftrightarrow> |
|
797 (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
|
798 continuous_on S f \<and> finite (f ` S) |
|
799 \<longrightarrow> f constant_on S))" (is ?thesis3) |
|
800 proof - |
|
801 have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk> |
|
802 \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)" |
|
803 by blast |
|
804 have "?thesis1 \<and> ?thesis2 \<and> ?thesis3" |
|
805 apply (rule *) |
|
806 using continuous_disconnected_range_constant apply metis |
|
807 apply clarify |
|
808 apply (frule discrete_subset_disconnected; blast) |
|
809 apply (blast dest: finite_implies_discrete) |
|
810 apply (blast intro!: finite_range_constant_imp_connected) |
|
811 done |
|
812 then show ?thesis1 ?thesis2 ?thesis3 |
|
813 by blast+ |
|
814 qed |
|
815 |
|
816 lemma continuous_discrete_range_constant: |
|
817 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1" |
|
818 assumes S: "connected S" |
|
819 and "continuous_on S f" |
|
820 and "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" |
|
821 shows "f constant_on S" |
|
822 using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms by blast |
|
823 |
|
824 lemma continuous_finite_range_constant: |
|
825 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1" |
|
826 assumes "connected S" |
|
827 and "continuous_on S f" |
|
828 and "finite (f ` S)" |
|
829 shows "f constant_on S" |
|
830 using assms continuous_finite_range_constant_eq by blast |
|
831 |
|
832 end |
741 end |