src/HOL/Limits.thy
changeset 50326 b5afeccab2db
parent 50325 5e40ad9f212a
child 50327 bbea2e82871c
     1.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:04 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:05 2012 +0100
     1.3 @@ -373,6 +373,12 @@
     1.4  definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
     1.5    where "at a = nhds a within - {a}"
     1.6  
     1.7 +abbreviation at_right :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
     1.8 +  "at_right x \<equiv> at x within {x <..}"
     1.9 +
    1.10 +abbreviation at_left :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
    1.11 +  "at_left x \<equiv> at x within {..< x}"
    1.12 +
    1.13  definition at_infinity :: "'a::real_normed_vector filter" where
    1.14    "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
    1.15