src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 54260 6a967667fd45 parent 54259 71c701dc5bf9 child 54263 c4159fe6fa46
equal 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 -`
`  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)`
`  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`