Documentation

Mathlib.Order.Filter.AtTopBot.Group

Convergence to ±infinity in ordered commutative groups #

theorem Filter.tendsto_atTop_mul_left_of_le' {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ᶠ (x : α) in l, C f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x * g x) l atTop
theorem Filter.tendsto_atTop_add_left_of_le' {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ᶠ (x : α) in l, C f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop
theorem Filter.tendsto_atBot_mul_left_of_ge' {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ᶠ (x : α) in l, f x C) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x * g x) l atBot
theorem Filter.tendsto_atBot_add_left_of_ge' {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ᶠ (x : α) in l, f x C) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot
theorem Filter.tendsto_atTop_mul_left_of_le {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ (x : α), C f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x * g x) l atTop
theorem Filter.tendsto_atTop_add_left_of_le {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ (x : α), C f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop
theorem Filter.tendsto_atBot_mul_left_of_ge {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ (x : α), f x C) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x * g x) l atBot
theorem Filter.tendsto_atBot_add_left_of_ge {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : ∀ (x : α), f x C) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot
theorem Filter.tendsto_atTop_mul_right_of_le' {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atTop) (hg : ∀ᶠ (x : α) in l, C g x) :
Tendsto (fun (x : α) => f x * g x) l atTop
theorem Filter.tendsto_atTop_add_right_of_le' {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atTop) (hg : ∀ᶠ (x : α) in l, C g x) :
Tendsto (fun (x : α) => f x + g x) l atTop
theorem Filter.tendsto_atBot_mul_right_of_ge' {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atBot) (hg : ∀ᶠ (x : α) in l, g x C) :
Tendsto (fun (x : α) => f x * g x) l atBot
theorem Filter.tendsto_atBot_add_right_of_ge' {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atBot) (hg : ∀ᶠ (x : α) in l, g x C) :
Tendsto (fun (x : α) => f x + g x) l atBot
theorem Filter.tendsto_atTop_mul_right_of_le {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atTop) (hg : ∀ (x : α), C g x) :
Tendsto (fun (x : α) => f x * g x) l atTop
theorem Filter.tendsto_atTop_add_right_of_le {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atTop) (hg : ∀ (x : α), C g x) :
Tendsto (fun (x : α) => f x + g x) l atTop
theorem Filter.tendsto_atBot_mul_right_of_ge {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atBot) (hg : ∀ (x : α), g x C) :
Tendsto (fun (x : α) => f x * g x) l atBot
theorem Filter.tendsto_atBot_add_right_of_ge {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f g : αG} (C : G) (hf : Tendsto f l atBot) (hg : ∀ (x : α), g x C) :
Tendsto (fun (x : α) => f x + g x) l atBot
theorem Filter.tendsto_atTop_mul_const_left {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => C * f x) l atTop
theorem Filter.tendsto_atTop_add_const_left {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => C + f x) l atTop
theorem Filter.tendsto_atBot_mul_const_left {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => C * f x) l atBot
theorem Filter.tendsto_atBot_add_const_left {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => C + f x) l atBot
theorem Filter.tendsto_atTop_mul_const_right {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x * C) l atTop
theorem Filter.tendsto_atTop_add_const_right {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x + C) l atTop
theorem Filter.tendsto_atBot_mul_const_right {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => f x * C) l atBot
theorem Filter.tendsto_atBot_add_const_right {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] (l : Filter α) {f : αG} (C : G) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => f x + C) l atBot
@[simp]
theorem Filter.tendsto_inv_atTop_iff {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] {l : Filter α} {f : αG} :
Tendsto (fun (x : α) => (f x)⁻¹) l atTop Tendsto f l atBot
@[simp]
theorem Filter.tendsto_neg_atTop_iff {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] {l : Filter α} {f : αG} :
Tendsto (fun (x : α) => -f x) l atTop Tendsto f l atBot
@[simp]
theorem Filter.tendsto_inv_atBot_iff {α : Type u_1} {G : Type u_2} [OrderedCommGroup G] {l : Filter α} {f : αG} :
Tendsto (fun (x : α) => (f x)⁻¹) l atBot Tendsto f l atTop
@[simp]
theorem Filter.tendsto_neg_atBot_iff {α : Type u_1} {G : Type u_2} [OrderedAddCommGroup G] {l : Filter α} {f : αG} :
Tendsto (fun (x : α) => -f x) l atBot Tendsto f l atTop

$\lim_{x\to+\infty}|x|_m=+\infty$

$\lim_{x\to+\infty}|x|=+\infty$

$\lim_{x\to\infty^{-1}|x|_m=+\infty$

$\lim_{x\to-\infty}|x|=+\infty$