remove duplicate lemma finite_choice in favor of finite_set_choice
authorhuffman
Sat Sep 03 09:26:11 2011 -0700 (2011-09-03 ago)
changeset 4468149ef76b4a634
parent 44680 761f427ef1ab
child 44682 e5ba1c0b8cac
child 44690 b6d8b11ed399
remove duplicate lemma finite_choice in favor of finite_set_choice
NEWS
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
     1.1 --- a/NEWS	Sat Sep 03 09:12:19 2011 -0700
     1.2 +++ b/NEWS	Sat Sep 03 09:26:11 2011 -0700
     1.3 @@ -204,6 +204,7 @@
     1.4  removed, and other theorems have been renamed or replaced with more
     1.5  general versions. INCOMPATIBILITY.
     1.6  
     1.7 +  finite_choice ~> finite_set_choice
     1.8    eventually_conjI ~> eventually_conj
     1.9    eventually_and ~> eventually_conj_iff
    1.10    eventually_false ~> eventually_False
     2.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Sep 03 09:12:19 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Sep 03 09:26:11 2011 -0700
     2.3 @@ -270,13 +270,6 @@
     2.4  
     2.5  subsection {* Metric space *}
     2.6  
     2.7 -(* TODO: move somewhere else *)
     2.8 -lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
     2.9 -apply (induct set: finite, simp_all)
    2.10 -apply (clarify, rename_tac y)
    2.11 -apply (rule_tac x="f(x:=y)" in exI, simp)
    2.12 -done
    2.13 -
    2.14  instantiation vec :: (metric_space, finite) metric_space
    2.15  begin
    2.16  
    2.17 @@ -311,7 +304,7 @@
    2.18        have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
    2.19          using A unfolding open_dist by simp
    2.20        hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
    2.21 -        by (rule finite_choice [OF finite])
    2.22 +        by (rule finite_set_choice [OF finite])
    2.23        then obtain r where r1: "\<forall>i. 0 < r i"
    2.24          and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
    2.25        have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"