Convergence to ±infinity in ordered commutative monoids #
@[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}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : 0 ≤ᶠ[l] f)
(hg : Tendsto g l atTop)
:
@[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}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : f ≤ᶠ[l] 0)
(hg : Tendsto g l atBot)
:
@[deprecated Filter.Tendsto.nonneg_add_atTop (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_add_nonneg_left
{α : Type u_1}
{M : Type u_2}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∀ (x : α), 0 ≤ f x)
(hg : Tendsto g l atTop)
:
Alias of Filter.Tendsto.nonneg_add_atTop.
@[deprecated Filter.Tendsto.nonpos_add_atBot (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_add_nonpos_left
{α : Type u_1}
{M : Type u_2}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∀ (x : α), f x ≤ 0)
(hg : Tendsto g l atBot)
:
Alias of Filter.Tendsto.nonpos_add_atBot.
@[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}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : 0 ≤ᶠ[l] g)
:
@[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}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : g ≤ᶠ[l] 0)
:
@[deprecated Filter.Tendsto.atTop_add_nonneg (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_add_nonneg_right
{α : Type u_1}
{M : Type u_2}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : ∀ (x : α), 0 ≤ g x)
:
Alias of Filter.Tendsto.atTop_add_nonneg.
@[deprecated Filter.Tendsto.atBot_add_nonpos (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_add_nonpos_right
{α : Type u_1}
{M : Type u_2}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : ∀ (x : α), g x ≤ 0)
:
Alias of Filter.Tendsto.atBot_add_nonpos.
theorem
Filter.Tendsto.atTop_mul_atTop
{α : Type u_1}
{M : Type u_2}
[OrderedCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : Tendsto g 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₀.
@[deprecated Filter.Tendsto.atTop_add_atTop (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_add
{α : Type u_1}
{M : Type u_2}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : Tendsto g l atTop)
:
Alias of Filter.Tendsto.atTop_add_atTop.
theorem
Filter.Tendsto.atBot_mul_atBot
{α : Type u_1}
{M : Type u_2}
[OrderedCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : Tendsto g 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₀.
@[deprecated Filter.Tendsto.atBot_add_atBot (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_add
{α : Type u_1}
{M : Type u_2}
[OrderedAddCommMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : Tendsto g l atBot)
:
Alias of Filter.Tendsto.atBot_add_atBot.
theorem
Filter.Tendsto.atTop_of_const_mul
{α : Type u_1}
{M : Type u_2}
[OrderedCancelCommMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C * f x) 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₀.
@[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}
[OrderedCancelAddCommMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C + f x) l atTop)
:
Alias of Filter.Tendsto.atTop_of_const_add.
@[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}
[OrderedCancelAddCommMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C + f x) l atBot)
:
Alias of Filter.Tendsto.atBot_of_const_add.
theorem
Filter.Tendsto.atTop_of_mul_const
{α : Type u_1}
{M : Type u_2}
[OrderedCancelCommMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x * C) 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₀.
@[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}
[OrderedCancelAddCommMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x + C) l atTop)
:
Alias of Filter.Tendsto.atTop_of_add_const.
@[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}
[OrderedCancelAddCommMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x + C) l atBot)
:
Alias of Filter.Tendsto.atBot_of_add_const.
theorem
Filter.Tendsto.atTop_of_isBoundedUnder_le_mul
{α : Type u_1}
{M : Type u_2}
[OrderedCancelCommMonoid 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)
:
If f is eventually bounded from above along l and f * g tends to +∞,
then g tends to +∞.
theorem
Filter.Tendsto.atTop_of_isBoundedUnder_le_add
{α : Type u_1}
{M : Type u_2}
[OrderedCancelAddCommMonoid 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)
:
If f is eventually bounded from above along l and f + g tends to +∞,
then g tends to +∞.
theorem
Filter.Tendsto.atBot_of_isBoundedUnder_ge_mul
{α : Type u_1}
{M : Type u_2}
[OrderedCancelCommMonoid 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)
:
theorem
Filter.Tendsto.atBot_of_isBoundedUnder_ge_add
{α : Type u_1}
{M : Type u_2}
[OrderedCancelAddCommMonoid 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)
:
theorem
Filter.Tendsto.atTop_of_mul_isBoundedUnder_le
{α : Type u_1}
{M : Type u_2}
[OrderedCancelCommMonoid 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)
:
theorem
Filter.Tendsto.atTop_of_add_isBoundedUnder_le
{α : Type u_1}
{M : Type u_2}
[OrderedCancelAddCommMonoid 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)
:
theorem
Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge
{α : Type u_1}
{M : Type u_2}
[OrderedCancelCommMonoid 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)
:
theorem
Filter.Tendsto.atBot_of_add_isBoundedUnder_ge
{α : Type u_1}
{M : Type u_2}
[OrderedCancelAddCommMonoid 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)
:
@[deprecated Filter.Tendsto.atTop_of_isBoundedUnder_le_add (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atBot_of_isBoundedUnder_ge_add (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atTop_of_le_const_add (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atBot_of_const_le_add (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atTop_of_add_isBoundedUnder_le (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atBot_of_add_isBoundedUnder_ge (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atTop_of_add_le_const (since := "2025-02-13")]
@[deprecated Filter.Tendsto.atBot_of_add_const_le (since := "2025-02-13")]