at_top
filter and archimedean (semi)rings/fields #
In this file we prove that for a linear ordered archimedean semiring R
and a function f : α → ℕ
,
the function coe ∘ f : α → R
tends to at_top
along a filter l
if and only if so does f
.
We also prove that coe : ℕ → R
tends to at_top
along at_top
, as well as version of these
two results for ℤ
(and a ring R
) and ℚ
(and a field R
).
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on ℕ
, ℤ
and ℝ
, although not necessary (a version in ordered fields is
given in filter.tendsto.const_mul_at_top
).
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on ℕ
, ℤ
and ℝ
, although not necessary (a version in ordered fields is
given in filter.tendsto.at_top_mul_const
).