mathlib3 documentation

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

filter α

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

filter.at_bot = ⨅ (a : α), filter.principal (set.Iic a)

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 : α) :

set.Ici a ∈ filter.at_top

theorem filter.Ioi_mem_at_top {α : Type u_3} [preorder α] [no_max_order α] (x : α) :

set.Ioi x ∈ filter.at_top

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 : α) :

set.Iic a ∈ filter.at_bot

theorem filter.Iio_mem_at_bot {α : Type u_3} [preorder α] [no_min_order α] (x : α) :

set.Iio x ∈ filter.at_bot

theorem filter.disjoint_at_bot_principal_Ioi {α : Type u_3} [preorder α] (x : α) :

disjoint filter.at_bot (filter.principal (set.Ioi x))

theorem filter.disjoint_at_top_principal_Iio {α : Type u_3} [preorder α] (x : α) :

disjoint filter.at_top (filter.principal (set.Iio x))

theorem filter.disjoint_at_top_principal_Iic {α : Type u_3} [preorder α] [no_max_order α] (x : α) :

disjoint filter.at_top (filter.principal (set.Iic x))

theorem filter.disjoint_at_bot_principal_Ici {α : Type u_3} [preorder α] [no_min_order α] (x : α) :

disjoint filter.at_bot (filter.principal (set.Ici x))

theorem filter.disjoint_pure_at_top {α : Type u_3} [preorder α] [no_max_order α] (x : α) :

disjoint (has_pure.pure x) filter.at_top

theorem filter.disjoint_pure_at_bot {α : Type u_3} [preorder α] [no_min_order α] (x : α) :

disjoint (has_pure.pure x) filter.at_bot

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

disjoint filter.at_bot filter.at_top

theorem filter.disjoint_at_bot_at_top {α : Type u_3} [partial_order α] [nontrivial α] :

disjoint filter.at_top filter.at_bot

theorem filter.disjoint_at_top_at_bot {α : Type u_3} [partial_order α] [nontrivial α] :

theorem filter.at_top_basis {α : Type u_3} [nonempty α] [semilattice_sup α] :

filter.at_top.has_basis (λ (_x : α), true) set.Ici

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

filter.at_bot.has_basis (λ (_x : α), true) set.Iic

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

filter.at_top.ne_bot

@[instance]

theorem filter.at_bot_ne_bot {α : Type u_3} [nonempty α] [semilattice_inf α] :

filter.at_bot.ne_bot

@[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 : α) :

∀ᶠ (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_max_order α] (a : α) :

∀ᶠ (x : α) in filter.at_top , a < x

theorem filter.eventually_ne_at_top {α : Type u_3} [preorder α] [no_max_order α] (a : α) :

∀ᶠ (x : α) in filter.at_top , x ≠ 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 : α) :

∀ᶠ (x : α) in filter.at_bot , x ≠ 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.at_top_basis_Ioi {α : Type u_3} [nonempty α] [semilattice_sup α] [no_max_order α] :

filter.at_top.has_basis (λ (_x : α), true) set.Ioi

theorem filter.at_top_countable_basis {α : Type u_3} [nonempty α] [semilattice_sup α] [countable α] :

filter.at_top.has_countable_basis (λ (_x : α), true) set.Ici

theorem filter.at_bot_countable_basis {α : Type u_3} [nonempty α] [semilattice_inf α] [countable α] :

filter.at_bot.has_countable_basis (λ (_x : α), true) set.Iic

filter.at_top.is_countably_generated

@[protected, instance]

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

filter.at_bot.is_countably_generated

@[protected, instance]

def filter.at_bot.is_countably_generated {α : Type u_3} [preorder α] [countable α] :

filter.at_top = has_pure.pure ⊤

theorem filter.order_top.at_top_eq (α : Type u_1) [partial_order α] [order_top α] :

filter.at_bot = has_pure.pure ⊥

theorem filter.order_bot.at_bot_eq (α : Type u_1) [partial_order α] [order_bot α] :

theorem filter.subsingleton.at_top_eq (α : Type u_1) [subsingleton α] [preorder α] :

filter.at_top = ⊤

theorem filter.subsingleton.at_bot_eq (α : Type u_1) [subsingleton α] [preorder α] :

filter.at_bot = ⊤

theorem filter.tendsto_at_top_pure {α : Type u_3} {β : Type u_4} [partial_order α] [order_top α] (f : α → β) :

filter.tendsto f filter.at_top (has_pure.pure (f ⊤))

theorem filter.tendsto_at_bot_pure {α : Type u_3} {β : Type u_4} [partial_order α] [order_bot α] (f : α → β) :

filter.tendsto f filter.at_bot (has_pure.pure (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₂) :

filter.tendsto f₁ l filter.at_top → filter.tendsto f₂ l filter.at_top

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

filter.tendsto f₂ l filter.at_bot → filter.tendsto f₁ l filter.at_bot

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

filter.tendsto f l filter.at_top → filter.tendsto g l filter.at_top

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

filter.tendsto g l filter.at_bot → filter.tendsto f l filter.at_bot

@[simp]

theorem order_iso.comap_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :

filter.comap ⇑e filter.at_top = filter.at_top

@[simp]

theorem order_iso.comap_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :

filter.comap ⇑e filter.at_bot = filter.at_bot

@[simp]

theorem order_iso.map_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :

filter.map ⇑e filter.at_top = filter.at_top

@[simp]

theorem order_iso.map_at_bot {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :

filter.map ⇑e filter.at_bot = filter.at_bot

filter.tendsto ⇑e filter.at_top filter.at_top

theorem order_iso.tendsto_at_top {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (e : α ≃o β) :

filter.tendsto ⇑e filter.at_bot filter.at_bot

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

filter.tendsto (λ (x : γ), ⇑e (f x)) l filter.at_top ↔ filter.tendsto f l filter.at_top

@[simp]

theorem order_iso.tendsto_at_bot_iff {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] {l : filter γ} {f : γ → α} (e : α ≃o β) :

filter.tendsto (λ (x : γ), ⇑e (f x)) l filter.at_bot ↔ filter.tendsto f l filter.at_bot

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_tendsto_at_top {β : Type u_1} [linear_order β] [no_max_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 strict_mono.tendsto_at_top {φ : ℕ → ℕ} (h : strict_mono φ) :

filter.tendsto φ filter.at_top filter.at_top

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

filter.tendsto bit0 filter.at_top filter.at_top

theorem filter.tendsto_bit0_at_top {β : Type u_4} [ordered_add_comm_monoid β] :

filter.tendsto bit0 filter.at_bot filter.at_bot

theorem filter.tendsto_bit0_at_bot {β : Type u_4} [ordered_add_comm_monoid β] :

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

filter.tendsto f 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) :

filter.tendsto f 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) :

filter.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 : α) in l, C ≤ f x) (h : filter.tendsto (λ (x : α), f x + g x) l filter.at_bot) :

filter.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 : β) (hC : ∀ (x : α), f x ≤ C) :

filter.tendsto (λ (x : α), f x + g x) l filter.at_top → filter.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_bot → filter.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) :

filter.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 : β) (hC : ∀ (x : α), g x ≤ C) :

filter.tendsto (λ (x : α), f x + g x) l filter.at_top → filter.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_bot → filter.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

filter.map has_neg.neg filter.at_bot = filter.at_top

theorem filter.map_neg_at_bot {β : Type u_4} [ordered_add_comm_group β] :

filter.map has_neg.neg filter.at_top = filter.at_bot

theorem filter.map_neg_at_top {β : Type u_4} [ordered_add_comm_group β] :

filter.comap has_neg.neg filter.at_bot = filter.at_top

@[simp]

theorem filter.comap_neg_at_bot {β : Type u_4} [ordered_add_comm_group β] :

filter.comap has_neg.neg filter.at_top = filter.at_bot

@[simp]

theorem filter.comap_neg_at_top {β : Type u_4} [ordered_add_comm_group β] :

filter.tendsto has_neg.neg filter.at_top filter.at_bot

theorem filter.tendsto_neg_at_top_at_bot {β : Type u_4} [ordered_add_comm_group β] :

filter.tendsto has_neg.neg filter.at_bot filter.at_top

theorem filter.tendsto_neg_at_bot_at_top {β : Type u_4} [ordered_add_comm_group β] :

@[simp]

theorem filter.tendsto_neg_at_top_iff {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] {l : filter α} {f : α → β} :

filter.tendsto (λ (x : α), -f x) l filter.at_top ↔ filter.tendsto f l filter.at_bot

@[simp]

theorem filter.tendsto_neg_at_bot_iff {α : Type u_3} {β : Type u_4} [ordered_add_comm_group β] {l : filter α} {f : α → β} :

filter.tendsto (λ (x : α), -f x) l filter.at_bot ↔ filter.tendsto f l filter.at_top

filter.tendsto bit1 filter.at_top filter.at_top

theorem filter.tendsto_bit1_at_top {α : Type u_3} [strict_ordered_semiring α] :

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_mul_self_at_top {α : Type u_3} [strict_ordered_semiring α] :

filter.tendsto (λ (x : α), x * x) filter.at_top filter.at_top

theorem filter.tendsto_pow_at_top {α : Type u_3} [strict_ordered_semiring α] {n : ℕ} (hn : n ≠ 0) :

filter.tendsto (λ (x : α), x ^ n) filter.at_top filter.at_top

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

filter.tendsto has_abs.abs filter.at_top filter.at_top

theorem filter.tendsto_abs_at_top_at_top {α : Type u_3} [linear_ordered_add_comm_group α] :

$\lim_{x\to+\infty}|x|=+\infty$

filter.tendsto has_abs.abs filter.at_bot filter.at_top

theorem filter.tendsto_abs_at_bot_at_top {α : Type u_3} [linear_ordered_add_comm_group α] :

$\lim_{x\to-\infty}|x|=+\infty$

filter.comap has_abs.abs filter.at_top = filter.at_bot ⊔ filter.at_top

@[simp]

theorem filter.comap_abs_at_top {α : Type u_3} [linear_ordered_add_comm_group α] :

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.tendsto_pow_at_top_iff {α : Type u_3} [linear_ordered_semiring α] {n : ℕ} :

filter.tendsto (λ (x : α), x ^ n) filter.at_top filter.at_top ↔ n ≠ 0

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.not_tendsto_pow_at_top_at_bot {α : Type u_3} [linear_ordered_ring α] {n : ℕ} :

¬filter.tendsto (λ (x : α), x ^ n) filter.at_top filter.at_bot

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

filter.tendsto (λ (x : β), r * f x) l filter.at_top ↔ filter.tendsto f l filter.at_top

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

filter.tendsto (λ (x : β), f x * r) l filter.at_top ↔ filter.tendsto f l filter.at_top

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

filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_top

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

filter.tendsto (λ (x : β), r * f x) l filter.at_bot ↔ filter.tendsto f l filter.at_bot

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

filter.tendsto (λ (x : β), f x * r) l filter.at_bot ↔ filter.tendsto f l filter.at_bot

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

filter.tendsto (λ (x : β), r * f x) l filter.at_top ↔ filter.tendsto f l filter.at_bot

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

filter.tendsto (λ (x : β), f x * r) l filter.at_top ↔ filter.tendsto f l filter.at_bot

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

filter.tendsto (λ (x : β), r * f x) l filter.at_bot ↔ filter.tendsto f l filter.at_top

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

filter.tendsto (λ (x : β), f x * r) l filter.at_bot ↔ filter.tendsto f l filter.at_top

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

filter.tendsto (λ (x : β), r * f x) l filter.at_top ↔ 0 < r ∧ filter.tendsto f l filter.at_top ∨ r < 0 ∧ filter.tendsto f l filter.at_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] :

filter.tendsto (λ (x : β), f x * r) l filter.at_top ↔ 0 < r ∧ filter.tendsto f l filter.at_top ∨ r < 0 ∧ filter.tendsto f l filter.at_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] :

filter.tendsto (λ (x : β), r * f x) l filter.at_bot ↔ 0 < r ∧ filter.tendsto f l filter.at_bot ∨ r < 0 ∧ filter.tendsto f l filter.at_top

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

filter.tendsto (λ (x : β), f x * r) l filter.at_bot ↔ 0 < r ∧ filter.tendsto f l filter.at_bot ∨ r < 0 ∧ filter.tendsto f l filter.at_top

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

filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_bot

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

filter.tendsto f filter.at_bot filter.at_bot

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 filter.tendsto_at_top_at_top_of_monotone.

filter.tendsto f filter.at_bot filter.at_bot

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 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 filter.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 filter.tendsto_at_bot_at_bot_iff_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) :

filter.comap e filter.at_top = filter.at_top

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

filter.comap e filter.at_bot = filter.at_bot

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

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 α} (hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ (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.

filter.tendsto finset.range filter.at_top filter.at_top

theorem filter.tendsto_finset_range :

theorem filter.at_top_finset_eq_infi {α : Type u_3} :

filter.at_top = ⨅ (x : α), filter.principal (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 filter.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) :

filter.tendsto (finset.image j) filter.at_top filter.at_top

theorem filter.tendsto_finset_preimage_at_top_at_top {α : Type u_3} {β : Type u_4} {f : α → β} (hf : function.injective f) :

filter.tendsto (λ (s : finset β), s.preimage f _) filter.at_top filter.at_top

filter.at_top.prod filter.at_top = filter.at_top

theorem filter.prod_at_top_at_top_eq {β₁ : Type u_1} {β₂ : Type u_2} [semilattice_sup β₁] [semilattice_sup β₂] :

filter.at_bot.prod filter.at_bot = filter.at_bot

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

(filter.map u₁ filter.at_top).prod (filter.map u₂ filter.at_top) = filter.map (prod.map u₁ u₂) filter.at_top

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

(filter.map u₁ filter.at_bot).prod (filter.map u₂ filter.at_bot) = filter.map (prod.map u₁ u₂) filter.at_bot

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

filter.tendsto (λ (a : α), (a, a)) filter.at_bot filter.at_bot

theorem filter.tendsto_at_top_diagonal {α : Type u_3} [semilattice_sup α] :

filter.tendsto (λ (a : α), (a, a)) filter.at_top filter.at_top

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

filter.tendsto (prod.map f g) (F.prod 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) :

filter.tendsto (prod.map f g) (F.prod G) filter.at_top

theorem filter.tendsto.prod_at_bot {α : Type u_3} {γ : Type u_5} [semilattice_inf α] [semilattice_inf γ] {f g : α → γ} (hf : filter.tendsto f filter.at_bot filter.at_bot) (hg : filter.tendsto g filter.at_bot filter.at_bot) :

filter.tendsto (prod.map f g) filter.at_bot filter.at_bot

theorem filter.tendsto.prod_at_top {α : Type u_3} {γ : Type u_5} [semilattice_sup α] [semilattice_sup γ] {f g : α → γ} (hf : filter.tendsto f filter.at_top filter.at_top) (hg : filter.tendsto g filter.at_top filter.at_top) :

filter.tendsto (prod.map f g) filter.at_top 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)) :

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' : β) (hf : monotone f) (gc : ∀ (a : α) (b : β), b ≤ b' → (b ≤ f a ↔ g b ≤ a)) (hgi : ∀ (b : β), b ≤ b' → f (g b) ≤ b) :

filter.map f filter.at_bot = filter.at_bot

filter.map coe filter.at_top = filter.at_top

theorem filter.map_coe_at_top_of_Ici_subset {α : Type u_3} [semilattice_sup α] {a : α} {s : set α} (h : set.Ici a ⊆ s) :

filter.map coe filter.at_top = filter.at_top

@[simp]

theorem filter.map_coe_Ici_at_top {α : Type u_3} [semilattice_sup α] (a : α) :

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

filter.map coe filter.at_top = filter.at_top

@[simp]

theorem filter.map_coe_Ioi_at_top {α : Type u_3} [semilattice_sup α] [no_max_order α] (a : α) :

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

filter.at_top = filter.comap coe filter.at_top

theorem filter.at_top_Ioi_eq {α : Type u_3} [semilattice_sup α] (a : α) :

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

filter.at_top = filter.comap coe filter.at_top

theorem filter.at_top_Ici_eq {α : Type u_3} [semilattice_sup α] (a : α) :

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

filter.map coe filter.at_bot = filter.at_bot

@[simp]

theorem filter.map_coe_Iio_at_bot {α : Type u_3} [semilattice_inf α] [no_min_order α] (a : α) :

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

filter.at_bot = filter.comap coe filter.at_bot

theorem filter.at_bot_Iio_eq {α : Type u_3} [semilattice_inf α] (a : α) :

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

filter.map coe filter.at_bot = filter.at_bot

@[simp]

theorem filter.map_coe_Iic_at_bot {α : Type u_3} [semilattice_inf α] (a : α) :

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

filter.at_bot = filter.comap coe filter.at_bot

theorem filter.at_bot_Iic_eq {α : Type u_3} [semilattice_inf α] (a : α) :

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

filter.tendsto f l filter.at_top ↔ filter.tendsto (λ (x : β), ↑(f x)) l filter.at_top

theorem filter.tendsto_Iio_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] {a : α} {f : β → ↥(set.Iio a)} {l : filter β} :

filter.tendsto f l filter.at_bot ↔ filter.tendsto (λ (x : β), ↑(f x)) l filter.at_bot

theorem filter.tendsto_Ici_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] {a : α} {f : β → ↥(set.Ici a)} {l : filter β} :

filter.tendsto f l filter.at_top ↔ filter.tendsto (λ (x : β), ↑(f x)) l filter.at_top

theorem filter.tendsto_Iic_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] {a : α} {f : β → ↥(set.Iic a)} {l : filter β} :

filter.tendsto f l filter.at_bot ↔ filter.tendsto (λ (x : β), ↑(f x)) l filter.at_bot

@[simp]

theorem filter.tendsto_comp_coe_Ioi_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] [no_max_order α] {a : α} {f : α → β} {l : filter β} :

filter.tendsto (λ (x : ↥(set.Ioi a)), f ↑x) filter.at_top l ↔ filter.tendsto f filter.at_top l

@[simp]

theorem filter.tendsto_comp_coe_Ici_at_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] {a : α} {f : α → β} {l : filter β} :

filter.tendsto (λ (x : ↥(set.Ici a)), f ↑x) filter.at_top l ↔ filter.tendsto f filter.at_top l

@[simp]

theorem filter.tendsto_comp_coe_Iio_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] [no_min_order α] {a : α} {f : α → β} {l : filter β} :

filter.tendsto (λ (x : ↥(set.Iio a)), f ↑x) filter.at_bot l ↔ filter.tendsto f filter.at_bot l

@[simp]

theorem filter.tendsto_comp_coe_Iic_at_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] {a : α} {f : α → β} {l : filter β} :

filter.tendsto (λ (x : ↥(set.Iic a)), f ↑x) filter.at_bot l ↔ filter.tendsto f filter.at_bot l

theorem filter.map_add_at_top_eq_nat (k : ℕ) :

filter.map (λ (a : ℕ), a + k) filter.at_top = filter.at_top

theorem filter.map_sub_at_top_eq_nat (k : ℕ) :

filter.map (λ (a : ℕ), a - k) filter.at_top = filter.at_top

theorem filter.tendsto_add_at_top_nat (k : ℕ) :

filter.tendsto (λ (a : ℕ), a + k) filter.at_top filter.at_top

theorem filter.tendsto_sub_at_top_nat (k : ℕ) :

filter.tendsto (λ (a : ℕ), a - k) filter.at_top filter.at_top

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

filter.tendsto (λ (n : ℕ), f (n + k)) filter.at_top l ↔ filter.tendsto f filter.at_top l

theorem filter.map_div_at_top_eq_nat (k : ℕ) (hk : 0 < k) :

filter.map (λ (a : ℕ), a / k) filter.at_top = filter.at_top

filter.tendsto u filter.at_top filter.at_top

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.

filter.tendsto u filter.at_bot filter.at_bot

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_max_order β] {f : α → β} (h : filter.tendsto f filter.at_top filter.at_top) :

¬bdd_above (set.range f)

theorem filter.unbounded_of_tendsto_at_bot {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_sup α] [preorder β] [no_min_order β] {f : α → β} (h : filter.tendsto f filter.at_top filter.at_bot) :

¬bdd_below (set.range f)

theorem filter.unbounded_of_tendsto_at_top' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] [no_max_order β] {f : α → β} (h : filter.tendsto f filter.at_bot filter.at_top) :

¬bdd_above (set.range f)

theorem filter.unbounded_of_tendsto_at_bot' {α : Type u_3} {β : Type u_4} [nonempty α] [semilattice_inf α] [preorder β] [no_min_order β] {f : α → β} (h : filter.tendsto f filter.at_bot filter.at_bot) :

¬bdd_below (set.range f)

filter.tendsto u filter.at_top filter.at_top

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.

filter.tendsto u filter.at_bot filter.at_bot

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.

filter.tendsto u filter.at_top filter.at_top

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

filter.tendsto u filter.at_bot filter.at_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] (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) :

filter.tendsto φ filter.at_top l

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

l.has_antitone_basis (s ∘ φ)

theorem filter.has_antitone_basis.comp_strict_mono {α : Type u_3} {l : filter α} {s : ℕ → set α} (hs : l.has_antitone_basis s) {φ : ℕ → ℕ} (hφ : strict_mono φ) :

l.has_antitone_basis (s ∘ φ)

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".

theorem filter.exists_seq_tendsto {α : Type u_3} (f : filter α) [f.is_countably_generated] [f.ne_bot] :

∃ (x : ℕ → α), filter.tendsto x filter.at_top f

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

filter.tendsto f k l ↔ ∀ (x : ℕ → α), filter.tendsto x filter.at_top k → filter.tendsto (f ∘ x) filter.at_top l

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

(∀ (x : ℕ → α), filter.tendsto x filter.at_top k → filter.tendsto (f ∘ x) filter.at_top l) → filter.tendsto f k l

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

filter.tendsto x l f

A sequence converges if every subsequence has a convergent subsequence.

theorem filter.subseq_tendsto_of_ne_bot {α : Type u_3} {f : filter α} [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

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.