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} :
(∀ᶠ (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} :
(∀ᶠ (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₂ : α → β⦄ :

theorem filter.tendsto_at_bot_mono' {α : Type u_3} {β : Type u_4} [preorder β] (l : filter α) ⦃f₁ f₂ : α → β⦄ :

theorem filter.tendsto_at_top_mono {α : Type u_3} {β : Type u_4} [preorder β] {l : filter α} {f g : α → β} :
(∀ (n : α), f n g n)filter.tendsto f l filter.at_topfilter.tendsto g l filter.at_top

theorem filter.tendsto_at_bot_mono {α : Type u_3} {β : Type u_4} [preorder β] {l : filter α} {f g : α → β} :
(∀ (n : α), f n g n)filter.tendsto g l filter.at_botfilter.tendsto f l filter.at_bot

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} :
(∀ (N : ), ∃ (n : ) (H : n > N), P n)(∃ (φ : ), strict_mono φ ∀ (n : ), P (φ n))

theorem filter.extraction_of_frequently_at_top {P : → Prop} :
(∃ᶠ (n : ) in filter.at_top, P n)(∃ (φ : ), strict_mono φ ∀ (n : ), P (φ n))

theorem filter.extraction_of_eventually_at_top {P : → Prop} :
(∀ᶠ (n : ) in filter.at_top, P n)(∃ (φ : ), strict_mono φ ∀ (n : ), P (φ 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 : → β} :
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 : → β} :
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_id_le {u : } :
(∀ (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 : α → β} :
(∀ᶠ (x : α) in l, 0 f x)filter.tendsto g l filter.at_topfilter.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 : α → β} :
(∀ᶠ (x : α) in l, f x 0)filter.tendsto g l filter.at_botfilter.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 : α → β} :
(∀ (x : α), 0 f x)filter.tendsto g l filter.at_topfilter.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 : α → β} :
(∀ (x : α), f x 0)filter.tendsto g l filter.at_botfilter.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 : α → β} :
filter.tendsto f l filter.at_top(∀ᶠ (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 : α → β} :
filter.tendsto f l filter.at_bot(∀ᶠ (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 : α → β} :
filter.tendsto f l filter.at_top(∀ (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 : α → β} :
filter.tendsto f l filter.at_bot(∀ (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 : α → β} :

theorem filter.tendsto_at_bot_add {α : Type u_3} {β : Type u_4} [ordered_add_comm_monoid β] {l : filter α} {f g : α → β} :

theorem filter.tendsto_at_top_of_add_const_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α → β} (C : β) :

theorem filter.tendsto_at_bot_of_add_const_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α → β} (C : β) :

theorem filter.tendsto_at_top_of_add_const_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α → β} (C : β) :

theorem filter.tendsto_at_bot_of_add_const_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f : α → β} (C : β) :

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 : β) :
(∀ᶠ (x : α) in l, 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 : β) :
(∀ᶠ (x : α) in l, 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_left {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α → β} (C : β) :
(∀ (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 : β) :
(∀ (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 : β) :
(∀ᶠ (x : α) in l, 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 : β) :
(∀ᶠ (x : α) in l, 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_of_add_bdd_above_right {α : Type u_3} {β : Type u_4} [ordered_cancel_add_comm_monoid β] {l : filter α} {f g : α → β} (C : β) :
(∀ (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 : β) :
(∀ (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 : β) :
(∀ᶠ (x : α) in l, C f x)filter.tendsto g l filter.at_topfilter.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 : β) :
(∀ᶠ (x : α) in l, f x C)filter.tendsto g l filter.at_botfilter.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 : β) :
(∀ (x : α), C f x)filter.tendsto g l filter.at_topfilter.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 : β) :
(∀ (x : α), f x C)filter.tendsto g l filter.at_botfilter.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 : β) :
filter.tendsto f l filter.at_top(∀ᶠ (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 : β) :
filter.tendsto f l filter.at_bot(∀ᶠ (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 : β) :
filter.tendsto f l filter.at_top(∀ (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 : β) :
filter.tendsto f l filter.at_bot(∀ (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 : β) :

theorem filter.tendsto_at_bot_add_const_left {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α → β} (C : β) :

theorem filter.tendsto_at_top_add_const_right {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α → β} (C : β) :

theorem filter.tendsto_at_bot_add_const_right {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] (l : filter α) {f : α → β} (C : β) :

theorem filter.tendsto_at_top_mul_at_top {α : Type u_3} {β : Type u_4} [ordered_semiring α] {l : filter β} {f g : β → α} :

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 : α → β} :
monotone f(∀ (b : β), ∃ (a : α), b f a)filter.tendsto f filter.at_top filter.at_top

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

theorem filter.tendsto_at_top_at_top_iff_of_monotone {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] {f : α → β} :
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 : α → β} :
monotone f(filter.tendsto f filter.at_bot filter.at_bot ∀ (b : β), ∃ (a : α), f a b)

theorem filter.tendsto_at_top_embedding {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder β] [preorder γ] {f : α → β} {e : β → γ} {l : filter α} :
(∀ (b₁ b₂ : β), e b₁ e b₂ b₁ b₂)(∀ (c : γ), ∃ (b : β), c e b)(filter.tendsto (e f) l filter.at_top filter.tendsto f l filter.at_top)

theorem filter.tendsto_at_bot_embedding {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder β] [preorder γ] {f : α → β} {e : β → γ} {l : filter α} :
(∀ (b₁ b₂ : β), e b₁ e b₂ b₁ b₂)(∀ (c : γ), ∃ (b : β), e b c)(filter.tendsto (e f) l filter.at_bot filter.tendsto f l filter.at_bot)

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 α} :
monotone f(∀ (x : α), ∃ (n : β), x f n)filter.tendsto f filter.at_top filter.at_top

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 filter.tendsto_finset_image_at_top_at_top {β : Type u_4} {γ : Type u_5} {i : β → γ} {j : γ → β} :

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.map_at_top_eq_of_gc {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] {f : α → β} (g : β → α) (b' : β) :
monotone f(∀ (a : α) (b : β), b b'(f a b a g b))(∀ (b : β), b b'b f (g b))filter.map f filter.at_top = filter.at_top

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' : β) :
monotone f(∀ (a : α) (b : β), b b'(b f a g b a))(∀ (b : β), b b'f (g b) b)filter.map f filter.at_bot = filter.at_bot

theorem filter.tendsto_add_at_top_iff_nat {α : Type u_3} {f : → α} {l : filter α} (k : ) :

theorem filter.tendsto_at_top_at_top_of_monotone' {ι : Type u_1} {α : Type u_3} [preorder ι] [linear_order α] {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 : ι → α} :

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 : α → β} :

theorem filter.unbounded_of_tendsto_at_bot {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] [no_bot_order β] {f : α → β} :

theorem filter.unbounded_of_tendsto_at_top' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] [no_top_order β] {f : α → β} :

theorem filter.unbounded_of_tendsto_at_bot' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] [no_bot_order β] {f : α → β} :

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] :

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] :

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] :

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] :

theorem filter.map_at_top_finset_prod_le_of_prod_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [comm_monoid α] {f : β → α} {g : γ → α} :
(∀ (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 : γ → α} :
(∀ (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_antimono_basis.tendsto {ι : Type u_1} {α : Type u_3} [semilattice_sup ι] [nonempty ι] {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α} :
(∀ (i : ι), φ i s i)filter.tendsto φ filter.at_top l

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

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 β} :

theorem filter.is_countably_generated.subseq_tendsto {α : Type u_3} {f : filter α} (hf : f.is_countably_generated) {u : → α} :

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 : β → α} :
(∀ (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 : β → α} :
(∀ (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.