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}"}.