src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50105 65d5b18e1626
parent 50104 de19856feb54
child 50245 dea9363887a6
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 19:14:23 2012 +0100
     1.3 @@ -3097,9 +3097,6 @@
     1.4    assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
     1.5  qed
     1.6  
     1.7 -lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
     1.8 -  by metis
     1.9 -
    1.10  lemma nat_approx_posE:
    1.11    fixes e::real
    1.12    assumes "0 < e"