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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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