src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51345 e7dd577cb053
parent 51344 b3d246c92dfb
child 51346 d33de22432e2
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:15 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:16 2013 +0100
     1.3 @@ -4915,59 +4915,63 @@
     1.4    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))"
     1.5    unfolding continuous_on_iff dist_norm by simp
     1.6  
     1.7 +lemma compact_attains_sup:
     1.8 +  fixes S :: "'a::linorder_topology set"
     1.9 +  assumes "compact S" "S \<noteq> {}"
    1.10 +  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
    1.11 +proof (rule classical)
    1.12 +  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
    1.13 +  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
    1.14 +    by (metis not_le)
    1.15 +  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
    1.16 +    by auto
    1.17 +  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
    1.18 +    by (erule compactE_image)
    1.19 +  with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
    1.20 +    by (auto intro!: Max_in)
    1.21 +  with C have "S \<subseteq> {..< Max (t`C)}"
    1.22 +    by (auto intro: less_le_trans simp: subset_eq)
    1.23 +  with t Max `C \<subseteq> S` show ?thesis
    1.24 +    by fastforce
    1.25 +qed
    1.26 +
    1.27 +lemma compact_attains_inf:
    1.28 +  fixes S :: "'a::linorder_topology set"
    1.29 +  assumes "compact S" "S \<noteq> {}"
    1.30 +  shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t"
    1.31 +proof (rule classical)
    1.32 +  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
    1.33 +  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
    1.34 +    by (metis not_le)
    1.35 +  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
    1.36 +    by auto
    1.37 +  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
    1.38 +    by (erule compactE_image)
    1.39 +  with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
    1.40 +    by (auto intro!: Min_in)
    1.41 +  with C have "S \<subseteq> {Min (t`C) <..}"
    1.42 +    by (auto intro: le_less_trans simp: subset_eq)
    1.43 +  with t Min `C \<subseteq> S` show ?thesis
    1.44 +    by fastforce
    1.45 +qed
    1.46 +
    1.47 +lemma continuous_attains_sup:
    1.48 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
    1.49 +  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)"
    1.50 +  using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
    1.51 +
    1.52 +lemma continuous_attains_inf:
    1.53 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
    1.54 +  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)"
    1.55 +  using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
    1.56 +
    1.57  text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
    1.58  
    1.59 -lemma compact_attains_sup:
    1.60 -  fixes s :: "real set"
    1.61 -  assumes "compact s"  "s \<noteq> {}"
    1.62 -  shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
    1.63 -proof-
    1.64 -  from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
    1.65 -  { 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"
    1.66 -    have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
    1.67 -    moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
    1.68 -    ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto  }
    1.69 -  thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
    1.70 -    apply(rule_tac x="Sup s" in bexI) by auto
    1.71 -qed
    1.72  
    1.73  lemma Inf:
    1.74    fixes S :: "real set"
    1.75    shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
    1.76  by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
    1.77 -
    1.78 -lemma compact_attains_inf:
    1.79 -  fixes s :: "real set"
    1.80 -  assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
    1.81 -proof-
    1.82 -  from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
    1.83 -  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s"  "Inf s \<notin> s"  "0 < e"
    1.84 -      "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
    1.85 -    have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
    1.86 -    moreover
    1.87 -    { fix x assume "x \<in> s"
    1.88 -      hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
    1.89 -      have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
    1.90 -    hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
    1.91 -    ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto  }
    1.92 -  thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
    1.93 -    apply(rule_tac x="Inf s" in bexI) by auto
    1.94 -qed
    1.95 -
    1.96 -lemma continuous_attains_sup:
    1.97 -  fixes f :: "'a::topological_space \<Rightarrow> real"
    1.98 -  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
    1.99 -        ==> (\<exists>x \<in> s. \<forall>y \<in> s.  f y \<le> f x)"
   1.100 -  using compact_attains_sup[of "f ` s"]
   1.101 -  using compact_continuous_image[of s f] by auto
   1.102 -
   1.103 -lemma continuous_attains_inf:
   1.104 -  fixes f :: "'a::topological_space \<Rightarrow> real"
   1.105 -  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
   1.106 -        \<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
   1.107 -  using compact_attains_inf[of "f ` s"]
   1.108 -  using compact_continuous_image[of s f] by auto
   1.109 -
   1.110  lemma distance_attains_sup:
   1.111    assumes "compact s" "s \<noteq> {}"
   1.112    shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a y \<le> dist a x"