mathlib documentation

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

source
theorem tendsto_coe_nat_at_top_iff {α : Type u_1} {R : Type u_2} [ordered_semiring R] [nontrivial R] [archimedean R] {f : α → ℕ} {l : filter α} :
filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top
source
theorem tendsto_coe_nat_at_top_at_top {R : Type u_2} [ordered_semiring R] [archimedean R] :
filter.tendsto coe filter.at_top filter.at_top
source
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 ↔ filter.tendsto f l filter.at_top
source
theorem tendsto_coe_int_at_top_at_top {R : Type u_2} [ordered_ring R] [archimedean R] :
filter.tendsto coe filter.at_top filter.at_top
source
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
source
theorem at_top_countable_basis_of_archimedean {R : Type u_2} [linear_ordered_semiring R] [archimedean R] :
filter.at_top.has_countable_basis (λ (i : R), i ∈ set.range coe) set.Ici
source
theorem at_bot_countable_basis_of_archimedean {R : Type u_2} [linear_ordered_ring R] [archimedean R] :
filter.at_bot.has_countable_basis (λ (i : R), i ∈ set.range coe) set.Iic
source
theorem at_top_countably_generated_of_archimedean {R : Type u_2} [linear_ordered_semiring R] [archimedean R] :
filter.at_top.is_countably_generated
source
theorem at_bot_countably_generated {R : Type u_2} [linear_ordered_ring R] [archimedean R] :
filter.at_bot.is_countably_generated
source
theorem filter.tendsto.const_mul_at_top' {α : Type u_1} {R : Type u_2} [linear_ordered_semiring R] [archimedean R] {l : filter α} {f : α → R} {r : R} (hr : 0 < r) (hf : filter.tendsto f l 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).

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