src/HOL/Library/Topology_Euclidean_Space.thy
changeset 31530 e31d63c66f55
parent 31529 689f5dae1f41
child 31531 fc78714d14e1
equal deleted inserted replaced
31529:689f5dae1f41 31530:e31d63c66f55
   967 definition
   967 definition
   968   at_infinity :: "'a::real_normed_vector net" where
   968   at_infinity :: "'a::real_normed_vector net" where
   969   "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
   969   "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
   970 
   970 
   971 definition
   971 definition
   972   indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
   972   indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
   973   "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
   973   "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
   974 
   974 
   975 text{* Prove That They are all nets. *}
   975 text{* Prove That They are all nets. *}
   976 
   976 
   977 lemma Rep_net_at_infinity:
   977 lemma Rep_net_at_infinity:
   978   "Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})"
   978   "Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})"