summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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