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
@[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
$\lim_{x\to+\infty}|x|=+\infty$
$\lim_{x\to-\infty}|x|=+\infty$
@[simp]