2066 done |
2066 done |
2067 |
2067 |
2068 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" |
2068 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" |
2069 by (auto simp: islimpt_def) |
2069 by (auto simp: islimpt_def) |
2070 |
2070 |
|
2071 lemma finite_ball_include: |
|
2072 fixes a :: "'a::metric_space" |
|
2073 assumes "finite S" |
|
2074 shows "\<exists>e>0. S \<subseteq> ball a e" |
|
2075 using assms |
|
2076 proof induction |
|
2077 case (insert x S) |
|
2078 then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto |
|
2079 define e where "e = max e0 (2 * dist a x)" |
|
2080 have "e>0" unfolding e_def using \<open>e0>0\<close> by auto |
|
2081 moreover have "insert x S \<subseteq> ball a e" |
|
2082 using e0 \<open>e>0\<close> unfolding e_def by auto |
|
2083 ultimately show ?case by auto |
|
2084 qed (auto intro: zero_less_one) |
|
2085 |
2071 lemma finite_set_avoid: |
2086 lemma finite_set_avoid: |
2072 fixes a :: "'a::metric_space" |
2087 fixes a :: "'a::metric_space" |
2073 assumes fS: "finite S" |
2088 assumes "finite S" |
2074 shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x" |
2089 shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x" |
2075 proof (induct rule: finite_induct[OF fS]) |
2090 using assms |
2076 case 1 |
2091 proof induction |
2077 then show ?case by (auto intro: zero_less_one) |
2092 case (insert x S) |
2078 next |
2093 then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x" |
2079 case (2 x F) |
|
2080 from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x" |
|
2081 by blast |
2094 by blast |
2082 show ?case |
2095 show ?case |
2083 proof (cases "x = a") |
2096 proof (cases "x = a") |
2084 case True |
2097 case True |
2085 with d show ?thesis by auto |
2098 with \<open>d > 0 \<close>d show ?thesis by auto |
2086 next |
2099 next |
2087 case False |
2100 case False |
2088 let ?d = "min d (dist a x)" |
2101 let ?d = "min d (dist a x)" |
2089 from False d(1) have dp: "?d > 0" |
2102 from False \<open>d > 0\<close> have dp: "?d > 0" |
2090 by auto |
2103 by auto |
2091 from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x" |
2104 from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x" |
2092 by auto |
2105 by auto |
2093 with dp False show ?thesis |
2106 with dp False show ?thesis |
2094 by (auto intro!: exI[where x="?d"]) |
2107 by (metis insert_iff le_less min_less_iff_conj not_less) |
2095 qed |
2108 qed |
2096 qed |
2109 qed (auto intro: zero_less_one) |
2097 |
2110 |
2098 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" |
2111 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" |
2099 by (simp add: islimpt_iff_eventually eventually_conj_iff) |
2112 by (simp add: islimpt_iff_eventually eventually_conj_iff) |
2100 |
2113 |
2101 lemma discrete_imp_closed: |
2114 lemma discrete_imp_closed: |