src/HOL/Library/Going_To_Filter.thy
changeset 67409 060efe532189
parent 66488 9d83e8fe3de3
child 68406 6beb45f6cf67
     1.1 --- a/src/HOL/Library/Going_To_Filter.thy	Fri Jan 12 15:27:46 2018 +0100
     1.2 +++ b/src/HOL/Library/Going_To_Filter.thy	Fri Jan 12 17:14:34 2018 +0100
     1.3 @@ -4,7 +4,9 @@
     1.4  
     1.5    A filter describing the points x such that f(x) tends to some other filter.
     1.6  *)
     1.7 -section \<open>The `going\_to' filter\<close>
     1.8 +
     1.9 +section \<open>The \<open>going_to\<close> filter\<close>
    1.10 +
    1.11  theory Going_To_Filter
    1.12    imports Complex_Main
    1.13  begin
    1.14 @@ -18,7 +20,7 @@
    1.15      where "f going_to F \<equiv> f going_to F within UNIV"
    1.16  
    1.17  text \<open>
    1.18 -  The `going\_to' filter is, in a sense, the opposite of @{term filtermap}. 
    1.19 +  The \<open>going_to\<close> filter is, in a sense, the opposite of @{term filtermap}. 
    1.20    It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the 
    1.21    range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be 
    1.22    written as @{term "f going_to F"}.
    1.23 @@ -27,7 +29,7 @@
    1.24    of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written
    1.25    as @{term "norm going_to at_top"}.
    1.26  
    1.27 -  Additionally, the `going\_to' filter can be restricted with an optional `within' parameter.
    1.28 +  Additionally, the \<open>going_to\<close> filter can be restricted with an optional `within' parameter.
    1.29    For instance, if one would would want to consider the filter of complex numbers near infinity
    1.30    that do not lie on the negative real line, one could write 
    1.31    @{term "norm going_to at_top within - complex_of_real ` {..0}"}.