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