# mathlibdocumentation

order.filter.archimedean

# 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} [archimedean R] {f : α → } {l : filter α} :
filter.tendsto (λ (n : α), (f n)) l filter.at_top

theorem tendsto_coe_nat_at_top_at_top {R : Type u_2} [archimedean R] :

theorem tendsto_coe_int_at_top_iff {α : Type u_1} {R : Type u_2} [archimedean R] {f : α → } {l : filter α} :
filter.tendsto (λ (n : α), (f n)) l filter.at_top

theorem tendsto_coe_int_at_top_at_top {R : Type u_2} [archimedean R] :

theorem tendsto_coe_rat_at_top_iff {α : Type u_1} {R : Type u_2} [archimedean R] {f : α → } {l : filter α} :
filter.tendsto (λ (n : α), (f n)) l filter.at_top