# 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).

@[simp]
theorem nat.comap_coe_at_top {R : Type u_2} [nontrivial R] [archimedean R] :
theorem tendsto_coe_nat_at_top_iff {α : Type u_1} {R : Type u_2} [nontrivial R] [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] :
@[simp]
theorem int.comap_coe_at_top {R : Type u_2} [ordered_ring R] [nontrivial R] [archimedean R] :
@[simp]
theorem int.comap_coe_at_bot {R : Type u_2} [ordered_ring R] [nontrivial R] [archimedean R] :
theorem tendsto_coe_int_at_top_iff {α : Type u_1} {R : Type u_2} [ordered_ring R] [nontrivial R] [archimedean R] {f : α → } {l : filter α} :
filter.tendsto (λ (n : α), (f n)) l filter.at_top
theorem tendsto_coe_int_at_bot_iff {α : Type u_1} {R : Type u_2} [ordered_ring R] [nontrivial R] [archimedean R] {f : α → } {l : filter α} :
filter.tendsto (λ (n : α), (f n)) l filter.at_bot
theorem tendsto_coe_int_at_top_at_top {R : Type u_2} [ordered_ring R] [archimedean R] :
@[simp]
theorem rat.comap_coe_at_top {R : Type u_2} [archimedean R] :
@[simp]
theorem rat.comap_coe_at_bot {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
theorem tendsto_coe_rat_at_bot_iff {α : Type u_1} {R : Type u_2} [archimedean R] {f : α → } {l : filter α} :
filter.tendsto (λ (n : α), (f n)) l filter.at_bot
@[protected, instance]
@[protected, instance]
theorem filter.tendsto.const_mul_at_top' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [archimedean R] (hr : 0 < r) (hf : filter.at_top) :
filter.tendsto (λ (x : α), r * f x) l filter.at_top

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).

theorem filter.tendsto.at_top_mul_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [archimedean R] (hr : 0 < r) (hf : filter.at_top) :
filter.tendsto (λ (x : α), f x * r) l filter.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).

theorem filter.tendsto.at_top_mul_neg_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [archimedean R] (hr : r < 0) (hf : filter.at_top) :
filter.tendsto (λ (x : α), f x * r) l filter.at_bot

See also filter.tendsto.at_top_mul_neg_const for a version of this lemma for linear_ordered_fields which does not require the archimedean assumption.

theorem filter.tendsto.at_bot_mul_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [archimedean R] (hr : 0 < r) (hf : filter.at_bot) :
filter.tendsto (λ (x : α), f x * r) l filter.at_bot

See also filter.tendsto.at_bot_mul_const for a version of this lemma for linear_ordered_fields which does not require the archimedean assumption.

theorem filter.tendsto.at_bot_mul_neg_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [archimedean R] (hr : r < 0) (hf : filter.at_bot) :
filter.tendsto (λ (x : α), f x * r) l filter.at_top

See also filter.tendsto.at_bot_mul_neg_const for a version of this lemma for linear_ordered_fields which does not require the archimedean assumption.

theorem filter.tendsto.at_top_nsmul_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [archimedean R] {f : α → } (hr : 0 < r) (hf : filter.at_top) :
filter.tendsto (λ (x : α), f x r) l filter.at_top
theorem filter.tendsto.at_top_nsmul_neg_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [archimedean R] {f : α → } (hr : r < 0) (hf : filter.at_top) :
filter.tendsto (λ (x : α), f x r) l filter.at_bot
theorem filter.tendsto.at_top_zsmul_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [archimedean R] {f : α → } (hr : 0 < r) (hf : filter.at_top) :
filter.tendsto (λ (x : α), f x r) l filter.at_top
theorem filter.tendsto.at_top_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [archimedean R] {f : α → } (hr : r < 0) (hf : filter.at_top) :
filter.tendsto (λ (x : α), f x r) l filter.at_bot
theorem filter.tendsto.at_bot_zsmul_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [archimedean R] {f : α → } (hr : 0 < r) (hf : filter.at_bot) :
filter.tendsto (λ (x : α), f x r) l filter.at_bot
theorem filter.tendsto.at_bot_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [archimedean R] {f : α → } (hr : r < 0) (hf : filter.at_bot) :
filter.tendsto (λ (x : α), f x r) l filter.at_top