src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50104 de19856feb54
parent 50094 84ddcf5364b4
child 50105 65d5b18e1626
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:49:46 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     1.3 @@ -2044,6 +2044,10 @@
     1.4  unfolding bounded_any_center [where a=0]
     1.5  by (simp add: dist_norm)
     1.6  
     1.7 +lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
     1.8 +  unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
     1.9 +  using assms by auto
    1.10 +
    1.11  lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
    1.12  lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
    1.13    by (metis bounded_def subset_eq)