# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464190747 -3600
# Node ID 1aa23fe79b9761914f68bfb26da701f2ee29260a
# Parent  82df5181d69988f3df7987cff1104ba7e112dd16
moved two theorems

diff -r 82df5181d699 -r 1aa23fe79b97 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Wed May 25 16:38:35 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Wed May 25 16:39:07 2016 +0100
@@ -9,33 +9,6 @@
 
 begin
 
-lemma finite_ball_avoid:
-  assumes "open S" "finite X" "p \<in> S"
-  shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
-proof -
-  obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S" 
-    using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
-  obtain e2 where "0<e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" 
-    using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
-  hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" using e1_b by auto
-  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close> 
-    apply (rule_tac x="min e1 e2" in exI)
-    by auto
-qed
-
-lemma finite_cball_avoid:
-  fixes S :: "'a :: euclidean_space set"
-  assumes "open S" "finite X" "p \<in> S"
-  shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
-proof -
-  obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" 
-    using finite_ball_avoid[OF assms] by auto
-  define e2 where "e2 \<equiv> e1/2"
-  have "e2>0" and "e2<e1" unfolding e2_def using \<open>e1>0\<close> by auto
-  then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
-  then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> e1 by auto
-qed
-
 subsection\<open>Cauchy's inequality and more versions of Liouville\<close>
 
 lemma Cauchy_higher_deriv_bound: