4913 lemma continuous_on_real_range: |
4913 lemma continuous_on_real_range: |
4914 fixes f :: "'a::real_normed_vector \<Rightarrow> real" |
4914 fixes f :: "'a::real_normed_vector \<Rightarrow> real" |
4915 shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))" |
4915 shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))" |
4916 unfolding continuous_on_iff dist_norm by simp |
4916 unfolding continuous_on_iff dist_norm by simp |
4917 |
4917 |
|
4918 lemma compact_attains_sup: |
|
4919 fixes S :: "'a::linorder_topology set" |
|
4920 assumes "compact S" "S \<noteq> {}" |
|
4921 shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s" |
|
4922 proof (rule classical) |
|
4923 assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)" |
|
4924 then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s" |
|
4925 by (metis not_le) |
|
4926 then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})" |
|
4927 by auto |
|
4928 with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})" |
|
4929 by (erule compactE_image) |
|
4930 with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)" |
|
4931 by (auto intro!: Max_in) |
|
4932 with C have "S \<subseteq> {..< Max (t`C)}" |
|
4933 by (auto intro: less_le_trans simp: subset_eq) |
|
4934 with t Max `C \<subseteq> S` show ?thesis |
|
4935 by fastforce |
|
4936 qed |
|
4937 |
|
4938 lemma compact_attains_inf: |
|
4939 fixes S :: "'a::linorder_topology set" |
|
4940 assumes "compact S" "S \<noteq> {}" |
|
4941 shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t" |
|
4942 proof (rule classical) |
|
4943 assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)" |
|
4944 then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s" |
|
4945 by (metis not_le) |
|
4946 then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})" |
|
4947 by auto |
|
4948 with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})" |
|
4949 by (erule compactE_image) |
|
4950 with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s" |
|
4951 by (auto intro!: Min_in) |
|
4952 with C have "S \<subseteq> {Min (t`C) <..}" |
|
4953 by (auto intro: le_less_trans simp: subset_eq) |
|
4954 with t Min `C \<subseteq> S` show ?thesis |
|
4955 by fastforce |
|
4956 qed |
|
4957 |
|
4958 lemma continuous_attains_sup: |
|
4959 fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology" |
|
4960 shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f y \<le> f x)" |
|
4961 using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto |
|
4962 |
|
4963 lemma continuous_attains_inf: |
|
4964 fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology" |
|
4965 shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)" |
|
4966 using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto |
|
4967 |
4918 text {* Hence some handy theorems on distance, diameter etc. of/from a set. *} |
4968 text {* Hence some handy theorems on distance, diameter etc. of/from a set. *} |
4919 |
4969 |
4920 lemma compact_attains_sup: |
|
4921 fixes s :: "real set" |
|
4922 assumes "compact s" "s \<noteq> {}" |
|
4923 shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x" |
|
4924 proof- |
|
4925 from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto |
|
4926 { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s" "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e" |
|
4927 have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto |
|
4928 moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto |
|
4929 ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto } |
|
4930 thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]] |
|
4931 apply(rule_tac x="Sup s" in bexI) by auto |
|
4932 qed |
|
4933 |
4970 |
4934 lemma Inf: |
4971 lemma Inf: |
4935 fixes S :: "real set" |
4972 fixes S :: "real set" |
4936 shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)" |
4973 shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)" |
4937 by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) |
4974 by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) |
4938 |
|
4939 lemma compact_attains_inf: |
|
4940 fixes s :: "real set" |
|
4941 assumes "compact s" "s \<noteq> {}" shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y" |
|
4942 proof- |
|
4943 from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto |
|
4944 { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s" "Inf s \<notin> s" "0 < e" |
|
4945 "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e" |
|
4946 have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto |
|
4947 moreover |
|
4948 { fix x assume "x \<in> s" |
|
4949 hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto |
|
4950 have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto } |
|
4951 hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto |
|
4952 ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto } |
|
4953 thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]] |
|
4954 apply(rule_tac x="Inf s" in bexI) by auto |
|
4955 qed |
|
4956 |
|
4957 lemma continuous_attains_sup: |
|
4958 fixes f :: "'a::topological_space \<Rightarrow> real" |
|
4959 shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f |
|
4960 ==> (\<exists>x \<in> s. \<forall>y \<in> s. f y \<le> f x)" |
|
4961 using compact_attains_sup[of "f ` s"] |
|
4962 using compact_continuous_image[of s f] by auto |
|
4963 |
|
4964 lemma continuous_attains_inf: |
|
4965 fixes f :: "'a::topological_space \<Rightarrow> real" |
|
4966 shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f |
|
4967 \<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)" |
|
4968 using compact_attains_inf[of "f ` s"] |
|
4969 using compact_continuous_image[of s f] by auto |
|
4970 |
|
4971 lemma distance_attains_sup: |
4975 lemma distance_attains_sup: |
4972 assumes "compact s" "s \<noteq> {}" |
4976 assumes "compact s" "s \<noteq> {}" |
4973 shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a y \<le> dist a x" |
4977 shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a y \<le> dist a x" |
4974 proof (rule continuous_attains_sup [OF assms]) |
4978 proof (rule continuous_attains_sup [OF assms]) |
4975 { fix x assume "x\<in>s" |
4979 { fix x assume "x\<in>s" |