856 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" |
856 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" |
857 by (simp add: set_eq_iff) |
857 by (simp add: set_eq_iff) |
858 |
858 |
859 lemma cball_diff_eq_sphere: "cball a r - ball a r = {x. dist x a = r}" |
859 lemma cball_diff_eq_sphere: "cball a r - ball a r = {x. dist x a = r}" |
860 by (auto simp: cball_def ball_def dist_commute) |
860 by (auto simp: cball_def ball_def dist_commute) |
|
861 |
|
862 lemma image_add_ball [simp]: |
|
863 fixes a :: "'a::real_normed_vector" |
|
864 shows "op + b ` ball a r = ball (a+b) r" |
|
865 apply (intro equalityI subsetI) |
|
866 apply (force simp: dist_norm) |
|
867 apply (rule_tac x="x-b" in image_eqI) |
|
868 apply (auto simp: dist_norm algebra_simps) |
|
869 done |
|
870 |
|
871 lemma image_add_cball [simp]: |
|
872 fixes a :: "'a::real_normed_vector" |
|
873 shows "op + b ` cball a r = cball (a+b) r" |
|
874 apply (intro equalityI subsetI) |
|
875 apply (force simp: dist_norm) |
|
876 apply (rule_tac x="x-b" in image_eqI) |
|
877 apply (auto simp: dist_norm algebra_simps) |
|
878 done |
861 |
879 |
862 lemma open_ball [intro, simp]: "open (ball x e)" |
880 lemma open_ball [intro, simp]: "open (ball x e)" |
863 proof - |
881 proof - |
864 have "open (dist x -` {..<e})" |
882 have "open (dist x -` {..<e})" |
865 by (intro open_vimage open_lessThan continuous_intros) |
883 by (intro open_vimage open_lessThan continuous_intros) |
2189 |
2207 |
2190 subsection \<open>Frontier (aka boundary)\<close> |
2208 subsection \<open>Frontier (aka boundary)\<close> |
2191 |
2209 |
2192 definition "frontier S = closure S - interior S" |
2210 definition "frontier S = closure S - interior S" |
2193 |
2211 |
2194 lemma frontier_closed: "closed (frontier S)" |
2212 lemma frontier_closed [iff]: "closed (frontier S)" |
2195 by (simp add: frontier_def closed_Diff) |
2213 by (simp add: frontier_def closed_Diff) |
2196 |
2214 |
2197 lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))" |
2215 lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))" |
2198 by (auto simp add: frontier_def interior_closure) |
2216 by (auto simp add: frontier_def interior_closure) |
2199 |
2217 |
2200 lemma frontier_straddle: |
2218 lemma frontier_straddle: |
2201 fixes a :: "'a::metric_space" |
2219 fixes a :: "'a::metric_space" |
2202 shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" |
2220 shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" |
2203 unfolding frontier_def closure_interior |
2221 unfolding frontier_def closure_interior |
2204 by (auto simp add: mem_interior subset_eq ball_def) |
2222 by (auto simp add: mem_interior subset_eq ball_def) |
2205 |
2223 |
2206 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S" |
2224 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S" |
2207 by (metis frontier_def closure_closed Diff_subset) |
2225 by (metis frontier_def closure_closed Diff_subset) |
2208 |
2226 |
2209 lemma frontier_empty[simp]: "frontier {} = {}" |
2227 lemma frontier_empty [simp]: "frontier {} = {}" |
2210 by (simp add: frontier_def) |
2228 by (simp add: frontier_def) |
2211 |
2229 |
2212 lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S" |
2230 lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S" |
2213 proof - |
2231 proof - |
2214 { |
2232 { |
5888 hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def) |
5907 hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def) |
5889 thus ?thesis using U continuous_on_eq_continuous_at by auto |
5908 thus ?thesis using U continuous_on_eq_continuous_at by auto |
5890 qed |
5909 qed |
5891 qed |
5910 qed |
5892 |
5911 |
|
5912 subsection\<open> Theorems relating continuity and uniform continuity to closures\<close> |
|
5913 |
|
5914 lemma continuous_on_closure: |
|
5915 "continuous_on (closure S) f \<longleftrightarrow> |
|
5916 (\<forall>x e. x \<in> closure S \<and> 0 < e |
|
5917 \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))" |
|
5918 (is "?lhs = ?rhs") |
|
5919 proof |
|
5920 assume ?lhs then show ?rhs |
|
5921 unfolding continuous_on_iff by (metis Un_iff closure_def) |
|
5922 next |
|
5923 assume R [rule_format]: ?rhs |
|
5924 show ?lhs |
|
5925 proof |
|
5926 fix x and e::real |
|
5927 assume "0 < e" and x: "x \<in> closure S" |
|
5928 obtain \<delta>::real where "\<delta> > 0" |
|
5929 and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2" |
|
5930 using R [of x "e/2"] \<open>0 < e\<close> x by auto |
|
5931 have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y |
|
5932 proof - |
|
5933 obtain \<delta>'::real where "\<delta>' > 0" |
|
5934 and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2" |
|
5935 using R [of y "e/2"] \<open>0 < e\<close> y by auto |
|
5936 obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2" |
|
5937 using closure_approachable y |
|
5938 by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral) |
|
5939 have "dist (f z) (f y) < e/2" |
|
5940 apply (rule \<delta>' [OF \<open>z \<in> S\<close>]) |
|
5941 using z \<open>0 < \<delta>'\<close> by linarith |
|
5942 moreover have "dist (f z) (f x) < e/2" |
|
5943 apply (rule \<delta> [OF \<open>z \<in> S\<close>]) |
|
5944 using z \<open>0 < \<delta>\<close> dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto |
|
5945 ultimately show ?thesis |
|
5946 by (metis dist_commute dist_triangle_half_l less_imp_le) |
|
5947 qed |
|
5948 then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e" |
|
5949 by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>) |
|
5950 qed |
|
5951 qed |
|
5952 |
|
5953 lemma continuous_on_closure_sequentially: |
|
5954 fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space" |
|
5955 shows |
|
5956 "continuous_on (closure S) f \<longleftrightarrow> |
|
5957 (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)" |
|
5958 (is "?lhs = ?rhs") |
|
5959 proof - |
|
5960 have "continuous_on (closure S) f \<longleftrightarrow> |
|
5961 (\<forall>x \<in> closure S. continuous (at x within S) f)" |
|
5962 by (force simp: continuous_on_closure Topology_Euclidean_Space.continuous_within_eps_delta) |
|
5963 also have "... = ?rhs" |
|
5964 by (force simp: continuous_within_sequentially) |
|
5965 finally show ?thesis . |
|
5966 qed |
|
5967 |
|
5968 lemma uniformly_continuous_on_closure: |
|
5969 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
|
5970 assumes ucont: "uniformly_continuous_on S f" |
|
5971 and cont: "continuous_on (closure S) f" |
|
5972 shows "uniformly_continuous_on (closure S) f" |
|
5973 unfolding uniformly_continuous_on_def |
|
5974 proof (intro allI impI) |
|
5975 fix e::real |
|
5976 assume "0 < e" |
|
5977 then obtain d::real |
|
5978 where "d>0" |
|
5979 and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3" |
|
5980 using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto |
|
5981 show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" |
|
5982 proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>) |
|
5983 fix x y |
|
5984 assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d" |
|
5985 obtain d1::real where "d1 > 0" |
|
5986 and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3" |
|
5987 using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto |
|
5988 obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)" |
|
5989 using closure_approachable [of x S] |
|
5990 by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral) |
|
5991 obtain d2::real where "d2 > 0" |
|
5992 and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3" |
|
5993 using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto |
|
5994 obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)" |
|
5995 using closure_approachable [of y S] |
|
5996 by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral) |
|
5997 have "dist x' x < d/3" using x' by auto |
|
5998 moreover have "dist x y < d/3" |
|
5999 by (metis dist_commute dyx less_divide_eq_numeral1(1)) |
|
6000 moreover have "dist y y' < d/3" |
|
6001 by (metis (no_types) dist_commute min_less_iff_conj y') |
|
6002 ultimately have "dist x' y' < d/3 + d/3 + d/3" |
|
6003 by (meson dist_commute_lessI dist_triangle_lt add_strict_mono) |
|
6004 then have "dist x' y' < d" by simp |
|
6005 then have "dist (f x') (f y') < e/3" |
|
6006 by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>]) |
|
6007 moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1 |
|
6008 by (simp add: closure_def) |
|
6009 moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2 |
|
6010 by (simp add: closure_def) |
|
6011 ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3" |
|
6012 by (meson dist_commute_lessI dist_triangle_lt add_strict_mono) |
|
6013 then show "dist (f y) (f x) < e" by simp |
|
6014 qed |
|
6015 qed |
|
6016 |
5893 subsection \<open>A function constant on a set\<close> |
6017 subsection \<open>A function constant on a set\<close> |
5894 |
6018 |
5895 definition constant_on (infixl "(constant'_on)" 50) |
6019 definition constant_on (infixl "(constant'_on)" 50) |
5896 where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y" |
6020 where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y" |
5897 |
6021 |
6383 from assms obtain b where "b \<in> s" by auto |
6507 from assms obtain b where "b \<in> s" by auto |
6384 let ?B = "s \<inter> cball a (dist b a)" |
6508 let ?B = "s \<inter> cball a (dist b a)" |
6385 have "?B \<noteq> {}" using \<open>b \<in> s\<close> |
6509 have "?B \<noteq> {}" using \<open>b \<in> s\<close> |
6386 by (auto simp: dist_commute) |
6510 by (auto simp: dist_commute) |
6387 moreover have "continuous_on ?B (dist a)" |
6511 moreover have "continuous_on ?B (dist a)" |
6388 by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const) |
6512 by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const) |
6389 moreover have "compact ?B" |
6513 moreover have "compact ?B" |
6390 by (intro closed_inter_compact \<open>closed s\<close> compact_cball) |
6514 by (intro closed_inter_compact \<open>closed s\<close> compact_cball) |
6391 ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y" |
6515 ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y" |
6392 by (metis continuous_attains_inf) |
6516 by (metis continuous_attains_inf) |
6393 with that show ?thesis by fastforce |
6517 with that show ?thesis by fastforce |
6826 proof cases |
6950 proof cases |
6827 assume "s \<noteq> {} \<and> t \<noteq> {}" |
6951 assume "s \<noteq> {} \<and> t \<noteq> {}" |
6828 then have "s \<noteq> {}" "t \<noteq> {}" by auto |
6952 then have "s \<noteq> {}" "t \<noteq> {}" by auto |
6829 let ?inf = "\<lambda>x. infdist x t" |
6953 let ?inf = "\<lambda>x. infdist x t" |
6830 have "continuous_on s ?inf" |
6954 have "continuous_on s ?inf" |
6831 by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_at_id) |
6955 by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident) |
6832 then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y" |
6956 then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y" |
6833 using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto |
6957 using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto |
6834 then have "0 < ?inf x" |
6958 then have "0 < ?inf x" |
6835 using t \<open>t \<noteq> {}\<close> in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg) |
6959 using t \<open>t \<noteq> {}\<close> in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg) |
6836 moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y" |
6960 moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y" |
8342 shows "\<exists>!x\<in>s. g x = x" |
8466 shows "\<exists>!x\<in>s. g x = x" |
8343 proof - |
8467 proof - |
8344 let ?D = "(\<lambda>x. (x, x)) ` s" |
8468 let ?D = "(\<lambda>x. (x, x)) ` s" |
8345 have D: "compact ?D" "?D \<noteq> {}" |
8469 have D: "compact ?D" "?D \<noteq> {}" |
8346 by (rule compact_continuous_image) |
8470 by (rule compact_continuous_image) |
8347 (auto intro!: s continuous_Pair continuous_within_id simp: continuous_on_eq_continuous_within) |
8471 (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within) |
8348 |
8472 |
8349 have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e" |
8473 have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e" |
8350 using dist by fastforce |
8474 using dist by fastforce |
8351 then have "continuous_on s g" |
8475 then have "continuous_on s g" |
8352 unfolding continuous_on_iff by auto |
8476 unfolding continuous_on_iff by auto |
8353 then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))" |
8477 then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))" |
8354 unfolding continuous_on_eq_continuous_within |
8478 unfolding continuous_on_eq_continuous_within |
8355 by (intro continuous_dist ballI continuous_within_compose) |
8479 by (intro continuous_dist ballI continuous_within_compose) |
8356 (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image) |
8480 (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image) |
8357 |
8481 |
8358 obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x" |
8482 obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x" |
8359 using continuous_attains_inf[OF D cont] by auto |
8483 using continuous_attains_inf[OF D cont] by auto |
8360 |
8484 |
8361 have "g a = a" |
8485 have "g a = a" |