Documentation

Mathlib.Order.Filter.AtTopBot.Monoid

Convergence to ±infinity in ordered commutative monoids #

source
theorem Filter.Tendsto.one_eventuallyLE_mul_atTop {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : 1 ≤ᶠ[l] f) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x * g x) l atTop
source
theorem Filter.Tendsto.zero_eventuallyLE_add_atTop {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : 0 ≤ᶠ[l] f) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop
source
@[deprecated Filter.Tendsto.zero_eventuallyLE_add_atTop (since := "2025-02-13")]
theorem Filter.tendsto_atTop_add_nonneg_left' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : 0 ≤ᶠ[l] f) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop

Alias of Filter.Tendsto.zero_eventuallyLE_add_atTop.

source
theorem Filter.Tendsto.eventuallyLE_one_mul_atBot {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : f ≤ᶠ[l] 1) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x * g x) l atBot
source
theorem Filter.Tendsto.eventuallyLE_zero_add_atBot {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : f ≤ᶠ[l] 0) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot
source
@[deprecated Filter.Tendsto.eventuallyLE_zero_add_atBot (since := "2025-02-13")]
theorem Filter.tendsto_atBot_add_nonpos_left' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : f ≤ᶠ[l] 0) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot

Alias of Filter.Tendsto.eventuallyLE_zero_add_atBot.

source
theorem Filter.Tendsto.one_le_mul_atTop {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : ∀ (x : α), 1 ≤ f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x * g x) l atTop
source
theorem Filter.Tendsto.nonneg_add_atTop {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : ∀ (x : α), 0 ≤ f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop
source
@[deprecated Filter.Tendsto.nonneg_add_atTop (since := "2025-02-13")]
theorem Filter.tendsto_atTop_add_nonneg_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : ∀ (x : α), 0 ≤ f x) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop

Alias of Filter.Tendsto.nonneg_add_atTop.

source
theorem Filter.Tendsto.le_one_mul_atBot {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : ∀ (x : α), f x ≤ 1) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x * g x) l atBot
source
theorem Filter.Tendsto.nonpos_add_atBot {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : ∀ (x : α), f x ≤ 0) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot
source
@[deprecated Filter.Tendsto.nonpos_add_atBot (since := "2025-02-13")]
theorem Filter.tendsto_atBot_add_nonpos_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : ∀ (x : α), f x ≤ 0) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot

Alias of Filter.Tendsto.nonpos_add_atBot.

source
theorem Filter.Tendsto.atTop_mul_one_eventuallyLE {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : 1 ≤ᶠ[l] g) :
Tendsto (fun (x : α) => f x * g x) l atTop
source
theorem Filter.Tendsto.atTop_add_zero_eventuallyLE {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : 0 ≤ᶠ[l] g) :
Tendsto (fun (x : α) => f x + g x) l atTop
source
@[deprecated Filter.Tendsto.atTop_add_zero_eventuallyLE (since := "2025-02-13")]
theorem Filter.tendsto_atTop_add_nonneg_right' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : 0 ≤ᶠ[l] g) :
Tendsto (fun (x : α) => f x + g x) l atTop

Alias of Filter.Tendsto.atTop_add_zero_eventuallyLE.

source
theorem Filter.Tendsto.atBot_mul_eventuallyLE_one {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : g ≤ᶠ[l] 1) :
Tendsto (fun (x : α) => f x * g x) l atBot
source
theorem Filter.Tendsto.atBot_add_eventuallyLE_zero {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : g ≤ᶠ[l] 0) :
Tendsto (fun (x : α) => f x + g x) l atBot
source
@[deprecated Filter.Tendsto.atBot_add_eventuallyLE_zero (since := "2025-02-13")]
theorem Filter.tendsto_atBot_add_nonpos_right' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : g ≤ᶠ[l] 0) :
Tendsto (fun (x : α) => f x + g x) l atBot

Alias of Filter.Tendsto.atBot_add_eventuallyLE_zero.

source
theorem Filter.Tendsto.atTop_mul_one_le {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : ∀ (x : α), 1 ≤ g x) :
Tendsto (fun (x : α) => f x * g x) l atTop
source
theorem Filter.Tendsto.atTop_add_nonneg {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : ∀ (x : α), 0 ≤ g x) :
Tendsto (fun (x : α) => f x + g x) l atTop
source
@[deprecated Filter.Tendsto.atTop_add_nonneg (since := "2025-02-13")]
theorem Filter.tendsto_atTop_add_nonneg_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : ∀ (x : α), 0 ≤ g x) :
Tendsto (fun (x : α) => f x + g x) l atTop

Alias of Filter.Tendsto.atTop_add_nonneg.

source
theorem Filter.Tendsto.atBot_mul_le_one {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : ∀ (x : α), g x ≤ 1) :
Tendsto (fun (x : α) => f x * g x) l atBot
source
theorem Filter.Tendsto.atBot_add_nonpos {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : ∀ (x : α), g x ≤ 0) :
Tendsto (fun (x : α) => f x + g x) l atBot
source
@[deprecated Filter.Tendsto.atBot_add_nonpos (since := "2025-02-13")]
theorem Filter.tendsto_atBot_add_nonpos_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : ∀ (x : α), g x ≤ 0) :
Tendsto (fun (x : α) => f x + g x) l atBot

Alias of Filter.Tendsto.atBot_add_nonpos.

source
theorem Filter.Tendsto.atTop_mul_atTop {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x * g x) l atTop

In an ordered multiplicative monoid, if f and g tend to +∞, then so does f * g.

Earlier, this name was used for a similar lemma about semirings, which is now called Filter.Tendsto.atTop_mul_atTop₀.

source
theorem Filter.Tendsto.atTop_add_atTop {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop
source
@[deprecated Filter.Tendsto.atTop_add_atTop (since := "2025-02-13")]
theorem Filter.tendsto_atTop_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
Tendsto (fun (x : α) => f x + g x) l atTop

Alias of Filter.Tendsto.atTop_add_atTop.

source
theorem Filter.Tendsto.atBot_mul_atBot {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x * g x) l atBot

In an ordered multiplicative monoid, if f and g tend to -∞, then so does f * g.

Earlier, this name was used for a similar lemma about rings (with conclusion f * g → +∞), which is now called Filter.Tendsto.atBot_mul_atBot₀.

source
theorem Filter.Tendsto.atBot_add_atBot {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot
source
@[deprecated Filter.Tendsto.atBot_add_atBot (since := "2025-02-13")]
theorem Filter.tendsto_atBot_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
Tendsto (fun (x : α) => f x + g x) l atBot

Alias of Filter.Tendsto.atBot_add_atBot.

source
theorem Filter.Tendsto.atTop_pow {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f : α → M} (hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) :
Tendsto (fun (x : α) => f x ^ n) l atTop
source
theorem Filter.Tendsto.nsmul_atTop {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f : α → M} (hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) :
Tendsto (fun (x : α) => n • f x) l atTop
source
theorem Filter.Tendsto.atBot_pow {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : Filter α} {f : α → M} (hf : Tendsto f l atBot) {n : ℕ} (hn : 0 < n) :
Tendsto (fun (x : α) => f x ^ n) l atBot
source
theorem Filter.Tendsto.nsmul_atBot {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : Filter α} {f : α → M} (hf : Tendsto f l atBot) {n : ℕ} (hn : 0 < n) :
Tendsto (fun (x : α) => n • f x) l atBot
source
theorem Filter.Tendsto.atTop_of_const_mul {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => C * f x) l atTop) :
Tendsto f l atTop

In an ordered cancellative multiplicative monoid, if C * f x → +∞, then f x → +∞.

Earlier, this name was used for a similar lemma about ordered rings, which is now called Filter.Tendsto.atTop_of_const_mul₀.

source
theorem Filter.Tendsto.atTop_of_const_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => C + f x) l atTop) :
Tendsto f l atTop
source
@[deprecated Filter.Tendsto.atTop_of_const_add (since := "2025-02-13")]
theorem Filter.tendsto_atTop_of_add_const_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => C + f x) l atTop) :
Tendsto f l atTop

Alias of Filter.Tendsto.atTop_of_const_add.

source
theorem Filter.Tendsto.atBot_of_const_mul {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => C * f x) l atBot) :
Tendsto f l atBot
source
theorem Filter.Tendsto.atBot_of_const_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => C + f x) l atBot) :
Tendsto f l atBot
source
@[deprecated Filter.Tendsto.atBot_of_const_add (since := "2025-02-13")]
theorem Filter.tendsto_atBot_of_add_const_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => C + f x) l atBot) :
Tendsto f l atBot

Alias of Filter.Tendsto.atBot_of_const_add.

source
theorem Filter.Tendsto.atTop_of_mul_const {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => f x * C) l atTop) :
Tendsto f l atTop

In an ordered cancellative multiplicative monoid, if f x * C → +∞, then f x → +∞.

Earlier, this name was used for a similar lemma about ordered rings, which is now called Filter.Tendsto.atTop_of_mul_const₀.

source
theorem Filter.Tendsto.atTop_of_add_const {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => f x + C) l atTop) :
Tendsto f l atTop
source
@[deprecated Filter.Tendsto.atTop_of_add_const (since := "2025-02-13")]
theorem Filter.tendsto_atTop_of_add_const_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => f x + C) l atTop) :
Tendsto f l atTop

Alias of Filter.Tendsto.atTop_of_add_const.

source
theorem Filter.Tendsto.atBot_of_mul_const {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => f x * C) l atBot) :
Tendsto f l atBot
source
theorem Filter.Tendsto.atBot_of_add_const {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => f x + C) l atBot) :
Tendsto f l atBot
source
@[deprecated Filter.Tendsto.atBot_of_add_const (since := "2025-02-13")]
theorem Filter.tendsto_atBot_of_add_const_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f : α → M} (C : M) (hf : Tendsto (fun (x : α) => f x + C) l atBot) :
Tendsto f l atBot

Alias of Filter.Tendsto.atBot_of_add_const.

source
theorem Filter.Tendsto.atTop_of_isBoundedUnder_le_mul {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l f) (hfg : Tendsto (fun (x : α) => f x * g x) l atTop) :
Tendsto g l atTop

If f is eventually bounded from above along l and f * g tends to +∞, then g tends to +∞.

source
theorem Filter.Tendsto.atTop_of_isBoundedUnder_le_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l f) (hfg : Tendsto (fun (x : α) => f x + g x) l atTop) :
Tendsto g l atTop

If f is eventually bounded from above along l and f + g tends to +∞, then g tends to +∞.

source
theorem Filter.Tendsto.atBot_of_isBoundedUnder_ge_mul {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l f) (h : Tendsto (fun (x : α) => f x * g x) l atBot) :
Tendsto g l atBot
source
theorem Filter.Tendsto.atBot_of_isBoundedUnder_ge_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l f) (h : Tendsto (fun (x : α) => f x + g x) l atBot) :
Tendsto g l atBot
source
theorem Filter.Tendsto.atTop_of_le_const_mul {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hf : ∃ (C : M), ∀ (x : α), f x ≤ C) (hfg : Tendsto (fun (x : α) => f x * g x) l atTop) :
Tendsto g l atTop
source
theorem Filter.Tendsto.atTop_of_le_const_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hf : ∃ (C : M), ∀ (x : α), f x ≤ C) (hfg : Tendsto (fun (x : α) => f x + g x) l atTop) :
Tendsto g l atTop
source
theorem Filter.Tendsto.atBot_of_const_le_mul {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hf : ∃ (C : M), ∀ (x : α), C ≤ f x) (hfg : Tendsto (fun (x : α) => f x * g x) l atBot) :
Tendsto g l atBot
source
theorem Filter.Tendsto.atBot_of_const_le_add {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hf : ∃ (C : M), ∀ (x : α), C ≤ f x) (hfg : Tendsto (fun (x : α) => f x + g x) l atBot) :
Tendsto g l atBot
source
theorem Filter.Tendsto.atTop_of_mul_isBoundedUnder_le {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l g) (h : Tendsto (fun (x : α) => f x * g x) l atTop) :
Tendsto f l atTop
source
theorem Filter.Tendsto.atTop_of_add_isBoundedUnder_le {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l g) (h : Tendsto (fun (x : α) => f x + g x) l atTop) :
Tendsto f l atTop
source
theorem Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l g) (h : Tendsto (fun (x : α) => f x * g x) l atBot) :
Tendsto f l atBot
source
theorem Filter.Tendsto.atBot_of_add_isBoundedUnder_ge {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l g) (h : Tendsto (fun (x : α) => f x + g x) l atBot) :
Tendsto f l atBot
source
theorem Filter.Tendsto.atTop_of_mul_le_const {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hg : ∃ (C : M), ∀ (x : α), g x ≤ C) (hfg : Tendsto (fun (x : α) => f x * g x) l atTop) :
Tendsto f l atTop
source
theorem Filter.Tendsto.atTop_of_add_le_const {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hg : ∃ (C : M), ∀ (x : α), g x ≤ C) (hfg : Tendsto (fun (x : α) => f x + g x) l atTop) :
Tendsto f l atTop
source
theorem Filter.Tendsto.atBot_of_mul_const_le {α : Type u_1} {M : Type u_2} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {l : Filter α} {f g : α → M} (hg : ∃ (C : M), ∀ (x : α), C ≤ g x) (hfg : Tendsto (fun (x : α) => f x * g x) l atBot) :
Tendsto f l atBot
source
theorem Filter.Tendsto.atBot_of_add_const_le {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (hg : ∃ (C : M), ∀ (x : α), C ≤ g x) (hfg : Tendsto (fun (x : α) => f x + g x) l atBot) :
Tendsto f l atBot
source
@[deprecated Filter.Tendsto.atTop_of_isBoundedUnder_le_add (since := "2025-02-13")]
theorem Filter.tendsto_atTop_of_add_bdd_above_left' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ᶠ (x : α) in l, f x ≤ C) (h : Tendsto (fun (x : α) => f x + g x) l atTop) :
Tendsto g l atTop
source
@[deprecated Filter.Tendsto.atBot_of_isBoundedUnder_ge_add (since := "2025-02-13")]
theorem Filter.tendsto_atBot_of_add_bdd_below_left' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ᶠ (x : α) in l, C ≤ f x) (h : Tendsto (fun (x : α) => f x + g x) l atBot) :
Tendsto g l atBot
source
@[deprecated Filter.Tendsto.atTop_of_le_const_add (since := "2025-02-13")]
theorem Filter.tendsto_atTop_of_add_bdd_above_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ (x : α), f x ≤ C) :
Tendsto (fun (x : α) => f x + g x) l atTop → Tendsto g l atTop
source
@[deprecated Filter.Tendsto.atBot_of_const_le_add (since := "2025-02-13")]
theorem Filter.tendsto_atBot_of_add_bdd_below_left {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ (x : α), C ≤ f x) :
Tendsto (fun (x : α) => f x + g x) l atBot → Tendsto g l atBot
source
@[deprecated Filter.Tendsto.atTop_of_add_isBoundedUnder_le (since := "2025-02-13")]
theorem Filter.tendsto_atTop_of_add_bdd_above_right' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ᶠ (x : α) in l, g x ≤ C) (h : Tendsto (fun (x : α) => f x + g x) l atTop) :
Tendsto f l atTop
source
@[deprecated Filter.Tendsto.atBot_of_add_isBoundedUnder_ge (since := "2025-02-13")]
theorem Filter.tendsto_atBot_of_add_bdd_below_right' {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ᶠ (x : α) in l, C ≤ g x) (h : Tendsto (fun (x : α) => f x + g x) l atBot) :
Tendsto f l atBot
source
@[deprecated Filter.Tendsto.atTop_of_add_le_const (since := "2025-02-13")]
theorem Filter.tendsto_atTop_of_add_bdd_above_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ (x : α), g x ≤ C) :
Tendsto (fun (x : α) => f x + g x) l atTop → Tendsto f l atTop
source
@[deprecated Filter.Tendsto.atBot_of_add_const_le (since := "2025-02-13")]
theorem Filter.tendsto_atBot_of_add_bdd_below_right {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {l : Filter α} {f g : α → M} (C : M) (hC : ∀ (x : α), C ≤ g x) :
Tendsto (fun (x : α) => f x + g x) l atBot → Tendsto f l atBot