# Convergence to ±infinity in linear ordered (semi)fields #

### Multiplication by constant: iff lemmas #

source
theorem Filter.tendsto_const_mul_atTop_of_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :
Tendsto (fun (x : β) => r * f x) l atTop ↔ Tendsto f l atTop

If `r` is a positive constant, `fun x ↦ r * f x` tends to infinity along a filter if and only if `f` tends to infinity along the same filter.

source
theorem Filter.tendsto_mul_const_atTop_of_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :
Tendsto (fun (x : β) => f x * r) l atTop ↔ Tendsto f l atTop

If `r` is a positive constant, `fun x ↦ f x * r` tends to infinity along a filter if and only if `f` tends to infinity along the same filter.

source
theorem Filter.tendsto_div_const_atTop_of_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :
Tendsto (fun (x : β) => f x / r) l atTop ↔ Tendsto f l atTop

If `r` is a positive constant, `x ↦ f x / r` tends to infinity along a filter if and only if `f` tends to infinity along the same filter.

source
theorem Filter.tendsto_const_mul_atTop_iff_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) :
Tendsto (fun (x : β) => r * f x) l atTop ↔ 0 < r

If `f` tends to infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to infinity if and only if `0 < r`.

source
theorem Filter.tendsto_mul_const_atTop_iff_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x * r) l atTop ↔ 0 < r

If `f` tends to infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to infinity if and only if `0 < r`.

source
theorem Filter.tendsto_div_const_atTop_iff_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x / r) l atTop ↔ 0 < r

If `f` tends to infinity along a nontrivial filter `l`, then `x ↦ f x * r` tends to infinity if and only if `0 < r`.

source
theorem Filter.Tendsto.const_mul_atTop {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : β) => r * f x) l atTop

If `f` tends to infinity along a filter, then `f` multiplied by a positive constant (on the left) also tends to infinity. For a version working in `ℕ` or `ℤ`, use `Filter.Tendsto.const_mul_atTop'` instead.

source
theorem Filter.Tendsto.atTop_mul_const {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x * r) l atTop

If a function `f` tends to infinity along a filter, then `f` multiplied by a positive constant (on the right) also tends to infinity. For a version working in `ℕ` or `ℤ`, use `Filter.Tendsto.atTop_mul_const'` instead.

source
theorem Filter.Tendsto.atTop_div_const {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x / r) l atTop

If a function `f` tends to infinity along a filter, then `f` divided by a positive constant also tends to infinity.

source
theorem Filter.tendsto_const_mul_pow_atTop {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : 0 < c) :
Tendsto (fun (x : α) => c * x ^ n) atTop atTop
source
theorem Filter.tendsto_const_mul_pow_atTop_iff {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} :
Tendsto (fun (x : α) => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
source
theorem Filter.tendsto_zpow_atTop_atTop {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℤ} (hn : 0 < n) :
Tendsto (fun (x : α) => x ^ n) atTop atTop
source
theorem Filter.map_div_atTop_eq {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (k : α) (hk : 0 < k) :
map (fun (a : α) => a / k) atTop = atTop
source
theorem Filter.tendsto_const_mul_atBot_of_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :
Tendsto (fun (x : β) => r * f x) l atBot ↔ Tendsto f l atBot

If `r` is a positive constant, `fun x ↦ r * f x` tends to negative infinity along a filter if and only if `f` tends to negative infinity along the same filter.

source
theorem Filter.tendsto_mul_const_atBot_of_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :
Tendsto (fun (x : β) => f x * r) l atBot ↔ Tendsto f l atBot

If `r` is a positive constant, `fun x ↦ f x * r` tends to negative infinity along a filter if and only if `f` tends to negative infinity along the same filter.

source
theorem Filter.tendsto_div_const_atBot_of_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :
Tendsto (fun (x : β) => f x / r) l atBot ↔ Tendsto f l atBot

If `r` is a positive constant, `fun x ↦ f x / r` tends to negative infinity along a filter if and only if `f` tends to negative infinity along the same filter.

source
theorem Filter.tendsto_const_mul_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :
Tendsto (fun (x : β) => r * f x) l atTop ↔ Tendsto f l atBot

If `r` is a negative constant, `fun x ↦ r * f x` tends to infinity along a filter `l` if and only if `f` tends to negative infinity along `l`.

source
theorem Filter.tendsto_mul_const_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :
Tendsto (fun (x : β) => f x * r) l atTop ↔ Tendsto f l atBot

If `r` is a negative constant, `fun x ↦ f x * r` tends to infinity along a filter `l` if and only if `f` tends to negative infinity along `l`.

source
theorem Filter.tendsto_div_const_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :
Tendsto (fun (x : β) => f x / r) l atTop ↔ Tendsto f l atBot

If `r` is a negative constant, `fun x ↦ f x / r` tends to infinity along a filter `l` if and only if `f` tends to negative infinity along `l`.

source
theorem Filter.tendsto_const_mul_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :
Tendsto (fun (x : β) => r * f x) l atBot ↔ Tendsto f l atTop

If `r` is a negative constant, `fun x ↦ r * f x` tends to negative infinity along a filter `l` if and only if `f` tends to infinity along `l`.

source
theorem Filter.tendsto_mul_const_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :
Tendsto (fun (x : β) => f x * r) l atBot ↔ Tendsto f l atTop

If `r` is a negative constant, `fun x ↦ f x * r` tends to negative infinity along a filter `l` if and only if `f` tends to infinity along `l`.

source
theorem Filter.tendsto_div_const_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :
Tendsto (fun (x : β) => f x / r) l atBot ↔ Tendsto f l atTop

If `r` is a negative constant, `fun x ↦ f x / r` tends to negative infinity along a filter `l` if and only if `f` tends to infinity along `l`.

source
theorem Filter.tendsto_const_mul_atTop_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :
Tendsto (fun (x : β) => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

The function `fun x ↦ r * f x` tends to infinity along a nontrivial filter if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity.

source
theorem Filter.tendsto_mul_const_atTop_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :
Tendsto (fun (x : β) => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

The function `fun x ↦ f x * r` tends to infinity along a nontrivial filter if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity.

source
theorem Filter.tendsto_div_const_atTop_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :
Tendsto (fun (x : β) => f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

The function `fun x ↦ f x / r` tends to infinity along a nontrivial filter if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity.

source
theorem Filter.tendsto_const_mul_atBot_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :
Tendsto (fun (x : β) => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

The function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity.

source
theorem Filter.tendsto_mul_const_atBot_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :
Tendsto (fun (x : β) => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

The function `fun x ↦ f x * r` tends to negative infinity along a nontrivial filter if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity.

source
theorem Filter.tendsto_div_const_atBot_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :
Tendsto (fun (x : β) => f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

The function `fun x ↦ f x / r` tends to negative infinity along a nontrivial filter if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity.

source
theorem Filter.tendsto_const_mul_atTop_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) :
Tendsto (fun (x : β) => r * f x) l atTop ↔ r < 0

If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to infinity if and only if `r < 0`.

source
theorem Filter.tendsto_mul_const_atTop_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x * r) l atTop ↔ r < 0

If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to infinity if and only if `r < 0`.

source
theorem Filter.tendsto_div_const_atTop_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x / r) l atTop ↔ r < 0

If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ f x / r` tends to infinity if and only if `r < 0`.

source
theorem Filter.tendsto_const_mul_atBot_iff_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) :
Tendsto (fun (x : β) => r * f x) l atBot ↔ 0 < r

If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to negative infinity if and only if `0 < r`.

source
theorem Filter.tendsto_mul_const_atBot_iff_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x * r) l atBot ↔ 0 < r

If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to negative infinity if and only if `0 < r`.

source
theorem Filter.tendsto_div_const_atBot_iff_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x / r) l atBot ↔ 0 < r

If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ f x / r` tends to negative infinity if and only if `0 < r`.

source
theorem Filter.tendsto_const_mul_atBot_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) :
Tendsto (fun (x : β) => r * f x) l atBot ↔ r < 0

If `f` tends to infinity along a nontrivial filter, `fun x ↦ r * f x` tends to negative infinity if and only if `r < 0`.

source
theorem Filter.tendsto_mul_const_atBot_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x * r) l atBot ↔ r < 0

If `f` tends to infinity along a nontrivial filter, `fun x ↦ f x * r` tends to negative infinity if and only if `r < 0`.

source
theorem Filter.tendsto_div_const_atBot_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x / r) l atBot ↔ r < 0

If `f` tends to infinity along a nontrivial filter, `fun x ↦ f x / r` tends to negative infinity if and only if `r < 0`.

source
theorem Filter.Tendsto.const_mul_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atTop) :
Tendsto (fun (x : β) => r * f x) l atBot

If a function `f` tends to infinity along a filter, then `f` multiplied by a negative constant (on the left) tends to negative infinity.

source
theorem Filter.Tendsto.atTop_mul_const_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x * r) l atBot

If a function `f` tends to infinity along a filter, then `f` multiplied by a negative constant (on the right) tends to negative infinity.

source
theorem Filter.Tendsto.atTop_div_const_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atTop) :
Tendsto (fun (x : β) => f x / r) l atBot

If a function `f` tends to infinity along a filter, then `f` divided by a negative constant tends to negative infinity.

source
theorem Filter.Tendsto.const_mul_atBot {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atBot) :
Tendsto (fun (x : β) => r * f x) l atBot

If a function `f` tends to negative infinity along a filter, then `f` multiplied by a positive constant (on the left) also tends to negative infinity.

source
theorem Filter.Tendsto.atBot_mul_const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x * r) l atBot

If a function `f` tends to negative infinity along a filter, then `f` multiplied by a positive constant (on the right) also tends to negative infinity.

source
theorem Filter.Tendsto.atBot_div_const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x / r) l atBot

If a function `f` tends to negative infinity along a filter, then `f` divided by a positive constant also tends to negative infinity.

source
theorem Filter.Tendsto.const_mul_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atBot) :
Tendsto (fun (x : β) => r * f x) l atTop

If a function `f` tends to negative infinity along a filter, then `f` multiplied by a negative constant (on the left) tends to positive infinity.

source
theorem Filter.Tendsto.atBot_mul_const_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atBot) :
Tendsto (fun (x : β) => f x * r) l atTop

If a function tends to negative infinity along a filter, then `f` multiplied by a negative constant (on the right) tends to positive infinity.

source
theorem Filter.tendsto_neg_const_mul_pow_atTop {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) :
Tendsto (fun (x : α) => c * x ^ n) atTop atBot
source
theorem Filter.tendsto_const_mul_pow_atBot_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} :
Tendsto (fun (x : α) => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0