Convergence to ±infinity in ordered commutative groups

theorem Filter.tendsto_atTop_add_left_of_le' {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (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_add_left_of_ge' {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (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_add_left_of_le {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (hf : ∀ (x : α), C ≤ f x) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x + g x) l atTop

theorem Filter.tendsto_atBot_add_left_of_ge {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (hf : ∀ (x : α), f x ≤ C) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x + g x) l atBot

theorem Filter.tendsto_atTop_add_right_of_le' {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (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_add_right_of_ge' {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (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_add_right_of_le {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (hf : Tendsto f l atTop) (hg : ∀ (x : α), C ≤ g x) : Tendsto (fun (x : α) => f x + g x) l atTop

theorem Filter.tendsto_atBot_add_right_of_ge {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β) (hf : Tendsto f l atBot) (hg : ∀ (x : α), g x ≤ C) : Tendsto (fun (x : α) => f x + g x) l atBot

theorem Filter.tendsto_atTop_add_const_left {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Tendsto f l atTop) : Tendsto (fun (x : α) => C + f x) l atTop

theorem Filter.tendsto_atBot_add_const_left {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Tendsto f l atBot) : Tendsto (fun (x : α) => C + f x) l atBot

theorem Filter.tendsto_atTop_add_const_right {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Tendsto f l atTop) : Tendsto (fun (x : α) => f x + C) l atTop

theorem Filter.tendsto_atBot_add_const_right {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Tendsto f l atBot) : Tendsto (fun (x : α) => f x + C) l atBot

theorem Filter.map_neg_atBot {β : Type u_2} [OrderedAddCommGroup β] : map Neg.neg atBot = atTop

theorem Filter.map_neg_atTop {β : Type u_2} [OrderedAddCommGroup β] : map Neg.neg atTop = atBot

theorem Filter.comap_neg_atBot {β : Type u_2} [OrderedAddCommGroup β] : comap Neg.neg atBot = atTop

theorem Filter.comap_neg_atTop {β : Type u_2} [OrderedAddCommGroup β] : comap Neg.neg atTop = atBot

theorem Filter.tendsto_neg_atTop_atBot {β : Type u_2} [OrderedAddCommGroup β] : Tendsto Neg.neg atTop atBot

theorem Filter.tendsto_neg_atBot_atTop {β : Type u_2} [OrderedAddCommGroup β] : Tendsto Neg.neg atBot atTop

@[simp]

theorem Filter.tendsto_neg_atTop_iff {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] {l : Filter α} {f : α → β} : Tendsto (fun (x : α) => -f x) l atTop ↔ Tendsto f l atBot

@[simp]

theorem Filter.tendsto_neg_atBot_iff {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup β] {l : Filter α} {f : α → β} : Tendsto (fun (x : α) => -f x) l atBot ↔ Tendsto f l atTop

theorem Filter.tendsto_abs_atTop_atTop {α : Type u_1} [LinearOrderedAddCommGroup α] : Tendsto abs atTop atTop

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

theorem Filter.tendsto_abs_atBot_atTop {α : Type u_1} [LinearOrderedAddCommGroup α] : Tendsto abs atBot atTop

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

@[simp]

theorem Filter.comap_abs_atTop {α : Type u_1} [LinearOrderedAddCommGroup α] : comap abs atTop = atBot ⊔ atTop