mathlib3 documentation

order.filter.at_top_bot

at_top and at_bot filters on preorded sets, monoids and groups. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the filters

Then we prove many lemmas like “if f → +∞, then f ± c → +∞”.

def filter.at_top {α : Type u_3} [preorder α] :

at_top is the filter representing the limit → ∞ on an ordered set. It is generated by the collection of up-sets {b | a ≤ b}. (The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element exists.)

Equations
Instances for filter.at_top
def filter.at_bot {α : Type u_3} [preorder α] :

at_bot is the filter representing the limit → -∞ on an ordered set. It is generated by the collection of down-sets {b | b ≤ a}. (The preorder need not have a bottom element for this to be well defined, and indeed is trivial when a bottom element exists.)

Equations
Instances for filter.at_bot
theorem filter.mem_at_top {α : Type u_3} [preorder α] (a : α) :
{b : α | a b} filter.at_top
theorem filter.Ici_mem_at_top {α : Type u_3} [preorder α] (a : α) :
theorem filter.Ioi_mem_at_top {α : Type u_3} [preorder α] [no_max_order α] (x : α) :
theorem filter.mem_at_bot {α : Type u_3} [preorder α] (a : α) :
{b : α | b a} filter.at_bot
theorem filter.Iic_mem_at_bot {α : Type u_3} [preorder α] (a : α) :
theorem filter.Iio_mem_at_bot {α : Type u_3} [preorder α] [no_min_order α] (x : α) :
theorem filter.not_tendsto_const_at_top {α : Type u_3} {β : Type u_4} [preorder α] [no_max_order α] (x : α) (l : filter β) [l.ne_bot] :
¬filter.tendsto (λ (_x : β), x) l filter.at_top
theorem filter.not_tendsto_const_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [no_min_order α] (x : α) (l : filter β) [l.ne_bot] :
¬filter.tendsto (λ (_x : β), x) l filter.at_bot
theorem filter.at_top_basis {α : Type u_3} [nonempty α] [semilattice_sup α] :
theorem filter.at_top_basis' {α : Type u_3} [semilattice_sup α] (a : α) :
filter.at_top.has_basis (λ (x : α), a x) set.Ici
theorem filter.at_bot_basis {α : Type u_3} [nonempty α] [semilattice_inf α] :
theorem filter.at_bot_basis' {α : Type u_3} [semilattice_inf α] (a : α) :
filter.at_bot.has_basis (λ (x : α), x a) set.Iic
@[instance]
@[instance]
@[simp]
theorem filter.mem_at_top_sets {α : Type u_3} [nonempty α] [semilattice_sup α] {s : set α} :
s filter.at_top (a : α), (b : α), b a b s
@[simp]
theorem filter.mem_at_bot_sets {α : Type u_3} [nonempty α] [semilattice_inf α] {s : set α} :
s filter.at_bot (a : α), (b : α), b a b s
@[simp]
theorem filter.eventually_at_top {α : Type u_3} [semilattice_sup α] [nonempty α] {p : α Prop} :
(∀ᶠ (x : α) in filter.at_top, p x) (a : α), (b : α), b a p b
@[simp]
theorem filter.eventually_at_bot {α : Type u_3} [semilattice_inf α] [nonempty α] {p : α Prop} :
(∀ᶠ (x : α) in filter.at_bot, p x) (a : α), (b : α), b a p b
theorem filter.eventually_ge_at_top {α : Type u_3} [preorder α] (a : α) :
theorem filter.eventually_le_at_bot {α : Type u_3} [preorder α] (a : α) :
theorem filter.eventually_gt_at_top {α : Type u_3} [preorder α] [no_max_order α] (a : α) :
∀ᶠ (x : α) in filter.at_top, a < x
theorem filter.eventually_ne_at_top {α : Type u_3} [preorder α] [no_max_order α] (a : α) :
theorem filter.tendsto.eventually_gt_at_top {α : Type u_3} {β : Type u_4} [preorder β] [no_max_order β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_top) (c : β) :
∀ᶠ (x : α) in l, c < f x
theorem filter.tendsto.eventually_ge_at_top {α : Type u_3} {β : Type u_4} [preorder β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_top) (c : β) :
∀ᶠ (x : α) in l, c f x
theorem filter.tendsto.eventually_ne_at_top {α : Type u_3} {β : Type u_4} [preorder β] [no_max_order β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_top) (c : β) :
∀ᶠ (x : α) in l, f x c
theorem filter.tendsto.eventually_ne_at_top' {α : Type u_3} {β : Type u_4} [preorder β] [no_max_order β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_top) (c : α) :
∀ᶠ (x : α) in l, x c
theorem filter.eventually_lt_at_bot {α : Type u_3} [preorder α] [no_min_order α] (a : α) :
∀ᶠ (x : α) in filter.at_bot, x < a
theorem filter.eventually_ne_at_bot {α : Type u_3} [preorder α] [no_min_order α] (a : α) :
theorem filter.tendsto.eventually_lt_at_bot {α : Type u_3} {β : Type u_4} [preorder β] [no_min_order β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_bot) (c : β) :
∀ᶠ (x : α) in l, f x < c
theorem filter.tendsto.eventually_le_at_bot {α : Type u_3} {β : Type u_4} [preorder β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_bot) (c : β) :
∀ᶠ (x : α) in l, f x c
theorem filter.tendsto.eventually_ne_at_bot {α : Type u_3} {β : Type u_4} [preorder β] [no_min_order β] {f : α β} {l : filter α} (hf : filter.tendsto f l filter.at_bot) (c : β) :
∀ᶠ (x : α) in l, f x c
theorem filter.tendsto_at_top_pure {α : Type u_3} {β : Type u_4} [partial_order α] [order_top α] (f : α β) :
theorem filter.tendsto_at_bot_pure {α : Type u_3} {β : Type u_4} [partial_order α] [order_bot α] (f : α β) :
theorem filter.eventually.exists_forall_of_at_top {α : Type u_3} [semilattice_sup α] [nonempty α] {p : α Prop} (h : ∀ᶠ (x : α) in filter.at_top, p x) :
(a : α), (b : α), b a p b
theorem filter.eventually.exists_forall_of_at_bot {α : Type u_3} [semilattice_inf α] [nonempty α] {p : α Prop} (h : ∀ᶠ (x : α) in filter.at_bot, p x) :
(a : α), (b : α), b a p b
theorem filter.frequently_at_top {α : Type u_3} [semilattice_sup α] [nonempty α] {p : α Prop} :
(∃ᶠ (x : α) in filter.at_top, p x) (a : α), (b : α) (H : b a), p b
theorem filter.frequently_at_bot {α : Type u_3} [semilattice_inf α] [nonempty α] {p : α Prop} :
(∃ᶠ (x : α) in filter.at_bot, p x) (a : α), (b : α) (H : b a), p b
theorem filter.frequently_at_top' {α : Type u_3} [semilattice_sup α] [nonempty α] [no_max_order α] {p : α Prop} :
(∃ᶠ (x : α) in filter.at_top, p x) (a : α), (b : α) (H : b > a), p b
theorem filter.frequently_at_bot' {α : Type u_3} [semilattice_inf α] [nonempty α] [no_min_order α] {p : α Prop} :
(∃ᶠ (x : α) in filter.at_bot, p x) (a : α), (b : α) (H : b < a), p b
theorem filter.frequently.forall_exists_of_at_top {α : Type u_3} [semilattice_sup α] [nonempty α] {p : α Prop} (h : ∃ᶠ (x : α) in filter.at_top, p x) (a : α) :
(b : α) (H : b a), p b
theorem filter.frequently.forall_exists_of_at_bot {α : Type u_3} [semilattice_inf α] [nonempty α] {p : α Prop} (h : ∃ᶠ (x : α) in filter.at_bot, p x) (a : α) :
(b : α) (H : b a), p b
theorem filter.map_at_top_eq {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] {f : α β} :
filter.map f filter.at_top = (a : α), filter.principal (f '' {a' : α | a a'})
theorem filter.map_at_bot_eq {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] {f : α β} :
filter.map f filter.at_bot = (a : α), filter.principal (f '' {a' : α | a' a})
theorem filter.tendsto_at_top {α : Type u_3} {β : Type u_4} [preorder β] {m : α β} {f : filter α} :
filter.tendsto m f filter.at_top (b : β), ∀ᶠ (a : α) in f, b m a
theorem filter.tendsto_at_bot {α : Type u_3} {β : Type u_4} [preorder β] {m : α β} {f : filter α} :
filter.tendsto m f filter.at_bot (b : β), ∀ᶠ (a : α) in f, m a b
theorem filter.tendsto_at_top_mono' {α : Type u_3} {β : Type u_4} [preorder β] (l : filter α) ⦃f₁ f₂ : α β⦄ (h : f₁ ≤ᶠ[l] f₂) :
theorem filter.tendsto_at_bot_mono' {α : Type u_3} {β : Type u_4} [preorder β] (l : filter α) ⦃f₁ f₂ : α β⦄ (h : f₁ ≤ᶠ[l] f₂) :
theorem filter.tendsto_at_top_mono {α : Type u_3} {β : Type u_4} [preorder β] {l : filter α} {f g : α β} (h : (n : α), f n g n) :
theorem filter.tendsto_at_bot_mono {α : Type u_3} {β : Type u_4} [preorder β] {l : filter α} {f g : α β} (h : (n : α), f n g n) :
@[simp]
theorem order_iso.comap_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :
@[simp]
theorem order_iso.comap_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :
@[simp]
theorem order_iso.map_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :
@[simp]
theorem order_iso.map_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :
theorem order_iso.tendsto_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :
theorem order_iso.tendsto_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :
@[simp]
theorem order_iso.tendsto_at_top_iff {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] {l : filter γ} {f : γ α} (e : α ≃o β) :
@[simp]
theorem order_iso.tendsto_at_bot_iff {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] {l : filter γ} {f : γ α} (e : α ≃o β) :

Sequences #

theorem filter.inf_map_at_top_ne_bot_iff {α : Type u_3} {β : Type u_4} [semilattice_sup α] [nonempty α] {F : filter β} {u : α β} :
(F filter.map u filter.at_top).ne_bot (U : set β), U F (N : α), (n : α) (H : n N), u n U
theorem filter.inf_map_at_bot_ne_bot_iff {α : Type u_3} {β : Type u_4} [semilattice_inf α] [nonempty α] {F : filter β} {u : α β} :
(F filter.map u filter.at_bot).ne_bot (U : set β), U F (N : α), (n : α) (H : n N), u n U
theorem filter.extraction_of_frequently_at_top' {P : Prop} (h : (N : ), (n : ) (H : n > N), P n) :
(φ : ), strict_mono φ (n : ), P (φ n)
theorem filter.extraction_of_frequently_at_top {P : Prop} (h : ∃ᶠ (n : ) in filter.at_top, P n) :
(φ : ), strict_mono φ (n : ), P (φ n)
theorem filter.extraction_of_eventually_at_top {P : Prop} (h : ∀ᶠ (n : ) in filter.at_top, P n) :
(φ : ), strict_mono φ (n : ), P (φ n)
theorem filter.extraction_forall_of_frequently {P : Prop} (h : (n : ), ∃ᶠ (k : ) in filter.at_top, P n k) :
(φ : ), strict_mono φ (n : ), P n (φ n)
theorem filter.extraction_forall_of_eventually {P : Prop} (h : (n : ), ∀ᶠ (k : ) in filter.at_top, P n k) :
(φ : ), strict_mono φ (n : ), P n (φ n)
theorem filter.extraction_forall_of_eventually' {P : Prop} (h : (n : ), (N : ), (k : ), k N P n k) :
(φ : ), strict_mono φ (n : ), P n (φ n)
theorem filter.exists_le_of_tendsto_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] [preorder β] {u : α β} (h : filter.tendsto u filter.at_top filter.at_top) (a : α) (b : β) :
(a' : α) (H : a' a), b u a'
@[nolint]
theorem filter.exists_le_of_tendsto_at_bot {α : Type u_3} {β : Type u_4} [semilattice_sup α] [preorder β] {u : α β} (h : filter.tendsto u filter.at_top filter.at_bot) (a : α) (b : β) :
(a' : α) (H : a' a), u a' b
theorem filter.exists_lt_of_tendsto_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] [preorder β] [no_max_order β] {u : α β} (h : filter.tendsto u filter.at_top filter.at_top) (a : α) (b : β) :
(a' : α) (H : a' a), b < u a'
@[nolint]
theorem filter.exists_lt_of_tendsto_at_bot {α : Type u_3} {β : Type u_4} [semilattice_sup α] [preorder β] [no_min_order β] {u : α β} (h : filter.tendsto u filter.at_top filter.at_bot) (a : α) (b : β) :
(a' : α) (H : a' a), u a' < b
theorem filter.high_scores {β : Type u_4} [linear_order β] [no_max_order β] {u : β} (hu : filter.tendsto u filter.at_top filter.at_top) (N : ) :
(n : ) (H : n N), (k : ), k < n u k < u n

If u is a sequence which is unbounded above, then after any point, it reaches a value strictly greater than all previous values.

@[nolint]
theorem filter.low_scores {β : Type u_4} [linear_order β] [no_min_order β] {u : β} (hu : filter.tendsto u filter.at_top filter.at_bot) (N : ) :
(n : ) (H : n N), (k : ), k < n u n < u k

If u is a sequence which is unbounded below, then after any point, it reaches a value strictly smaller than all previous values.

theorem filter.frequently_high_scores {β : Type u_4} [linear_order β] [no_max_order β] {u : β} (hu : filter.tendsto u filter.at_top filter.at_top) :
∃ᶠ (n : ) in filter.at_top, (k : ), k < n u k < u n

If u is a sequence which is unbounded above, then it frequently reaches a value strictly greater than all previous values.

theorem filter.frequently_low_scores {β : Type u_4} [linear_order β] [no_min_order β] {u : β} (hu : filter.tendsto u filter.at_top filter.at_bot) :
∃ᶠ (n : ) in filter.at_top, (k : ), k < n u n < u k

If u is a sequence which is unbounded below, then it frequently reaches a value strictly smaller than all previous values.

theorem filter.strict_mono_subseq_of_id_le {u : } (hu : (n : ), n u n) :
theorem filter.tendsto_at_top_add_nonneg_left' {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : ∀ᶠ (x : α) in l, 0 f x) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_nonpos_left' {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : ∀ᶠ (x : α) in l, f x 0) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_nonneg_left {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : (x : α), 0 f x) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_nonpos_left {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : (x : α), f x 0) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_nonneg_right' {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : filter.tendsto f l filter.at_top) (hg : ∀ᶠ (x : α) in l, 0 g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_nonpos_right' {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : filter.tendsto f l filter.at_bot) (hg : ∀ᶠ (x : α) in l, g x 0) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_nonneg_right {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : filter.tendsto f l filter.at_top) (hg : (x : α), 0 g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_nonpos_right {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : filter.tendsto f l filter.at_bot) (hg : (x : α), g x 0) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : filter.tendsto f l filter.at_top) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α β} (hf : filter.tendsto f l filter.at_bot) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto.nsmul_at_top {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f : α β} (hf : filter.tendsto f l filter.at_top) {n : } (hn : 0 < n) :
filter.tendsto (λ (x : α), n f x) l filter.at_top
theorem filter.tendsto.nsmul_at_bot {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f : α β} (hf : filter.tendsto f l filter.at_bot) {n : } (hn : 0 < n) :
filter.tendsto (λ (x : α), n f x) l filter.at_bot
theorem filter.tendsto_at_top_of_add_const_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α β} (C : β) (hf : filter.tendsto (λ (x : α), C + f x) l filter.at_top) :
theorem filter.tendsto_at_bot_of_add_const_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α β} (C : β) (hf : filter.tendsto (λ (x : α), C + f x) l filter.at_bot) :
theorem filter.tendsto_at_top_of_add_const_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α β} (C : β) (hf : filter.tendsto (λ (x : α), f x + C) l filter.at_top) :
theorem filter.tendsto_at_bot_of_add_const_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α β} (C : β) (hf : filter.tendsto (λ (x : α), f x + C) l filter.at_bot) :
theorem filter.tendsto_at_top_of_add_bdd_above_left' {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : ∀ᶠ (x : α) in l, f x C) (h : filter.tendsto (λ (x : α), f x + g x) l filter.at_top) :
theorem filter.tendsto_at_bot_of_add_bdd_below_left' {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : ∀ᶠ (x : α) in l, C f x) (h : filter.tendsto (λ (x : α), f x + g x) l filter.at_bot) :
theorem filter.tendsto_at_top_of_add_bdd_above_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : (x : α), f x C) :
theorem filter.tendsto_at_bot_of_add_bdd_below_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : (x : α), C f x) :
theorem filter.tendsto_at_top_of_add_bdd_above_right' {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : ∀ᶠ (x : α) in l, g x C) (h : filter.tendsto (λ (x : α), f x + g x) l filter.at_top) :
theorem filter.tendsto_at_bot_of_add_bdd_below_right' {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : ∀ᶠ (x : α) in l, C g x) (h : filter.tendsto (λ (x : α), f x + g x) l filter.at_bot) :
theorem filter.tendsto_at_top_of_add_bdd_above_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : (x : α), g x C) :
theorem filter.tendsto_at_bot_of_add_bdd_below_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α β} (C : β) (hC : (x : α), C g x) :
theorem filter.tendsto_at_top_add_left_of_le' {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : ∀ᶠ (x : α) in l, C f x) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_left_of_ge' {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : ∀ᶠ (x : α) in l, f x C) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_left_of_le {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : (x : α), C f x) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_left_of_ge {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : (x : α), f x C) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_right_of_le' {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : filter.tendsto f l filter.at_top) (hg : ∀ᶠ (x : α) in l, C g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_right_of_ge' {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : filter.tendsto f l filter.at_bot) (hg : ∀ᶠ (x : α) in l, g x C) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_right_of_le {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : filter.tendsto f l filter.at_top) (hg : (x : α), C g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem filter.tendsto_at_bot_add_right_of_ge {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f g : α β} (C : β) (hf : filter.tendsto f l filter.at_bot) (hg : (x : α), g x C) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem filter.tendsto_at_top_add_const_left {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α β} (C : β) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : α), C + f x) l filter.at_top
theorem filter.tendsto_at_bot_add_const_left {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α β} (C : β) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : α), C + f x) l filter.at_bot
theorem filter.tendsto_at_top_add_const_right {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α β} (C : β) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : α), f x + C) l filter.at_top
theorem filter.tendsto_at_bot_add_const_right {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α β} (C : β) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : α), f x + C) l filter.at_bot
@[simp]
theorem filter.tendsto_neg_at_top_iff {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] {l : filter α} {f : α β} :
@[simp]
theorem filter.tendsto_neg_at_bot_iff {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] {l : filter α} {f : α β} :
theorem filter.tendsto.at_top_mul_at_top {α : Type u_3} {β : Type u_4} [strict_ordered_semiring α] {l : filter β} {f g : β α} (hf : filter.tendsto f l filter.at_top) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_top
theorem filter.tendsto_pow_at_top {α : Type u_3} [strict_ordered_semiring α] {n : } (hn : n 0) :

The monomial function x^n tends to +∞ at +∞ for any positive natural n. A version for positive real powers exists as tendsto_rpow_at_top.

theorem filter.zero_pow_eventually_eq {α : Type u_3} [monoid_with_zero α] :
(λ (n : ), 0 ^ n) =ᶠ[filter.at_top] λ (n : ), 0
theorem filter.tendsto.at_top_mul_at_bot {α : Type u_3} {β : Type u_4} [strict_ordered_ring α] {l : filter β} {f g : β α} (hf : filter.tendsto f l filter.at_top) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_bot
theorem filter.tendsto.at_bot_mul_at_top {α : Type u_3} {β : Type u_4} [strict_ordered_ring α] {l : filter β} {f g : β α} (hf : filter.tendsto f l filter.at_bot) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_bot
theorem filter.tendsto.at_bot_mul_at_bot {α : Type u_3} {β : Type u_4} [strict_ordered_ring α] {l : filter β} {f g : β α} (hf : filter.tendsto f l filter.at_bot) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), f x * g x) l filter.at_top
theorem filter.tendsto.at_top_of_const_mul {α : Type u_3} {β : Type u_4} [linear_ordered_semiring α] {l : filter β} {f : β α} {c : α} (hc : 0 < c) (hf : filter.tendsto (λ (x : β), c * f x) l filter.at_top) :
theorem filter.tendsto.at_top_of_mul_const {α : Type u_3} {β : Type u_4} [linear_ordered_semiring α] {l : filter β} {f : β α} {c : α} (hc : 0 < c) (hf : filter.tendsto (λ (x : β), f x * c) l filter.at_top) :
@[simp]
theorem filter.nonneg_of_eventually_pow_nonneg {α : Type u_3} [linear_ordered_ring α] {a : α} (h : ∀ᶠ (n : ) in filter.at_top, 0 a ^ n) :
0 a

Multiplication by constant: iff lemmas #

theorem filter.tendsto_const_mul_at_top_of_pos {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) :

If r is a positive constant, then λ x, r * f x tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem filter.tendsto_mul_const_at_top_of_pos {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) :

If r is a positive constant, then λ x, f x * r tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem filter.tendsto_const_mul_at_top_iff_pos {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), r * f x) l filter.at_top 0 < r

If f tends to infinity along a nontrivial filter l, then λ x, r * f x tends to infinity if and only if 0 < r.

theorem filter.tendsto_mul_const_at_top_iff_pos {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), f x * r) l filter.at_top 0 < r

If f tends to infinity along a nontrivial filter l, then λ x, f x * r tends to infinity if and only if 0 < r.

theorem filter.tendsto.const_mul_at_top {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), r * f x) l filter.at_top

If a function tends to infinity along a filter, then this function multiplied by a positive constant (on the left) also tends to infinity. For a version working in or , use filter.tendsto.const_mul_at_top' instead.

theorem filter.tendsto.at_top_mul_const {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), f x * r) l filter.at_top

If a function tends to infinity along a filter, then this function multiplied by a positive constant (on the right) also tends to infinity. For a version working in or , use filter.tendsto.at_top_mul_const' instead.

theorem filter.tendsto.at_top_div_const {α : Type u_3} {β : Type u_4} [linear_ordered_semifield α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), f x / r) l filter.at_top

If a function tends to infinity along a filter, then this function divided by a positive constant also tends to infinity.

theorem filter.tendsto_const_mul_pow_at_top {α : Type u_3} [linear_ordered_semifield α] {c : α} {n : } (hn : n 0) (hc : 0 < c) :
theorem filter.tendsto_const_mul_pow_at_top_iff {α : Type u_3} [linear_ordered_semifield α] {c : α} {n : } :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_top n 0 0 < c
theorem filter.tendsto_const_mul_at_bot_of_pos {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) :

If r is a positive constant, then λ x, r * f x tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem filter.tendsto_mul_const_at_bot_of_pos {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) :

If r is a positive constant, then λ x, f x * r tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem filter.tendsto_const_mul_at_top_of_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) :

If r is a negative constant, then λ x, r * f x tends to infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem filter.tendsto_mul_const_at_top_of_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) :

If r is a negative constant, then λ x, f x * r tends to infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem filter.tendsto_const_mul_at_bot_of_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) :

If r is a negative constant, then λ x, r * f x tends to negative infinity along a filter if and only if f tends to infinity along the same filter.

theorem filter.tendsto_mul_const_at_bot_of_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) :

If r is a negative constant, then λ x, f x * r tends to negative infinity along a filter if and only if f tends to infinity along the same filter.

theorem filter.tendsto_const_mul_at_top_iff {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] :

The function λ x, r * f x tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem filter.tendsto_mul_const_at_top_iff {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] :

The function λ x, f x * r tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem filter.tendsto_const_mul_at_bot_iff {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] :

The function λ x, r * f x tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem filter.tendsto_mul_const_at_bot_iff {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] :

The function λ x, f x * r tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem filter.tendsto_const_mul_at_top_iff_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), r * f x) l filter.at_top r < 0

If f tends to negative infinity along a nontrivial filter l, then λ x, r * f x tends to infinity if and only if r < 0.

theorem filter.tendsto_mul_const_at_top_iff_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), f x * r) l filter.at_top r < 0

If f tends to negative infinity along a nontrivial filter l, then λ x, f x * r tends to infinity if and only if r < 0.

theorem filter.tendsto_const_mul_at_bot_iff_pos {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), r * f x) l filter.at_bot 0 < r

If f tends to negative infinity along a nontrivial filter l, then λ x, r * f x tends to negative infinity if and only if 0 < r.

theorem filter.tendsto_mul_const_at_bot_iff_pos {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), f x * r) l filter.at_bot 0 < r

If f tends to negative infinity along a nontrivial filter l, then λ x, f x * r tends to negative infinity if and only if 0 < r.

theorem filter.tendsto_const_mul_at_bot_iff_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), r * f x) l filter.at_bot r < 0

If f tends to infinity along a nontrivial filter l, then λ x, r * f x tends to negative infinity if and only if r < 0.

theorem filter.tendsto_mul_const_at_bot_iff_neg {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} [l.ne_bot] (h : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), f x * r) l filter.at_bot r < 0

If f tends to infinity along a nontrivial filter l, then λ x, f x * r tends to negative infinity if and only if r < 0.

theorem filter.tendsto.neg_const_mul_at_top {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), r * f x) l filter.at_bot

If a function tends to infinity along a filter, then this function multiplied by a negative constant (on the left) tends to negative infinity.

theorem filter.tendsto.at_top_mul_neg_const {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) (hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), f x * r) l filter.at_bot

If a function tends to infinity along a filter, then this function multiplied by a negative constant (on the right) tends to negative infinity.

theorem filter.tendsto.const_mul_at_bot {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), r * f x) l filter.at_bot

If a function tends to negative infinity along a filter, then this function multiplied by a positive constant (on the left) also tends to negative infinity.

theorem filter.tendsto.at_bot_mul_const {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), f x * r) l filter.at_bot

If a function tends to negative infinity along a filter, then this function multiplied by a positive constant (on the right) also tends to negative infinity.

theorem filter.tendsto.at_bot_div_const {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : 0 < r) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), f x / r) l filter.at_bot

If a function tends to negative infinity along a filter, then this function divided by a positive constant also tends to negative infinity.

theorem filter.tendsto.neg_const_mul_at_bot {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), r * f x) l filter.at_top

If a function tends to negative infinity along a filter, then this function multiplied by a negative constant (on the left) tends to positive infinity.

theorem filter.tendsto.at_bot_mul_neg_const {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {l : filter β} {f : β α} {r : α} (hr : r < 0) (hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), f x * r) l filter.at_top

If a function tends to negative infinity along a filter, then this function multiplied by a negative constant (on the right) tends to positive infinity.

theorem filter.tendsto_neg_const_mul_pow_at_top {α : Type u_3} [linear_ordered_field α] {c : α} {n : } (hn : n 0) (hc : c < 0) :
theorem filter.tendsto_const_mul_pow_at_bot_iff {α : Type u_3} [linear_ordered_field α] {c : α} {n : } :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_bot n 0 c < 0
theorem filter.tendsto_at_top' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] {f : α β} {l : filter β} :
filter.tendsto f filter.at_top l (s : set β), s l ( (a : α), (b : α), b a f b s)
theorem filter.tendsto_at_bot' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] {f : α β} {l : filter β} :
filter.tendsto f filter.at_bot l (s : set β), s l ( (a : α), (b : α), b a f b s)
theorem filter.tendsto_at_top_principal {α : Type u_3} {β : Type u_4} [nonempty β] [semilattice_sup β] {f : β α} {s : set α} :
filter.tendsto f filter.at_top (filter.principal s) (N : β), (n : β), n N f n s
theorem filter.tendsto_at_bot_principal {α : Type u_3} {β : Type u_4} [nonempty β] [semilattice_inf β] {f : β α} {s : set α} :
filter.tendsto f filter.at_bot (filter.principal s) (N : β), (n : β), n N f n s
theorem filter.tendsto_at_top_at_top {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] {f : α β} :
filter.tendsto f filter.at_top filter.at_top (b : β), (i : α), (a : α), i a b f a

A function f grows to +∞ independent of an order-preserving embedding e.

theorem filter.tendsto_at_top_at_bot {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] {f : α β} :
filter.tendsto f filter.at_top filter.at_bot (b : β), (i : α), (a : α), i a f a b
theorem filter.tendsto_at_bot_at_top {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] {f : α β} :
filter.tendsto f filter.at_bot filter.at_top (b : β), (i : α), (a : α), a i b f a
theorem filter.tendsto_at_bot_at_bot {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] {f : α β} :
filter.tendsto f filter.at_bot filter.at_bot (b : β), (i : α), (a : α), a i f a b
theorem filter.tendsto_at_top_at_top_of_monotone {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : α β} (hf : monotone f) (h : (b : β), (a : α), b f a) :
theorem filter.tendsto_at_bot_at_bot_of_monotone {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : α β} (hf : monotone f) (h : (b : β), (a : α), f a b) :
theorem filter.tendsto_at_top_at_top_iff_of_monotone {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] {f : α β} (hf : monotone f) :
theorem filter.tendsto_at_bot_at_bot_iff_of_monotone {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] {f : α β} (hf : monotone f) :
theorem monotone.tendsto_at_top_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : α β} (hf : monotone f) (h : (b : β), (a : α), b f a) :

Alias of filter.tendsto_at_top_at_top_of_monotone.

theorem monotone.tendsto_at_bot_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : α β} (hf : monotone f) (h : (b : β), (a : α), f a b) :

Alias of filter.tendsto_at_bot_at_bot_of_monotone.

theorem filter.comap_embedding_at_top {β : Type u_4} {γ : Type u_5} [preorder β] [preorder γ] {e : β γ} (hm : (b₁ b₂ : β), e b₁ e b₂ b₁ b₂) (hu : (c : γ), (b : β), c e b) :
theorem filter.comap_embedding_at_bot {β : Type u_4} {γ : Type u_5} [preorder β] [preorder γ] {e : β γ} (hm : (b₁ b₂ : β), e b₁ e b₂ b₁ b₂) (hu : (c : γ), (b : β), e b c) :
theorem filter.tendsto_at_top_embedding {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder β] [preorder γ] {f : α β} {e : β γ} {l : filter α} (hm : (b₁ b₂ : β), e b₁ e b₂ b₁ b₂) (hu : (c : γ), (b : β), c e b) :
theorem filter.tendsto_at_bot_embedding {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder β] [preorder γ] {f : α β} {e : β γ} {l : filter α} (hm : (b₁ b₂ : β), e b₁ e b₂ b₁ b₂) (hu : (c : γ), (b : β), e b c) :

A function f goes to -∞ independent of an order-preserving embedding e.

theorem filter.tendsto_at_top_finset_of_monotone {α : Type u_3} {β : Type u_4} [preorder β] {f : β finset α} (h : monotone f) (h' : (x : α), (n : β), x f n) :

If f is a monotone sequence of finsets and each x belongs to one of f n, then tendsto f at_top at_top.

theorem monotone.tendsto_at_top_finset {α : Type u_3} {β : Type u_4} [preorder β] {f : β finset α} (h : monotone f) (h' : (x : α), (n : β), x f n) :

Alias of filter.tendsto_at_top_finset_of_monotone.

theorem filter.prod_map_at_top_eq {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} [semilattice_sup β₁] [semilattice_sup β₂] (u₁ : β₁ α₁) (u₂ : β₂ α₂) :
theorem filter.prod_map_at_bot_eq {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} [semilattice_inf β₁] [semilattice_inf β₂] (u₁ : β₁ α₁) (u₂ : β₂ α₂) :
theorem filter.tendsto.subseq_mem {α : Type u_3} {F : filter α} {V : set α} (h : (n : ), V n F) {u : α} (hu : filter.tendsto u filter.at_top F) :
(φ : ), strict_mono φ (n : ), u (φ n) V n
theorem filter.tendsto.prod_map_prod_at_bot {α : Type u_3} {β : Type u_4} {γ : Type u_5} [semilattice_inf γ] {F : filter α} {G : filter β} {f : α γ} {g : β γ} (hf : filter.tendsto f F filter.at_bot) (hg : filter.tendsto g G filter.at_bot) :
theorem filter.tendsto.prod_map_prod_at_top {α : Type u_3} {β : Type u_4} {γ : Type u_5} [semilattice_sup γ] {F : filter α} {G : filter β} {f : α γ} {g : β γ} (hf : filter.tendsto f F filter.at_top) (hg : filter.tendsto g G filter.at_top) :
theorem filter.eventually_at_bot_prod_self {α : Type u_3} [semilattice_inf α] [nonempty α] {p : α × α Prop} :
(∀ᶠ (x : α × α) in filter.at_bot, p x) (a : α), (k l : α), k a l a p (k, l)
theorem filter.eventually_at_top_prod_self {α : Type u_3} [semilattice_sup α] [nonempty α] {p : α × α Prop} :
(∀ᶠ (x : α × α) in filter.at_top, p x) (a : α), (k l : α), a k a l p (k, l)
theorem filter.eventually_at_bot_prod_self' {α : Type u_3} [semilattice_inf α] [nonempty α] {p : α × α Prop} :
(∀ᶠ (x : α × α) in filter.at_bot, p x) (a : α), (k : α), k a (l : α), l a p (k, l)
theorem filter.eventually_at_top_prod_self' {α : Type u_3} [semilattice_sup α] [nonempty α] {p : α × α Prop} :
(∀ᶠ (x : α × α) in filter.at_top, p x) (a : α), (k : α), k a (l : α), l a p (k, l)
theorem filter.eventually_at_top_curry {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] {p : α × β Prop} (hp : ∀ᶠ (x : α × β) in filter.at_top, p x) :
∀ᶠ (k : α) in filter.at_top, ∀ᶠ (l : β) in filter.at_top, p (k, l)
theorem filter.eventually_at_bot_curry {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] {p : α × β Prop} (hp : ∀ᶠ (x : α × β) in filter.at_bot, p x) :
∀ᶠ (k : α) in filter.at_bot, ∀ᶠ (l : β) in filter.at_bot, p (k, l)
theorem filter.map_at_top_eq_of_gc {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] {f : α β} (g : β α) (b' : β) (hf : monotone f) (gc : (a : α) (b : β), b b' (f a b a g b)) (hgi : (b : β), b b' b f (g b)) :

A function f maps upwards closed sets (at_top sets) to upwards closed sets when it is a Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an insertion and a connetion above b'.

theorem filter.map_at_bot_eq_of_gc {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] {f : α β} (g : β α) (b' : β) (hf : monotone f) (gc : (a : α) (b : β), b b' (b f a g b a)) (hgi : (b : β), b b' f (g b) b) :
@[simp]

The image of the filter at_top on Ici a under the coercion equals at_top.

@[simp]

The image of the filter at_top on Ioi a under the coercion equals at_top.

The at_top filter for an open interval Ioi a comes from the at_top filter in the ambient order.

The at_top filter for an open interval Ici a comes from the at_top filter in the ambient order.

@[simp]

The at_bot filter for an open interval Iio a comes from the at_bot filter in the ambient order.

The at_bot filter for an open interval Iio a comes from the at_bot filter in the ambient order.

@[simp]

The at_bot filter for an open interval Iic a comes from the at_bot filter in the ambient order.

The at_bot filter for an open interval Iic a comes from the at_bot filter in the ambient order.

theorem filter.tendsto_Ioi_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] {a : α} {f : β (set.Ioi a)} {l : filter β} :
theorem filter.tendsto_Iio_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] {a : α} {f : β (set.Iio a)} {l : filter β} :
theorem filter.tendsto_Ici_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] {a : α} {f : β (set.Ici a)} {l : filter β} :
theorem filter.tendsto_Iic_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] {a : α} {f : β (set.Iic a)} {l : filter β} :
@[simp]
theorem filter.tendsto_comp_coe_Ioi_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] [no_max_order α] {a : α} {f : α β} {l : filter β} :
@[simp]
theorem filter.tendsto_comp_coe_Ici_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] {a : α} {f : α β} {l : filter β} :
@[simp]
theorem filter.tendsto_comp_coe_Iio_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] [no_min_order α] {a : α} {f : α β} {l : filter β} :
@[simp]
theorem filter.tendsto_comp_coe_Iic_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] {a : α} {f : α β} {l : filter β} :
theorem filter.tendsto_add_at_top_iff_nat {α : Type u_3} {f : α} {l : filter α} (k : ) :
theorem filter.map_div_at_top_eq_nat (k : ) (hk : 0 < k) :

If u is a monotone function with linear ordered codomain and the range of u is not bounded above, then tendsto u at_top at_top.

If u is a monotone function with linear ordered codomain and the range of u is not bounded below, then tendsto u at_bot at_bot.

If a monotone function u : ι → α tends to at_top along some non-trivial filter l, then it tends to at_top along at_top.

If a monotone function u : ι → α tends to at_bot along some non-trivial filter l, then it tends to at_bot along at_bot.

theorem filter.tendsto_at_top_of_monotone_of_subseq {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι] [preorder α] {u : ι α} {φ : ι' ι} (h : monotone u) {l : filter ι'} [l.ne_bot] (H : filter.tendsto (u φ) l filter.at_top) :
theorem filter.tendsto_at_bot_of_monotone_of_subseq {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι] [preorder α] {u : ι α} {φ : ι' ι} (h : monotone u) {l : filter ι'} [l.ne_bot] (H : filter.tendsto (u φ) l filter.at_bot) :
theorem filter.map_at_top_finset_prod_le_of_prod_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [comm_monoid α] {f : β α} {g : γ α} (h_eq : (u : finset γ), (v : finset β), (v' : finset β), v v' ( (u' : finset γ), u u' u'.prod (λ (x : γ), g x) = v'.prod (λ (b : β), f b))) :
filter.map (λ (s : finset β), s.prod (λ (b : β), f b)) filter.at_top filter.map (λ (s : finset γ), s.prod (λ (x : γ), g x)) filter.at_top

Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient condition for comparison of the filter at_top.map (λ s, ∏ b in s, f b) with at_top.map (λ s, ∏ b in s, g b). This is useful to compare the set of limit points of Π b in s, f b as s → at_top with the similar set for g.

theorem filter.map_at_top_finset_sum_le_of_sum_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [add_comm_monoid α] {f : β α} {g : γ α} (h_eq : (u : finset γ), (v : finset β), (v' : finset β), v v' ( (u' : finset γ), u u' u'.sum (λ (x : γ), g x) = v'.sum (λ (b : β), f b))) :
filter.map (λ (s : finset β), s.sum (λ (b : β), f b)) filter.at_top filter.map (λ (s : finset γ), s.sum (λ (x : γ), g x)) filter.at_top

Let f and g be two maps to the same commutative additive monoid. This lemma gives a sufficient condition for comparison of the filter at_top.map (λ s, ∑ b in s, f b) with at_top.map (λ s, ∑ b in s, g b). This is useful to compare the set of limit points of ∑ b in s, f b as s → at_top with the similar set for g.

theorem filter.has_antitone_basis.eventually_subset {ι : Type u_1} {α : Type u_3} [preorder ι] {l : filter α} {s : ι set α} (hl : l.has_antitone_basis s) {t : set α} (ht : t l) :
∀ᶠ (i : ι) in filter.at_top, s i t
@[protected]
theorem filter.has_antitone_basis.tendsto {ι : Type u_1} {α : Type u_3} [preorder ι] {l : filter α} {s : ι set α} (hl : l.has_antitone_basis s) {φ : ι α} (h : (i : ι), φ i s i) :
theorem filter.has_antitone_basis.comp_mono {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [semilattice_sup ι] [nonempty ι] [preorder ι'] {l : filter α} {s : ι' set α} (hs : l.has_antitone_basis s) {φ : ι ι'} (φ_mono : monotone φ) (hφ : filter.tendsto φ filter.at_top filter.at_top) :
theorem filter.has_antitone_basis.comp_strict_mono {α : Type u_3} {l : filter α} {s : set α} (hs : l.has_antitone_basis s) {φ : } (hφ : strict_mono φ) :
theorem filter.has_antitone_basis.subbasis_with_rel {α : Type u_3} {f : filter α} {s : set α} (hs : f.has_antitone_basis s) {r : Prop} (hr : (m : ), ∀ᶠ (n : ) in filter.at_top, r m n) :
(φ : ), strict_mono φ ( ⦃m n : ⦄, m < n r (φ m) (φ n)) f.has_antitone_basis (s φ)

Given an antitone basis s : ℕ → set α of a filter, extract an antitone subbasis s ∘ φ, φ : ℕ → ℕ, such that m < n implies r (φ m) (φ n). This lemma can be used to extract an antitone basis with basis sets decreasing "sufficiently fast".

If f is a nontrivial countably generated filter, then there exists a sequence that converges to f.

theorem filter.tendsto_iff_seq_tendsto {α : Type u_3} {β : Type u_4} {f : α β} {k : filter α} {l : filter β} [k.is_countably_generated] :

An abstract version of continuity of sequentially continuous functions on metric spaces: if a filter k is countably generated then tendsto f k l iff for every sequence u converging to k, f ∘ u tends to l.

theorem filter.tendsto_of_seq_tendsto {α : Type u_3} {β : Type u_4} {f : α β} {k : filter α} {l : filter β} [k.is_countably_generated] :
theorem filter.tendsto_iff_forall_eventually_mem {α : Type u_1} {ι : Type u_2} {x : ι α} {f : filter α} {l : filter ι} :
filter.tendsto x l f (s : set α), s f (∀ᶠ (n : ι) in l, x n s)
theorem filter.not_tendsto_iff_exists_frequently_nmem {α : Type u_1} {ι : Type u_2} {x : ι α} {f : filter α} {l : filter ι} :
¬filter.tendsto x l f (s : set α) (H : s f), ∃ᶠ (n : ι) in l, x n s
theorem filter.frequently_iff_seq_frequently {ι : Type u_1} {l : filter ι} {p : ι Prop} [hl : l.is_countably_generated] :
(∃ᶠ (n : ι) in l, p n) (x : ι), filter.tendsto x filter.at_top l ∃ᶠ (n : ) in filter.at_top, p (x n)
theorem filter.eventually_iff_seq_eventually {ι : Type u_1} {l : filter ι} {p : ι Prop} [hl : l.is_countably_generated] :
(∀ᶠ (n : ι) in l, p n) (x : ι), filter.tendsto x filter.at_top l (∀ᶠ (n : ) in filter.at_top, p (x n))
theorem filter.subseq_forall_of_frequently {ι : Type u_1} {x : ι} {p : ι Prop} {l : filter ι} (h_tendsto : filter.tendsto x filter.at_top l) (h : ∃ᶠ (n : ) in filter.at_top, p (x n)) :
(ns : ), filter.tendsto (λ (n : ), x (ns n)) filter.at_top l (n : ), p (x (ns n))
theorem filter.exists_seq_forall_of_frequently {ι : Type u_1} {l : filter ι} {p : ι Prop} [hl : l.is_countably_generated] (h : ∃ᶠ (n : ι) in l, p n) :
(ns : ι), filter.tendsto ns filter.at_top l (n : ), p (ns n)
theorem filter.tendsto_of_subseq_tendsto {α : Type u_1} {ι : Type u_2} {x : ι α} {f : filter α} {l : filter ι} [l.is_countably_generated] (hxy : (ns : ι), filter.tendsto ns filter.at_top l ( (ms : ), filter.tendsto (λ (n : ), x (ns (ms n))) filter.at_top f)) :

A sequence converges if every subsequence has a convergent subsequence.

theorem exists_lt_mul_self {R : Type u_6} [linear_ordered_semiring R] (a : R) :
(x : R) (H : x 0), a < x * x
theorem exists_le_mul_self {R : Type u_6} [linear_ordered_semiring R] (a : R) :
(x : R) (H : x 0), a x * x
theorem function.injective.map_at_top_finset_sum_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [add_comm_monoid α] {g : γ β} (hg : function.injective g) {f : β α} (hf : (x : β), x set.range g f x = 0) :
filter.map (λ (s : finset γ), s.sum (λ (i : γ), f (g i))) filter.at_top = filter.map (λ (s : finset β), s.sum (λ (i : β), f i)) filter.at_top

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to an additive commutative monoid. Suppose that f x = 0 outside of the range of g. Then the filters at_top.map (λ s, ∑ i in s, f (g i)) and at_top.map (λ s, ∑ i in s, f i) coincide.

This lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.

theorem function.injective.map_at_top_finset_prod_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [comm_monoid α] {g : γ β} (hg : function.injective g) {f : β α} (hf : (x : β), x set.range g f x = 1) :
filter.map (λ (s : finset γ), s.prod (λ (i : γ), f (g i))) filter.at_top = filter.map (λ (s : finset β), s.prod (λ (i : β), f i)) filter.at_top

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to a commutative monoid. Suppose that f x = 1 outside of the range of g. Then the filters at_top.map (λ s, ∏ i in s, f (g i)) and at_top.map (λ s, ∏ i in s, f i) coincide.

The additive version of this lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.