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).
theorem
tendsto_coe_nat_at_top_iff
{α : Type u_1}
{R : Type u_2}
[linear_ordered_semiring R]
[archimedean R]
{f : α → ℕ}
{l : filter α} :
filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top
theorem
tendsto_coe_int_at_top_iff
{α : Type u_1}
{R : Type u_2}
[linear_ordered_ring R]
[archimedean R]
{f : α → ℤ}
{l : filter α} :
filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top
theorem
tendsto_coe_rat_at_top_iff
{α : Type u_1}
{R : Type u_2}
[linear_ordered_field R]
[archimedean R]
{f : α → ℚ}
{l : filter α} :
filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top