src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 54260 6a967667fd45
parent 54259 71c701dc5bf9
child 54263 c4159fe6fa46
equal deleted inserted replaced
54259:71c701dc5bf9 54260:6a967667fd45
  1970 qed
  1970 qed
  1971 
  1971 
  1972 
  1972 
  1973 subsection {* Infimum Distance *}
  1973 subsection {* Infimum Distance *}
  1974 
  1974 
  1975 definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
  1975 definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
  1976 
  1976 
  1977 lemma bdd_below_infdist[intro, simp]: "bdd_below {dist x a|a. a \<in> A}"
  1977 lemma bdd_below_infdist[intro, simp]: "bdd_below (dist x`A)"
  1978   by (auto intro!: zero_le_dist)
  1978   by (auto intro!: zero_le_dist)
  1979 
  1979 
  1980 lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
  1980 lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"
  1981   by (simp add: infdist_def)
  1981   by (simp add: infdist_def)
  1982 
  1982 
  1983 lemma infdist_nonneg: "0 \<le> infdist x A"
  1983 lemma infdist_nonneg: "0 \<le> infdist x A"
  1984   by (auto simp add: infdist_def intro: cInf_greatest)
  1984   by (auto simp add: infdist_def intro: cINF_greatest)
  1985 
  1985 
  1986 lemma infdist_le: "a \<in> A \<Longrightarrow> d = dist x a \<Longrightarrow> infdist x A \<le> d"
  1986 lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
  1987   using assms by (auto intro: cInf_lower simp add: infdist_def)
  1987   by (auto intro: cINF_lower simp add: infdist_def)
       
  1988 
       
  1989 lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
       
  1990   by (auto intro!: cINF_lower2 simp add: infdist_def)
  1988 
  1991 
  1989 lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
  1992 lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
  1990   by (auto intro!: antisym infdist_nonneg infdist_le)
  1993   by (auto intro!: antisym infdist_nonneg infdist_le2)
  1991 
  1994 
  1992 lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
  1995 lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
  1993 proof (cases "A = {}")
  1996 proof (cases "A = {}")
  1994   case True
  1997   case True
  1995   then show ?thesis by (simp add: infdist_def)
  1998   then show ?thesis by (simp add: infdist_def)
  2004     assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
  2007     assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
  2005     then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
  2008     then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
  2006       by auto
  2009       by auto
  2007     show "infdist x A \<le> d"
  2010     show "infdist x A \<le> d"
  2008       unfolding infdist_notempty[OF `A \<noteq> {}`]
  2011       unfolding infdist_notempty[OF `A \<noteq> {}`]
  2009     proof (rule cInf_lower2)
  2012     proof (rule cINF_lower2)
  2010       show "dist x a \<in> {dist x a |a. a \<in> A}"
  2013       show "a \<in> A" by fact
  2011         using `a \<in> A` by auto
       
  2012       show "dist x a \<le> d"
  2014       show "dist x a \<le> d"
  2013         unfolding d by (rule dist_triangle)
  2015         unfolding d by (rule dist_triangle)
  2014     qed simp
  2016     qed simp
  2015   qed
  2017   qed
  2016   also have "\<dots> = dist x y + infdist y A"
  2018   also have "\<dots> = dist x y + infdist y A"
  2022   next
  2024   next
  2023     fix i
  2025     fix i
  2024     assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
  2026     assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
  2025     then have "i - dist x y \<le> infdist y A"
  2027     then have "i - dist x y \<le> infdist y A"
  2026       unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
  2028       unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
  2027       by (intro cInf_greatest) (auto simp: field_simps)
  2029       by (intro cINF_greatest) (auto simp: field_simps)
  2028     then show "i \<le> dist x y + infdist y A"
  2030     then show "i \<le> dist x y + infdist y A"
  2029       by simp
  2031       by simp
  2030   qed
  2032   qed
  2031   finally show ?thesis by simp
  2033   finally show ?thesis by simp
  2032 qed
  2034 qed
  2061     fix e :: real
  2063     fix e :: real
  2062     assume "e > 0"
  2064     assume "e > 0"
  2063     assume "\<not> (\<exists>y\<in>A. dist y x < e)"
  2065     assume "\<not> (\<exists>y\<in>A. dist y x < e)"
  2064     then have "infdist x A \<ge> e" using `a \<in> A`
  2066     then have "infdist x A \<ge> e" using `a \<in> A`
  2065       unfolding infdist_def
  2067       unfolding infdist_def
  2066       by (force simp: dist_commute intro: cInf_greatest)
  2068       by (force simp: dist_commute intro: cINF_greatest)
  2067     with x `e > 0` show False by auto
  2069     with x `e > 0` show False by auto
  2068   qed
  2070   qed
  2069 qed
  2071 qed
  2070 
  2072 
  2071 lemma in_closed_iff_infdist_zero:
  2073 lemma in_closed_iff_infdist_zero:
  5699     using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
  5701     using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
  5700 qed
  5702 qed
  5701 
  5703 
  5702 text {* We can state this in terms of diameter of a set. *}
  5704 text {* We can state this in terms of diameter of a set. *}
  5703 
  5705 
  5704 definition "diameter s = (if s = {} then 0::real else Sup {dist x y | x y. x \<in> s \<and> y \<in> s})"
  5706 definition diameter :: "'a::metric_space set \<Rightarrow> real" where
       
  5707   "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
  5705 
  5708 
  5706 lemma diameter_bounded_bound:
  5709 lemma diameter_bounded_bound:
  5707   fixes s :: "'a :: metric_space set"
  5710   fixes s :: "'a :: metric_space set"
  5708   assumes s: "bounded s" "x \<in> s" "y \<in> s"
  5711   assumes s: "bounded s" "x \<in> s" "y \<in> s"
  5709   shows "dist x y \<le> diameter s"
  5712   shows "dist x y \<le> diameter s"
  5710 proof -
  5713 proof -
  5711   let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
       
  5712   from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
  5714   from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
  5713     unfolding bounded_def by auto
  5715     unfolding bounded_def by auto
  5714   have "dist x y \<le> Sup ?D"
  5716   have "bdd_above (split dist ` (s\<times>s))"
  5715   proof (rule cSup_upper)
  5717   proof (intro bdd_aboveI, safe)
  5716     show "bdd_above ?D"
  5718     fix a b
  5717       unfolding bdd_above_def
  5719     assume "a \<in> s" "b \<in> s"
  5718     proof (safe intro!: exI)
  5720     with z[of a] z[of b] dist_triangle[of a b z]
  5719       fix a b
  5721     show "dist a b \<le> 2 * d"
  5720       assume "a \<in> s" "b \<in> s"
  5722       by (simp add: dist_commute)
  5721       with z[of a] z[of b] dist_triangle[of a b z]
  5723   qed
  5722       show "dist a b \<le> 2 * d"
  5724   moreover have "(x,y) \<in> s\<times>s" using s by auto
  5723         by (simp add: dist_commute)
  5725   ultimately have "dist x y \<le> (SUP (x,y):s\<times>s. dist x y)"
  5724     qed
  5726     by (rule cSUP_upper2) simp
  5725   qed (insert s, auto)
       
  5726   with `x \<in> s` show ?thesis
  5727   with `x \<in> s` show ?thesis
  5727     by (auto simp add: diameter_def)
  5728     by (auto simp add: diameter_def)
  5728 qed
  5729 qed
  5729 
  5730 
  5730 lemma diameter_lower_bounded:
  5731 lemma diameter_lower_bounded:
  5731   fixes s :: "'a :: metric_space set"
  5732   fixes s :: "'a :: metric_space set"
  5732   assumes s: "bounded s"
  5733   assumes s: "bounded s"
  5733     and d: "0 < d" "d < diameter s"
  5734     and d: "0 < d" "d < diameter s"
  5734   shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
  5735   shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
  5735 proof (rule ccontr)
  5736 proof (rule ccontr)
  5736   let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
       
  5737   assume contr: "\<not> ?thesis"
  5737   assume contr: "\<not> ?thesis"
  5738   moreover
  5738   moreover have "s \<noteq> {}"
  5739   from d have "s \<noteq> {}"
  5739     using d by (auto simp add: diameter_def)
  5740     by (auto simp: diameter_def)
  5740   ultimately have "diameter s \<le> d"
  5741   then have "?D \<noteq> {}" by auto
  5741     by (auto simp: not_less diameter_def intro!: cSUP_least)
  5742   ultimately have "Sup ?D \<le> d"
  5742   with `d < diameter s` show False by auto
  5743     by (intro cSup_least) (auto simp: not_less)
       
  5744   with `d < diameter s` `s \<noteq> {}` show False
       
  5745     by (auto simp: diameter_def)
       
  5746 qed
  5743 qed
  5747 
  5744 
  5748 lemma diameter_bounded:
  5745 lemma diameter_bounded:
  5749   assumes "bounded s"
  5746   assumes "bounded s"
  5750   shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
  5747   shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
  5763     and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
  5760     and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
  5764     using compact_sup_maxdistance[OF assms] by auto
  5761     using compact_sup_maxdistance[OF assms] by auto
  5765   then have "diameter s \<le> dist x y"
  5762   then have "diameter s \<le> dist x y"
  5766     unfolding diameter_def
  5763     unfolding diameter_def
  5767     apply clarsimp
  5764     apply clarsimp
  5768     apply (rule cSup_least)
  5765     apply (rule cSUP_least)
  5769     apply fast+
  5766     apply fast+
  5770     done
  5767     done
  5771   then show ?thesis
  5768   then show ?thesis
  5772     by (metis b diameter_bounded_bound order_antisym xys)
  5769     by (metis b diameter_bounded_bound order_antisym xys)
  5773 qed
  5770 qed