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 : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.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 : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.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 : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.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 : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

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

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

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

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

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

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

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

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

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

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

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

theorem Filter.tendsto_atBot_of_add_const_right {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} (C : β) (hf : Filter.Tendsto (fun (x : α) => f x + C) l Filter.atBot) : Filter.Tendsto f l Filter.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 : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop) : Filter.Tendsto g l Filter.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 : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot) : Filter.Tendsto g l Filter.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) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop → Filter.Tendsto g l Filter.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) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot → Filter.Tendsto g l Filter.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 : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop) : Filter.Tendsto f l Filter.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 : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot) : Filter.Tendsto f l Filter.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) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop → Filter.Tendsto f l Filter.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) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot