Convergence to ±infinity in ordered commutative monoids

theorem Filter.tendsto_atTop_add_nonneg_left' {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : ∀ᶠ (x : α) in l, 0 ≤ f x) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x + g x) l atTop

theorem Filter.tendsto_atBot_add_nonpos_left' {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : ∀ᶠ (x : α) in l, f x ≤ 0) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x + g x) l atBot

theorem Filter.tendsto_atTop_add_nonneg_left {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : ∀ (x : α), 0 ≤ f x) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x + g x) l atTop

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

theorem Filter.tendsto_atTop_add_nonneg_right' {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : Tendsto f l atTop) (hg : ∀ᶠ (x : α) in l, 0 ≤ g x) : Tendsto (fun (x : α) => f x + g x) l atTop

theorem Filter.tendsto_atBot_add_nonpos_right' {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : Tendsto f l atBot) (hg : ∀ᶠ (x : α) in l, g x ≤ 0) : Tendsto (fun (x : α) => f x + g x) l atBot

theorem Filter.tendsto_atTop_add_nonneg_right {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : Tendsto f l atTop) (hg : ∀ (x : α), 0 ≤ g x) : Tendsto (fun (x : α) => f x + g x) l atTop

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

theorem Filter.tendsto_atTop_add {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) : Tendsto (fun (x : α) => f x + g x) l atTop

theorem Filter.tendsto_atBot_add {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f g : α → β} (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) : Tendsto (fun (x : α) => f x + g x) l atBot

theorem Filter.Tendsto.nsmul_atTop {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} (hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) : Tendsto (fun (x : α) => n • f x) l atTop

theorem Filter.Tendsto.nsmul_atBot {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} (hf : Tendsto f l atBot) {n : ℕ} (hn : 0 < n) : Tendsto (fun (x : α) => n • f x) l atBot

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

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

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

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

theorem Filter.tendsto_atTop_of_add_bdd_above_left' {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, f x ≤ C) (h : Tendsto (fun (x : α) => f x + g x) l atTop) : Tendsto g l atTop

theorem Filter.tendsto_atBot_of_add_bdd_below_left' {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, C ≤ f x) (h : Tendsto (fun (x : α) => f x + g x) l atBot) : Tendsto g l atBot

theorem Filter.tendsto_atTop_of_add_bdd_above_left {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f g : α → β} (C : β) (hC : ∀ (x : α), f x ≤ C) : Tendsto (fun (x : α) => f x + g x) l atTop → Tendsto g l atTop

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

theorem Filter.tendsto_atTop_of_add_bdd_above_right' {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, g x ≤ C) (h : Tendsto (fun (x : α) => f x + g x) l atTop) : Tendsto f l atTop

theorem Filter.tendsto_atBot_of_add_bdd_below_right' {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, C ≤ g x) (h : Tendsto (fun (x : α) => f x + g x) l atBot) : Tendsto f l atBot

theorem Filter.tendsto_atTop_of_add_bdd_above_right {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f g : α → β} (C : β) (hC : ∀ (x : α), g x ≤ C) : Tendsto (fun (x : α) => f x + g x) l atTop → Tendsto f l atTop

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