src/HOL/Library/Topology_Euclidean_Space.thy
 changeset 31530 e31d63c66f55 parent 31529 689f5dae1f41 child 31531 fc78714d14e1
equal 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})"`