src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 66793 deabce3ccf1f
parent 66643 f7e38b8583a0
child 66794 83bf64da6938
equal deleted inserted replaced
66792:6b76a5d1b7a5 66793:deabce3ccf1f
   673   have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
   673   have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
   674     using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
   674     using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
   675   then show ?thesis
   675   then show ?thesis
   676     using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
   676     using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
   677 qed
   677 qed
       
   678 
       
   679 lemma openin_Inter [intro]:
       
   680   assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
       
   681   by (metis (full_types) assms openin_INT2 image_ident)
   678 
   682 
   679 
   683 
   680 subsubsection \<open>Closed sets\<close>
   684 subsubsection \<open>Closed sets\<close>
   681 
   685 
   682 definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
   686 definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
  2401   apply (force simp: closure_def)
  2405   apply (force simp: closure_def)
  2402   done
  2406   done
  2403 
  2407 
  2404 lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
  2408 lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
  2405   by (meson closedin_limpt closed_subset closedin_closed_trans)
  2409   by (meson closedin_limpt closed_subset closedin_closed_trans)
       
  2410 
       
  2411 lemma connected_closed_set:
       
  2412    "closed S
       
  2413     \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
       
  2414   unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
  2406 
  2415 
  2407 lemma closedin_subset_trans:
  2416 lemma closedin_subset_trans:
  2408   "closedin (subtopology euclidean U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
  2417   "closedin (subtopology euclidean U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
  2409     closedin (subtopology euclidean T) S"
  2418     closedin (subtopology euclidean T) S"
  2410   by (meson closedin_limpt subset_iff)
  2419   by (meson closedin_limpt subset_iff)
  5404   then show ?lhs
  5413   then show ?lhs
  5405     using bounded_closed_imp_seq_compact[of s]
  5414     using bounded_closed_imp_seq_compact[of s]
  5406     unfolding compact_eq_seq_compact_metric
  5415     unfolding compact_eq_seq_compact_metric
  5407     by auto
  5416     by auto
  5408 qed
  5417 qed
       
  5418 
       
  5419 lemma compact_Inter:
       
  5420   fixes \<F> :: "'a :: heine_borel set set"
       
  5421   assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"
       
  5422   shows "compact(\<Inter> \<F>)"
       
  5423   using assms
       
  5424   by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)
  5409 
  5425 
  5410 lemma compact_closure [simp]:
  5426 lemma compact_closure [simp]:
  5411   fixes S :: "'a::heine_borel set"
  5427   fixes S :: "'a::heine_borel set"
  5412   shows "compact(closure S) \<longleftrightarrow> bounded S"
  5428   shows "compact(closure S) \<longleftrightarrow> bounded S"
  5413 by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
  5429 by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
  5817       unfolding lim_sequentially by auto
  5833       unfolding lim_sequentially by auto
  5818   }
  5834   }
  5819   then show ?thesis unfolding complete_def by auto
  5835   then show ?thesis unfolding complete_def by auto
  5820 qed
  5836 qed
  5821 
  5837 
  5822 lemma nat_approx_posE:
       
  5823   fixes e::real
       
  5824   assumes "0 < e"
       
  5825   obtains n :: nat where "1 / (Suc n) < e"
       
  5826 proof atomize_elim
       
  5827   have "1 / real (Suc (nat \<lceil>1/e\<rceil>)) < 1 / \<lceil>1/e\<rceil>"
       
  5828     by (rule divide_strict_left_mono) (auto simp: \<open>0 < e\<close>)
       
  5829   also have "1 / \<lceil>1/e\<rceil> \<le> 1 / (1/e)"
       
  5830     by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
       
  5831   also have "\<dots> = e" by simp
       
  5832   finally show  "\<exists>n. 1 / real (Suc n) < e" ..
       
  5833 qed
       
  5834 
       
  5835 lemma compact_eq_totally_bounded:
  5838 lemma compact_eq_totally_bounded:
  5836   "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
  5839   "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
  5837     (is "_ \<longleftrightarrow> ?rhs")
  5840     (is "_ \<longleftrightarrow> ?rhs")
  5838 proof
  5841 proof
  5839   assume assms: "?rhs"
  5842   assume assms: "?rhs"
  9677     using assms
  9680     using assms
  9678     apply (auto intro!: continuous_intros
  9681     apply (auto intro!: continuous_intros
  9679       simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
  9682       simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
  9680     done
  9683     done
  9681 
  9684 
       
  9685 lemma homeomorphic_ball01_UNIV:
       
  9686   "ball (0::'a::real_normed_vector) 1 homeomorphic (UNIV:: 'a set)"
       
  9687   (is "?B homeomorphic ?U")
       
  9688 proof
       
  9689   have "x \<in> (\<lambda>z. z /\<^sub>R (1 - norm z)) ` ball 0 1" for x::'a
       
  9690     apply (rule_tac x="x /\<^sub>R (1 + norm x)" in image_eqI)
       
  9691      apply (auto simp: divide_simps)
       
  9692     using norm_ge_zero [of x] apply linarith+
       
  9693     done
       
  9694   then show "(\<lambda>z::'a. z /\<^sub>R (1 - norm z)) ` ?B = ?U"
       
  9695     by blast
       
  9696   have "x \<in> range (\<lambda>z. (1 / (1 + norm z)) *\<^sub>R z)" if "norm x < 1" for x::'a
       
  9697     apply (rule_tac x="x /\<^sub>R (1 - norm x)" in image_eqI)
       
  9698     using that apply (auto simp: divide_simps)
       
  9699     done
       
  9700   then show "(\<lambda>z::'a. z /\<^sub>R (1 + norm z)) ` ?U = ?B"
       
  9701     by (force simp: divide_simps dest: add_less_zeroD)
       
  9702   show "continuous_on (ball 0 1) (\<lambda>z. z /\<^sub>R (1 - norm z))"
       
  9703     by (rule continuous_intros | force)+
       
  9704   show "continuous_on UNIV (\<lambda>z. z /\<^sub>R (1 + norm z))"
       
  9705     apply (intro continuous_intros)
       
  9706     apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
       
  9707     done
       
  9708   show "\<And>x. x \<in> ball 0 1 \<Longrightarrow>
       
  9709          x /\<^sub>R (1 - norm x) /\<^sub>R (1 + norm (x /\<^sub>R (1 - norm x))) = x"
       
  9710     by (auto simp: divide_simps)
       
  9711   show "\<And>y. y /\<^sub>R (1 + norm y) /\<^sub>R (1 - norm (y /\<^sub>R (1 + norm y))) = y"
       
  9712     apply (auto simp: divide_simps)
       
  9713     apply (metis le_add_same_cancel1 norm_ge_zero not_le zero_less_one)
       
  9714     done
       
  9715 qed
       
  9716 
       
  9717 proposition homeomorphic_ball_UNIV:
       
  9718   fixes a ::"'a::real_normed_vector"
       
  9719   assumes "0 < r" shows "ball a r homeomorphic (UNIV:: 'a set)"
       
  9720   using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
       
  9721 
  9682 subsection\<open>Inverse function property for open/closed maps\<close>
  9722 subsection\<open>Inverse function property for open/closed maps\<close>
  9683 
  9723 
  9684 lemma continuous_on_inverse_open_map:
  9724 lemma continuous_on_inverse_open_map:
  9685   assumes contf: "continuous_on S f"
  9725   assumes contf: "continuous_on S f"
  9686     and imf: "f ` S = T"
  9726     and imf: "f ` S = T"
 10709      apply (simp add: clof)
 10749      apply (simp add: clof)
 10710     by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
 10750     by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
 10711   then show ?thesis by blast
 10751   then show ?thesis by blast
 10712 qed
 10752 qed
 10713 
 10753 
 10714 lemma closed_imp_fip_compact:
 10754 lemma clconnected_closedin_eqosed_imp_fip_compact:
 10715   fixes S :: "'a::heine_borel set"
 10755   fixes S :: "'a::heine_borel set"
 10716   shows
 10756   shows
 10717    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
 10757    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
 10718      \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
 10758      \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
 10719         \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
 10759         \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
 11041 subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
 11081 subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
 11042 
 11082 
 11043 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
 11083 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
 11044 
 11084 
 11045 lemma continuous_disconnected_range_constant:
 11085 lemma continuous_disconnected_range_constant:
 11046   assumes s: "connected s"
 11086   assumes S: "connected S"
 11047       and conf: "continuous_on s f"
 11087       and conf: "continuous_on S f"
 11048       and fim: "f ` s \<subseteq> t"
 11088       and fim: "f ` S \<subseteq> t"
 11049       and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
 11089       and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
 11050     shows "\<exists>a. \<forall>x \<in> s. f x = a"
 11090     shows "\<exists>a. \<forall>x \<in> S. f x = a"
 11051 proof (cases "s = {}")
 11091 proof (cases "S = {}")
 11052   case True then show ?thesis by force
 11092   case True then show ?thesis by force
 11053 next
 11093 next
 11054   case False
 11094   case False
 11055   { fix x assume "x \<in> s"
 11095   { fix x assume "x \<in> S"
 11056     then have "f ` s \<subseteq> {f x}"
 11096     then have "f ` S \<subseteq> {f x}"
 11057     by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
 11097     by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
 11058   }
 11098   }
 11059   with False show ?thesis
 11099   with False show ?thesis
 11060     by blast
 11100     by blast
 11061 qed
 11101 qed
 11062 
 11102 
 11063 lemma discrete_subset_disconnected:
 11103 lemma discrete_subset_disconnected:
 11064   fixes s :: "'a::topological_space set"
 11104   fixes S :: "'a::topological_space set"
 11065   fixes t :: "'b::real_normed_vector set"
 11105   fixes t :: "'b::real_normed_vector set"
 11066   assumes conf: "continuous_on s f"
 11106   assumes conf: "continuous_on S f"
 11067       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)"
 11107       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)"
 11068    shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
 11108    shows "f ` S \<subseteq> {y. connected_component_set (f ` S) y = {y}}"
 11069 proof -
 11109 proof -
 11070   { fix x assume x: "x \<in> s"
 11110   { fix x assume x: "x \<in> S"
 11071     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)"
 11111     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)"
 11072       using conf no [OF x] by auto
 11112       using conf no [OF x] by auto
 11073     then have e2: "0 \<le> e / 2"
 11113     then have e2: "0 \<le> e / 2"
 11074       by simp
 11114       by simp
 11075     have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
 11115     have "f y = f x" if "y \<in> S" and ccs: "f y \<in> connected_component_set (f ` S) (f x)" for y
 11076       apply (rule ccontr)
 11116       apply (rule ccontr)
 11077       using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
 11117       using connected_closed [of "connected_component_set (f ` S) (f x)"] \<open>e>0\<close>
 11078       apply (simp add: del: ex_simps)
 11118       apply (simp add: del: ex_simps)
 11079       apply (drule spec [where x="cball (f x) (e / 2)"])
 11119       apply (drule spec [where x="cball (f x) (e / 2)"])
 11080       apply (drule spec [where x="- ball(f x) e"])
 11120       apply (drule spec [where x="- ball(f x) e"])
 11081       apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
 11121       apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
 11082         apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
 11122         apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
 11083        using centre_in_cball connected_component_refl_eq e2 x apply blast
 11123        using centre_in_cball connected_component_refl_eq e2 x apply blast
 11084       using ccs
 11124       using ccs
 11085       apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
 11125       apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> S\<close>])
 11086       done
 11126       done
 11087     moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
 11127     moreover have "connected_component_set (f ` S) (f x) \<subseteq> f ` S"
 11088       by (auto simp: connected_component_in)
 11128       by (auto simp: connected_component_in)
 11089     ultimately have "connected_component_set (f ` s) (f x) = {f x}"
 11129     ultimately have "connected_component_set (f ` S) (f x) = {f x}"
 11090       by (auto simp: x)
 11130       by (auto simp: x)
 11091   }
 11131   }
 11092   with assms show ?thesis
 11132   with assms show ?thesis
 11093     by blast
 11133     by blast
 11094 qed
 11134 qed
 11095 
 11135 
 11096 lemma finite_implies_discrete:
 11136 lemma finite_implies_discrete:
 11097   fixes s :: "'a::topological_space set"
 11137   fixes S :: "'a::topological_space set"
 11098   assumes "finite (f ` s)"
 11138   assumes "finite (f ` S)"
 11099   shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
 11139   shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
 11100 proof -
 11140 proof -
 11101   have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
 11141   have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
 11102   proof (cases "f ` s - {f x} = {}")
 11142   proof (cases "f ` S - {f x} = {}")
 11103     case True
 11143     case True
 11104     with zero_less_numeral show ?thesis
 11144     with zero_less_numeral show ?thesis
 11105       by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
 11145       by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
 11106   next
 11146   next
 11107     case False
 11147     case False
 11108     then obtain z where z: "z \<in> s" "f z \<noteq> f x"
 11148     then obtain z where z: "z \<in> S" "f z \<noteq> f x"
 11109       by blast
 11149       by blast
 11110     have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
 11150     have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
 11111       using assms by simp
 11151       using assms by simp
 11112     then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
 11152     then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
 11113       apply (rule finite_imp_less_Inf)
 11153       apply (rule finite_imp_less_Inf)
 11114       using z apply force+
 11154       using z apply force+
 11115       done
 11155       done
 11116     show ?thesis
 11156     show ?thesis
 11117       by (force intro!: * cInf_le_finite [OF finn])
 11157       by (force intro!: * cInf_le_finite [OF finn])
 11121 qed
 11161 qed
 11122 
 11162 
 11123 text\<open>This proof requires the existence of two separate values of the range type.\<close>
 11163 text\<open>This proof requires the existence of two separate values of the range type.\<close>
 11124 lemma finite_range_constant_imp_connected:
 11164 lemma finite_range_constant_imp_connected:
 11125   assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
 11165   assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
 11126               \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
 11166               \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
 11127     shows "connected s"
 11167     shows "connected S"
 11128 proof -
 11168 proof -
 11129   { fix t u
 11169   { fix t u
 11130     assume clt: "closedin (subtopology euclidean s) t"
 11170     assume clt: "closedin (subtopology euclidean S) t"
 11131        and clu: "closedin (subtopology euclidean s) u"
 11171        and clu: "closedin (subtopology euclidean S) u"
 11132        and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
 11172        and tue: "t \<inter> u = {}" and tus: "t \<union> u = S"
 11133     have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
 11173     have conif: "continuous_on S (\<lambda>x. if x \<in> t then 0 else 1)"
 11134       apply (subst tus [symmetric])
 11174       apply (subst tus [symmetric])
 11135       apply (rule continuous_on_cases_local)
 11175       apply (rule continuous_on_cases_local)
 11136       using clt clu tue
 11176       using clt clu tue
 11137       apply (auto simp: tus continuous_on_const)
 11177       apply (auto simp: tus continuous_on_const)
 11138       done
 11178       done
 11139     have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
 11179     have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
 11140       by (rule finite_subset [of _ "{0,1}"]) auto
 11180       by (rule finite_subset [of _ "{0,1}"]) auto
 11141     have "t = {} \<or> u = {}"
 11181     have "t = {} \<or> u = {}"
 11142       using assms [OF conif fi] tus [symmetric]
 11182       using assms [OF conif fi] tus [symmetric]
 11143       by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
 11183       by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
 11144   }
 11184   }