Convergence to ±infinity in ordered commutative groups

theorem Filter.tendsto_atTop_mul_left_of_le' {α : Type u_1} {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α) {f : α → G} (C : G) (hf : Tendsto f l atBot) : Tendsto (fun (x : α) => f x + C) l atBot

theorem Filter.map_inv_atBot {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : map Inv.inv atBot = atTop

theorem Filter.map_neg_atBot {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : map Neg.neg atBot = atTop

theorem Filter.map_inv_atTop {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : map Inv.inv atTop = atBot

theorem Filter.map_neg_atTop {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : map Neg.neg atTop = atBot

theorem Filter.comap_inv_atBot {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : comap Inv.inv atBot = atTop

theorem Filter.comap_neg_atBot {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : comap Neg.neg atBot = atTop

theorem Filter.comap_inv_atTop {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : comap Inv.inv atTop = atBot

theorem Filter.comap_neg_atTop {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : comap Neg.neg atTop = atBot

theorem Filter.tendsto_inv_atTop_atBot {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : Tendsto Inv.inv atTop atBot

theorem Filter.tendsto_neg_atTop_atBot {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : Tendsto Neg.neg atTop atBot

theorem Filter.tendsto_inv_atBot_atTop {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : Tendsto Inv.inv atBot atTop

theorem Filter.tendsto_neg_atBot_atTop {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : Tendsto Neg.neg atBot atTop

@[simp]

theorem Filter.tendsto_inv_atTop_iff {α : Type u_1} {G : Type u_2} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [PartialOrder G] [IsOrderedMonoid 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} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] {l : Filter α} {f : α → G} : Tendsto (fun (x : α) => -f x) l atBot ↔ Tendsto f l atTop

theorem Filter.tendsto_mabs_atTop_atTop {G : Type u_2} [CommGroup G] [LinearOrder G] : Tendsto mabs atTop atTop

$\underset{x\to +\mathrm{\infty }}{lim}|x{|}_m=+\mathrm{\infty }$

theorem Filter.tendsto_abs_atTop_atTop {G : Type u_2} [AddCommGroup G] [LinearOrder G] : Tendsto abs atTop atTop

$\underset{x\to +\mathrm{\infty }}{lim}|x|=+\mathrm{\infty }$

theorem Filter.tendsto_mabs_atBot_atTop {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] : Tendsto mabs atBot atTop

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

theorem Filter.tendsto_abs_atBot_atTop {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : Tendsto abs atBot atTop

$\underset{x\to -\mathrm{\infty }}{lim}|x|=+\mathrm{\infty }$

@[simp]

theorem Filter.comap_mabs_atTop {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] : comap mabs atTop = atBot ⊔ atTop

@[simp]

theorem Filter.comap_abs_atTop {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : comap abs atTop = atBot ⊔ atTop