summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 18 Jan 2018 17:04:35 +0100 | |

changeset 67455 | fe6bcf0137b4 |

parent 67454 | 867d7e91af65 |

child 67456 | 7895c159d7b1 |

moved from AFP/Gromov

--- a/src/HOL/Analysis/Connected.thy Thu Jan 18 15:21:06 2018 +0100 +++ b/src/HOL/Analysis/Connected.thy Thu Jan 18 17:04:35 2018 +0100 @@ -1396,6 +1396,58 @@ with assms show ?thesis by simp qed +lemma infdist_pos_not_in_closed: + assumes "closed S" "S \<noteq> {}" "x \<notin> S" + shows "infdist x S > 0" +using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce + +text \<open>Every metric space is a T4 space:\<close> + +instance metric_space \<subseteq> t4_space +proof + fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}" + consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto + then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}" + proof (cases) + case 1 + show ?thesis + apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto + next + case 2 + show ?thesis + apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto + next + case 3 + define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))" + have A: "open U" unfolding U_def by auto + have "infdist x T > 0" if "x \<in> S" for x + using H that 3 by (auto intro!: infdist_pos_not_in_closed) + then have B: "S \<subseteq> U" unfolding U_def by auto + define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))" + have C: "open V" unfolding V_def by auto + have "infdist x S > 0" if "x \<in> T" for x + using H that 3 by (auto intro!: infdist_pos_not_in_closed) + then have D: "T \<subseteq> V" unfolding V_def by auto + + have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y + proof (auto) + fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S" + have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z" + using dist_triangle[of x y z] by (auto simp add: dist_commute) + also have "... < infdist x T + infdist y S" + using H by auto + finally have "dist x y < infdist x T \<or> dist x y < infdist y S" + by auto + then show False + using infdist_le[OF \<open>x \<in> S\<close>, of y] infdist_le[OF \<open>y \<in> T\<close>, of x] by (auto simp add: dist_commute) + qed + then have E: "U \<inter> V = {}" + unfolding U_def V_def by auto + show ?thesis + apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto + qed +qed + lemma tendsto_infdist [tendsto_intros]: assumes f: "(f \<longlongrightarrow> l) F" shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"