mathlib documentation

order.filter.at_top_bot

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

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
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
theorem filter.mem_at_top {α : Type u_3} [preorder α] (a : α) :
{b : α | a b} filter.at_top
theorem filter.Ioi_mem_at_top {α : Type u_3} [preorder α] [no_top_order α] (x : α) :
theorem filter.mem_at_bot {α : Type u_3} [preorder α] (a : α) :
{b : α | b a} filter.at_bot
theorem filter.Iio_mem_at_bot {α : Type u_3} [preorder α] [no_bot_order α] (x : α) :
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]
theorem filter.at_top_ne_bot {α : Type u_3} [nonempty α] [semilattice_sup α] :
@[instance]
theorem filter.at_bot_ne_bot {α : Type u_3} [nonempty α] [semilattice_inf α] :
@[simp]
theorem filter.mem_at_top_sets {α : Type u_3} [nonempty α] [semilattice_sup α] {s : set α} :
s filter.at_top ∃ (a : α), ∀ (b : α), b ab s
@[simp]
theorem filter.mem_at_bot_sets {α : Type u_3} [nonempty α] [semilattice_inf α] {s : set α} :
s filter.at_bot ∃ (a : α), ∀ (b : α), b ab 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 ap 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 ap b
theorem filter.eventually_ge_at_top {α : Type u_3} [preorder α] (a : α) :
∀ᶠ (x : α) in filter.at_top, a x
theorem filter.eventually_le_at_bot {α : Type u_3} [preorder α] (a : α) :
∀ᶠ (x : α) in filter.at_bot, x a
theorem filter.eventually_gt_at_top {α : Type u_3} [preorder α] [no_top_order α] (a : α) :
∀ᶠ (x : α) in filter.at_top, a < x
theorem filter.eventually_lt_at_bot {α : Type u_3} [preorder α] [no_bot_order α] (a : α) :
∀ᶠ (x : α) in filter.at_bot, x < a
theorem filter.at_top_basis_Ioi {α : Type u_3} [nonempty α] [semilattice_sup α] [no_top_order α] :
theorem filter.tendsto_at_top_pure {α : Type u_3} {β : Type u_4} [order_top α] (f : α → β) :
theorem filter.tendsto_at_bot_pure {α : Type u_3} {β : Type u_4} [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 ap 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 ap 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_top_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_bot_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 : α), 𝓟 (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 : α), 𝓟 (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) :

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 NP 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_top_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_bot_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_top_order β] {u : → β} (hu : filter.tendsto u filter.at_top filter.at_top) (N : ) :
∃ (n : ) (H : n N), ∀ (k : ), k < nu 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_bot_order β] {u : → β} (hu : filter.tendsto u filter.at_top filter.at_bot) (N : ) :
∃ (n : ) (H : n N), ∀ (k : ), k < nu 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_top_order β] {u : → β} (hu : filter.tendsto u filter.at_top filter.at_top) :
∃ᶠ (n : ) in filter.at_top, ∀ (k : ), k < nu 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_bot_order β] {u : → β} (hu : filter.tendsto u filter.at_top filter.at_bot) :
∃ᶠ (n : ) in filter.at_top, ∀ (k : ), k < nu 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_tendsto_at_top {β : Type u_1} [linear_order β] [no_top_order β] {u : → β} (hu : filter.tendsto u filter.at_top filter.at_top) :
∃ (φ : ), strict_mono φ strict_mono (u φ)
theorem filter.strict_mono_subseq_of_id_le {u : } (hu : ∀ (n : ), n u n) :
∃ (φ : ), strict_mono φ strict_mono (u φ)
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) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_topfilter.tendsto g 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 : α), C f x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_botfilter.tendsto g 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 : α) 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) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_topfilter.tendsto f 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 : α), C g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_botfilter.tendsto f 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 : α) 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
theorem filter.tendsto.at_top_mul_at_top {α : Type u_3} {β : Type u_4} [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} [ordered_semiring α] {n : } (hn : 1 n) :

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} [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} [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} [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) :
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
theorem filter.tendsto.const_mul_at_top {α : Type u_3} {β : Type u_4} [linear_ordered_field α] {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_field α] {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_field α] {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.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_const_mul_pow_at_top {α : Type u_3} [linear_ordered_field α] {c : α} {n : } (hn : 1 n) (hc : 0 < c) :
theorem filter.tendsto_const_mul_pow_at_top_iff {α : Type u_3} [linear_ordered_field α] (c : α) (n : ) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_top 1 n 0 < c
theorem filter.tendsto_neg_const_mul_pow_at_top {α : Type u_3} [linear_ordered_field α] {c : α} {n : } (hn : 1 n) (hc : c < 0) :
theorem filter.tendsto_neg_const_mul_pow_at_top_iff {α : Type u_3} [linear_ordered_field α] (c : α) (n : ) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_bot 1 n 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 af 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 af 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 (𝓟 s) ∃ (N : β), ∀ (n : β), n Nf 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 (𝓟 s) ∃ (N : β), ∀ (n : β), n Nf 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 ab 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 af 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 ib 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 if 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) :
filter.tendsto f filter.at_top filter.at_top ∀ (b : β), ∃ (a : α), b f a
theorem filter.tendsto_at_bot_at_bot_iff_of_monotone {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] {f : α → β} (hf : monotone f) :
filter.tendsto f filter.at_bot filter.at_bot ∀ (b : β), ∃ (a : α), f a b
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 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 tendsto_at_bot_at_bot_of_monotone.

theorem monotone.tendsto_at_top_at_top_iff {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] {f : α → β} (hf : monotone f) :
filter.tendsto f filter.at_top filter.at_top ∀ (b : β), ∃ (a : α), b f a

Alias of tendsto_at_top_at_top_iff_of_monotone.

theorem monotone.tendsto_at_bot_at_bot_iff {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] {f : α → β} (hf : monotone f) :
filter.tendsto f filter.at_bot filter.at_bot ∀ (b : β), ∃ (a : α), f a b

Alias of tendsto_at_bot_at_bot_iff_of_monotone.

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.at_top_finset_eq_infi {α : Type u_3} :
filter.at_top = ⨅ (x : α), 𝓟 (set.Ici {x})
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 tendsto_at_top_finset_of_monotone.

theorem filter.tendsto_finset_image_at_top_at_top {β : Type u_4} {γ : Type u_5} {i : β → γ} {j : γ → β} (h : function.left_inverse j i) :
theorem filter.tendsto_finset_preimage_at_top_at_top {α : Type u_3} {β : Type u_4} {f : α → β} (hf : function.injective f) :
theorem filter.prod_at_top_at_top_eq {β₁ : Type u_1} {β₂ : Type u_2} [semilattice_sup β₁] [semilattice_sup β₂] :
theorem filter.prod_at_bot_at_bot_eq {β₁ : Type u_1} {β₂ : Type u_2} [semilattice_inf β₁] [semilattice_inf β₂] :
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_at_bot_diagonal {α : Type u_3} [semilattice_inf α] :
theorem filter.tendsto_at_top_diagonal {α : Type u_3} [semilattice_sup α] :
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 al ap (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 ka lp (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 ap (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 ap (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_top_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_bot_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) :
theorem filter.tendsto_at_top_at_top_of_monotone' {ι : Type u_1} {α : Type u_3} [preorder ι] [linear_order α] {u : ι → α} (h : monotone u) (H : ¬bdd_above (set.range u)) :

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.

theorem filter.tendsto_at_bot_at_bot_of_monotone' {ι : Type u_1} {α : Type u_3} [preorder ι] [linear_order α] {u : ι → α} (h : monotone u) (H : ¬bdd_below (set.range u)) :

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.

theorem filter.unbounded_of_tendsto_at_top {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] [no_top_order β] {f : α → β} (h : filter.tendsto f filter.at_top filter.at_top) :
theorem filter.unbounded_of_tendsto_at_bot {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] [no_bot_order β] {f : α → β} (h : filter.tendsto f filter.at_top filter.at_bot) :
theorem filter.unbounded_of_tendsto_at_top' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] [no_top_order β] {f : α → β} (h : filter.tendsto f filter.at_bot filter.at_top) :
theorem filter.unbounded_of_tendsto_at_bot' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] [no_bot_order β] {f : α → β} (h : filter.tendsto f filter.at_bot filter.at_bot) :
theorem filter.tendsto_at_top_of_monotone_of_filter {ι : Type u_1} {α : Type u_3} [preorder ι] [preorder α] {l : filter ι} {u : ι → α} (h : monotone u) [l.ne_bot] (hu : filter.tendsto u l filter.at_top) :

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

theorem filter.tendsto_at_bot_of_monotone_of_filter {ι : Type u_1} {α : Type u_3} [preorder ι] [preorder α] {l : filter ι} {u : ι → α} (h : monotone u) [l.ne_bot] (hu : filter.tendsto u l filter.at_bot) :

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' ∏ (x : γ) in u', g x = ∏ (b : β) in v', f b)) :
filter.map (λ (s : finset β), ∏ (b : β) in s, f b) filter.at_top filter.map (λ (s : finset γ), ∏ (x : γ) in s, 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' ∑ (x : γ) in u', g x = ∑ (b : β) in v', f b)) :
filter.map (λ (s : finset β), ∑ (b : β) in s, f b) filter.at_top filter.map (λ (s : finset γ), ∑ (x : γ) in s, g x) filter.at_top
theorem filter.has_antitone_basis.tendsto {ι : Type u_1} {α : Type u_3} [semilattice_sup ι] [nonempty ι] {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_antitone_basis p s) {φ : ι → α} (h : ∀ (i : ι), φ i s i) :
theorem filter.is_countably_generated.tendsto_iff_seq_tendsto {α : Type u_3} {β : Type u_4} {f : α → β} {k : filter α} {l : filter β} (hcb : 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.is_countably_generated.tendsto_of_seq_tendsto {α : Type u_3} {β : Type u_4} {f : α → β} {k : filter α} {l : filter β} (hcb : k.is_countably_generated) :
(∀ (x : → α), filter.tendsto x filter.at_top kfilter.tendsto (f x) filter.at_top l)filter.tendsto f k l
theorem filter.is_countably_generated.subseq_tendsto {α : Type u_3} {f : filter α} (hf : f.is_countably_generated) {u : → α} (hx : (f filter.map u filter.at_top).ne_bot) :
∃ (θ : ), strict_mono θ filter.tendsto (u θ) filter.at_top f
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
@[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 β) :
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 gf x = 0) :
filter.map (λ (s : finset γ), ∑ (i : γ) in s, f (g i)) filter.at_top = filter.map (λ (s : finset β), ∑ (i : β) in s, 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 gf x = 1) :
filter.map (λ (s : finset γ), ∏ (i : γ) in s, f (g i)) filter.at_top = filter.map (λ (s : finset β), ∏ (i : β) in s, 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.