at_top and at_bot filters on preorded sets, monoids and groups. #
In this file we define the filters
at_top: corresponds ton → +∞;at_bot: corresponds ton → -∞.
Then we prove many lemmas like “if f → +∞, then f ± c → +∞”.
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
- filter.at_top = ⨅ (a : α), 𝓟 (set.Ici a)
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 : α), 𝓟 (set.Iic a)
theorem
filter.disjoint_at_bot_principal_Ioi
{α : Type u_3}
[preorder α]
(x : α) :
disjoint filter.at_bot (𝓟 (set.Ioi x))
theorem
filter.disjoint_at_top_principal_Iio
{α : Type u_3}
[preorder α]
(x : α) :
disjoint filter.at_top (𝓟 (set.Iio x))
theorem
filter.disjoint_at_top_principal_Iic
{α : Type u_3}
[preorder α]
[no_max_order α]
(x : α) :
disjoint filter.at_top (𝓟 (set.Iic x))
theorem
filter.disjoint_at_bot_principal_Ici
{α : Type u_3}
[preorder α]
[no_min_order α]
(x : α) :
disjoint filter.at_bot (𝓟 (set.Ici x))
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]
@[instance]
@[simp]
theorem
filter.mem_at_top_sets
{α : Type u_3}
[nonempty α]
[semilattice_sup α]
{s : set α} :
s ∈ filter.at_top ↔ ∃ (a : α), ∀ (b : α), b ≥ a → b ∈ s
@[simp]
theorem
filter.mem_at_bot_sets
{α : Type u_3}
[nonempty α]
[semilattice_inf α]
{s : set α} :
s ∈ filter.at_bot ↔ ∃ (a : α), ∀ (b : α), b ≤ a → b ∈ s
@[simp]
theorem
filter.eventually_at_top
{α : Type u_3}
[semilattice_sup α]
[nonempty α]
{p : α → Prop} :
(∀ᶠ (x : α) in filter.at_top, p x) ↔ ∃ (a : α), ∀ (b : α), b ≥ a → p b
@[simp]
theorem
filter.eventually_at_bot
{α : Type u_3}
[semilattice_inf α]
[nonempty α]
{p : α → Prop} :
(∀ᶠ (x : α) in filter.at_bot, p x) ↔ ∃ (a : α), ∀ (b : α), b ≤ a → p b
theorem
filter.eventually_ge_at_top
{α : Type u_3}
[preorder α]
(a : α) :
∀ᶠ (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.eventually_lt_at_bot
{α : Type u_3}
[preorder α]
[no_min_order α]
(a : α) :
∀ᶠ (x : α) in filter.at_bot, x < a
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 α]
[encodable α] :
filter.at_top.has_countable_basis (λ (_x : α), true) set.Ici
theorem
filter.at_bot_countable_basis
{α : Type u_3}
[nonempty α]
[semilattice_inf α]
[encodable α] :
filter.at_bot.has_countable_basis (λ (_x : α), true) set.Iic
@[protected, instance]
@[protected, instance]
theorem
filter.tendsto_at_top_pure
{α : Type u_3}
{β : Type u_4}
[partial_order α]
[order_top α]
(f : α → β) :
filter.tendsto f filter.at_top (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 (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 : α), 𝓟 (f '' {a' : α | a ≤ a'})
theorem
filter.map_at_bot_eq
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
{f : α → β} :
filter.map f filter.at_bot = ⨅ (a : α), 𝓟 (f '' {a' : α | a' ≤ a})
theorem
filter.tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[preorder β]
{m : α → β}
{f : filter α} :
filter.tendsto m f filter.at_top ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
theorem
filter.tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[preorder β]
{m : α → β}
{f : filter α} :
filter.tendsto m f filter.at_bot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
theorem
filter.tendsto_at_top_mono'
{α : Type u_3}
{β : Type u_4}
[preorder β]
(l : filter α)
⦃f₁ f₂ : α → β⦄
(h : f₁ ≤ᶠ[l] f₂) :
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) :
theorem
filter.tendsto_at_bot_mono
{α : Type u_3}
{β : Type u_4}
[preorder β]
{l : filter α}
{f g : α → β}
(h : ∀ (n : α), f n ≤ g n) :
Sequences #
theorem
filter.inf_map_at_top_ne_bot_iff
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[nonempty α]
{F : filter β}
{u : α → β} :
(F ⊓ filter.map u filter.at_top).ne_bot ↔ ∀ (U : set β), U ∈ F → ∀ (N : α), ∃ (n : α) (H : n ≥ N), u n ∈ U
theorem
filter.inf_map_at_bot_ne_bot_iff
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[nonempty α]
{F : filter β}
{u : α → β} :
(F ⊓ filter.map u filter.at_bot).ne_bot ↔ ∀ (U : set β), U ∈ F → ∀ (N : α), ∃ (n : α) (H : n ≤ N), u n ∈ U
theorem
filter.extraction_of_frequently_at_top
{P : ℕ → Prop}
(h : ∃ᶠ (n : ℕ) 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.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 : β) :
@[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 : β) :
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 : β) :
@[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 : β) :
theorem
filter.high_scores
{β : Type u_4}
[linear_order β]
[no_max_order β]
{u : ℕ → β}
(hu : filter.tendsto u filter.at_top filter.at_top)
(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 : ℕ) :
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
filter.tendsto_at_top_add_nonneg_left'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ᶠ (x : α) in l, 0 ≤ f x)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_left'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ᶠ (x : α) in l, f x ≤ 0)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_left
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ (x : α), 0 ≤ f x)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_left
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ (x : α), f x ≤ 0)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_right'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_top)
(hg : ∀ᶠ (x : α) in l, 0 ≤ g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_right'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_bot)
(hg : ∀ᶠ (x : α) in l, g x ≤ 0) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_right
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_top)
(hg : ∀ (x : α), 0 ≤ g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_right
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_bot)
(hg : ∀ (x : α), g x ≤ 0) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_top)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_bot)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto.nsmul_at_top
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f : α → β}
(hf : filter.tendsto f l filter.at_top)
{n : ℕ}
(hn : 0 < n) :
filter.tendsto (λ (x : α), n • f x) l filter.at_top
theorem
filter.tendsto.nsmul_at_bot
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f : α → β}
(hf : filter.tendsto f l filter.at_bot)
{n : ℕ}
(hn : 0 < n) :
filter.tendsto (λ (x : α), n • f x) l filter.at_bot
theorem
filter.tendsto_at_top_of_add_const_left
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f : α → β}
(C : β)
(hf : filter.tendsto (λ (x : α), C + f x) l filter.at_top) :
theorem
filter.tendsto_at_bot_of_add_const_left
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f : α → β}
(C : β)
(hf : filter.tendsto (λ (x : α), C + f x) l filter.at_bot) :
theorem
filter.tendsto_at_top_of_add_const_right
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f : α → β}
(C : β)
(hf : filter.tendsto (λ (x : α), f x + C) l filter.at_top) :
theorem
filter.tendsto_at_bot_of_add_const_right
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f : α → β}
(C : β)
(hf : filter.tendsto (λ (x : α), f x + C) l filter.at_bot) :
theorem
filter.tendsto_at_top_of_add_bdd_above_left'
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(C : β)
(hC : ∀ᶠ (x : α) in l, f x ≤ C)
(h : filter.tendsto (λ (x : α), f x + g x) l filter.at_top) :
theorem
filter.tendsto_at_bot_of_add_bdd_below_left'
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(C : β)
(hC : ∀ᶠ (x : α) in l, C ≤ f x)
(h : filter.tendsto (λ (x : α), f x + g x) l filter.at_bot) :
theorem
filter.tendsto_at_top_of_add_bdd_above_left
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(C : β)
(hC : ∀ (x : α), f x ≤ C) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_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) :
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
theorem
filter.tendsto_at_top_iff_tends_to_neg_at_bot
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_group β]
(l : filter α)
{f : α → β} :
filter.tendsto f l filter.at_top ↔ filter.tendsto (-f) l filter.at_bot
theorem
filter.tendsto_at_bot_iff_tends_to_neg_at_top
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_group β]
(l : filter α)
{f : α → β} :
filter.tendsto f l filter.at_bot ↔ filter.tendsto (-f) l filter.at_top
theorem
filter.tendsto.at_top_mul_at_top
{α : Type u_3}
{β : Type u_4}
[ordered_semiring α]
{l : filter β}
{f g : β → α}
(hf : filter.tendsto f l filter.at_top)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_top
theorem
filter.tendsto_mul_self_at_top
{α : Type u_3}
[ordered_semiring α] :
filter.tendsto (λ (x : α), x * x) filter.at_top filter.at_top
theorem
filter.tendsto_pow_at_top
{α : Type u_3}
[ordered_semiring α]
{n : ℕ}
(hn : 1 ≤ n) :
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.eventually_ne_of_tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[ordered_semiring α]
{l : filter β}
{f : β → α}
[nontrivial α]
(hf : filter.tendsto f l filter.at_top)
(c : α) :
∀ᶠ (x : β) in l, f x ≠ c
theorem
filter.eventually_ne_of_tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[ordered_ring α]
{l : filter β}
{f : β → α}
[nontrivial α]
(hf : filter.tendsto f l filter.at_bot)
(c : α) :
∀ᶠ (x : β) in l, f x ≠ c
theorem
filter.tendsto.at_top_mul_at_bot
{α : Type u_3}
{β : Type u_4}
[ordered_ring α]
{l : filter β}
{f g : β → α}
(hf : filter.tendsto f l filter.at_top)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_bot
theorem
filter.tendsto.at_bot_mul_at_top
{α : Type u_3}
{β : Type u_4}
[ordered_ring α]
{l : filter β}
{f g : β → α}
(hf : filter.tendsto f l filter.at_bot)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_bot
theorem
filter.tendsto.at_bot_mul_at_bot
{α : Type u_3}
{β : Type u_4}
[ordered_ring α]
{l : filter β}
{f g : β → α}
(hf : filter.tendsto f l filter.at_bot)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_top
$\lim_{x\to+\infty}|x|=+\infty$
$\lim_{x\to-\infty}|x|=+\infty$
@[simp]
theorem
filter.tendsto.at_top_of_const_mul
{α : Type u_3}
{β : Type u_4}
[linear_ordered_semiring α]
{l : filter β}
{f : β → α}
{c : α}
(hc : 0 < c)
(hf : filter.tendsto (λ (x : β), c * f x) l filter.at_top) :
theorem
filter.tendsto.at_top_of_mul_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_semiring α]
{l : filter β}
{f : β → α}
{c : α}
(hc : 0 < c)
(hf : filter.tendsto (λ (x : β), (f x) * c) l filter.at_top) :
theorem
filter.nonneg_of_eventually_pow_nonneg
{α : Type u_3}
[linear_ordered_ring α]
{a : α}
(h : ∀ᶠ (n : ℕ) in filter.at_top, 0 ≤ a ^ n) :
0 ≤ a
theorem
filter.tendsto.const_mul_at_top
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : 0 < r)
(hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), r * f x) l filter.at_top
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. For a version working in ℕ or ℤ, use
filter.tendsto.const_mul_at_top' instead.
theorem
filter.tendsto.at_top_mul_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : 0 < r)
(hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), (f x) * r) l filter.at_top
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. For a version working in ℕ or ℤ, use
filter.tendsto.at_top_mul_const' instead.
theorem
filter.tendsto.at_top_div_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : 0 < r)
(hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), f x / r) l filter.at_top
If a function tends to infinity along a filter, then this function divided by a positive constant also tends to infinity.
theorem
filter.tendsto.neg_const_mul_at_top
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : r < 0)
(hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), r * f x) l filter.at_bot
If a function tends to infinity along a filter, then this function multiplied by a negative constant (on the left) tends to negative infinity.
theorem
filter.tendsto.at_top_mul_neg_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : r < 0)
(hf : filter.tendsto f l filter.at_top) :
filter.tendsto (λ (x : β), (f x) * r) l filter.at_bot
If a function tends to infinity along a filter, then this function multiplied by a negative constant (on the right) tends to negative infinity.
theorem
filter.tendsto.const_mul_at_bot
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : 0 < r)
(hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), r * f x) l filter.at_bot
If a function tends to negative infinity along a filter, then this function multiplied by a positive constant (on the left) also tends to negative infinity.
theorem
filter.tendsto.at_bot_mul_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : 0 < r)
(hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), (f x) * r) l filter.at_bot
If a function tends to negative infinity along a filter, then this function multiplied by a positive constant (on the right) also tends to negative infinity.
theorem
filter.tendsto.at_bot_div_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : 0 < r)
(hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), f x / r) l filter.at_bot
If a function tends to negative infinity along a filter, then this function divided by a positive constant also tends to negative infinity.
theorem
filter.tendsto.neg_const_mul_at_bot
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : r < 0)
(hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), r * f x) l filter.at_top
If a function tends to negative infinity along a filter, then this function multiplied by a negative constant (on the left) tends to positive infinity.
theorem
filter.tendsto.at_bot_mul_neg_const
{α : Type u_3}
{β : Type u_4}
[linear_ordered_field α]
{l : filter β}
{f : β → α}
{r : α}
(hr : r < 0)
(hf : filter.tendsto f l filter.at_bot) :
filter.tendsto (λ (x : β), (f x) * r) l filter.at_top
If a function tends to negative infinity along a filter, then this function multiplied by a negative constant (on the right) tends to positive infinity.
theorem
filter.tendsto_const_mul_pow_at_top
{α : Type u_3}
[linear_ordered_field α]
{c : α}
{n : ℕ}
(hn : 1 ≤ n)
(hc : 0 < c) :
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_field α]
(c : α)
(n : ℕ) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_top ↔ 1 ≤ n ∧ 0 < c
theorem
filter.tendsto_neg_const_mul_pow_at_top
{α : Type u_3}
[linear_ordered_field α]
{c : α}
{n : ℕ}
(hn : 1 ≤ n)
(hc : c < 0) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_bot
theorem
filter.tendsto_neg_const_mul_pow_at_top_iff
{α : Type u_3}
[linear_ordered_field α]
(c : α)
(n : ℕ) :
filter.tendsto (λ (x : α), c * x ^ n) filter.at_top filter.at_bot ↔ 1 ≤ n ∧ c < 0
theorem
filter.tendsto_at_top'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
{f : α → β}
{l : filter β} :
filter.tendsto f filter.at_top l ↔ ∀ (s : set β), s ∈ l → (∃ (a : α), ∀ (b : α), b ≥ 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 (𝓟 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 (𝓟 s) ↔ ∃ (N : β), ∀ (n : β), n ≤ N → f n ∈ s
theorem
filter.tendsto_at_top_at_top
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
{f : α → β} :
filter.tendsto f filter.at_top filter.at_top ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≤ f a
A function f grows to +∞ independent of an order-preserving embedding e.
theorem
filter.tendsto_at_top_at_bot
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
{f : α → β} :
filter.tendsto f filter.at_top filter.at_bot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → f a ≤ b
theorem
filter.tendsto_at_bot_at_top
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
{f : α → β} :
filter.tendsto f filter.at_bot filter.at_top ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), a ≤ i → b ≤ f a
theorem
filter.tendsto_at_bot_at_bot
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
{f : α → β} :
filter.tendsto f filter.at_bot filter.at_bot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), a ≤ i → f a ≤ b
theorem
filter.tendsto_at_top_at_top_of_monotone
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : α → β}
(hf : monotone f)
(h : ∀ (b : β), ∃ (a : α), b ≤ f a) :
theorem
filter.tendsto_at_bot_at_bot_of_monotone
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : α → β}
(hf : monotone f)
(h : ∀ (b : β), ∃ (a : α), f a ≤ b) :
theorem
filter.tendsto_at_top_at_top_iff_of_monotone
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
{f : α → β}
(hf : monotone f) :
filter.tendsto f filter.at_top filter.at_top ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
theorem
filter.tendsto_at_bot_at_bot_iff_of_monotone
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
{f : α → β}
(hf : monotone f) :
filter.tendsto f filter.at_bot filter.at_bot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
theorem
monotone.tendsto_at_top_at_top
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : α → β}
(hf : monotone f)
(h : ∀ (b : β), ∃ (a : α), b ≤ f a) :
Alias of tendsto_at_top_at_top_of_monotone.
theorem
monotone.tendsto_at_bot_at_bot
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : α → β}
(hf : monotone f)
(h : ∀ (b : β), ∃ (a : α), f a ≤ b) :
Alias of tendsto_at_bot_at_bot_of_monotone.
theorem
monotone.tendsto_at_top_at_top_iff
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
{f : α → β}
(hf : monotone f) :
filter.tendsto f filter.at_top filter.at_top ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
Alias of tendsto_at_top_at_top_iff_of_monotone.
theorem
monotone.tendsto_at_bot_at_bot_iff
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
{f : α → β}
(hf : monotone f) :
filter.tendsto f filter.at_bot filter.at_bot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
Alias of tendsto_at_bot_at_bot_iff_of_monotone.
theorem
filter.tendsto_at_top_embedding
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[preorder β]
[preorder γ]
{f : α → β}
{e : β → γ}
{l : filter α}
(hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
(hu : ∀ (c : γ), ∃ (b : β), c ≤ e b) :
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.
theorem
monotone.tendsto_at_top_finset
{α : Type u_3}
{β : Type u_4}
[preorder β]
{f : β → finset α}
(h : monotone f)
(h' : ∀ (x : α), ∃ (n : β), x ∈ f n) :
Alias of tendsto_at_top_finset_of_monotone.
theorem
filter.tendsto_finset_image_at_top_at_top
{β : Type u_4}
{γ : Type u_5}
{i : β → γ}
{j : γ → β}
(h : function.left_inverse j i) :
theorem
filter.tendsto_finset_preimage_at_top_at_top
{α : Type u_3}
{β : Type u_4}
{f : α → β}
(hf : function.injective f) :
filter.tendsto (λ (s : finset β), s.preimage f _) filter.at_top filter.at_top
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₂ : β₂ → α₂) :
filter.map u₁ filter.at_top ×ᶠ 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 ×ᶠ 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) :
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 ×ᶠ 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 ×ᶠ 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) :
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) :
theorem
filter.eventually_at_bot_prod_self
{α : Type u_3}
[semilattice_inf α]
[nonempty α]
{p : α × α → Prop} :
(∀ᶠ (x : α × α) in filter.at_bot, p x) ↔ ∃ (a : α), ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
theorem
filter.eventually_at_top_prod_self
{α : Type u_3}
[semilattice_sup α]
[nonempty α]
{p : α × α → Prop} :
(∀ᶠ (x : α × α) in filter.at_top, p x) ↔ ∃ (a : α), ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)
theorem
filter.eventually_at_bot_prod_self'
{α : Type u_3}
[semilattice_inf α]
[nonempty α]
{p : α × α → Prop} :
(∀ᶠ (x : α × α) in filter.at_bot, p x) ↔ ∃ (a : α), ∀ (k : α), k ≤ a → ∀ (l : α), l ≤ a → p (k, l)
theorem
filter.eventually_at_top_prod_self'
{α : Type u_3}
[semilattice_sup α]
[nonempty α]
{p : α × α → Prop} :
(∀ᶠ (x : α × α) in filter.at_top, p x) ↔ ∃ (a : α), ∀ (k : α), k ≥ a → ∀ (l : α), l ≥ a → p (k, l)
theorem
filter.eventually_at_top_curry
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[semilattice_sup β]
{p : α × β → Prop}
(hp : ∀ᶠ (x : α × β) in filter.at_top, p x) :
∀ᶠ (k : α) in filter.at_top, ∀ᶠ (l : β) in filter.at_top, p (k, l)
theorem
filter.eventually_at_bot_curry
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[semilattice_inf β]
{p : α × β → Prop}
(hp : ∀ᶠ (x : α × β) in filter.at_bot, p x) :
∀ᶠ (k : α) in filter.at_bot, ∀ᶠ (l : β) in filter.at_bot, p (k, l)
theorem
filter.map_at_top_eq_of_gc
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[semilattice_sup β]
{f : α → β}
(g : β → α)
(b' : β)
(hf : monotone f)
(gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b))
(hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)) :
A function f maps upwards closed sets (at_top sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connetion above b'.
theorem
filter.map_at_bot_eq_of_gc
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[semilattice_inf β]
{f : α → β}
(g : β → α)
(b' : β)
(hf : monotone f)
(gc : ∀ (a : α) (b : β), b ≤ b' → (b ≤ f a ↔ g b ≤ a))
(hgi : ∀ (b : β), b ≤ b' → f (g b) ≤ b) :
theorem
filter.map_coe_at_top_of_Ici_subset
{α : Type u_3}
[semilattice_sup α]
{a : α}
{s : set α}
(h : set.Ici a ⊆ s) :
@[simp]
The image of the filter at_top on Ici a under the coercion equals at_top.
@[simp]
The image of the filter at_top on Ioi a under the coercion equals at_top.
The at_top filter for an open interval Ioi a comes from the at_top filter in the ambient
order.
The at_top filter for an open interval Ici a comes from the at_top filter in the ambient
order.
@[simp]
The at_bot filter for an open interval Iio a comes from the at_bot filter in the ambient
order.
The at_bot filter for an open interval Iio a comes from the at_bot filter in the ambient
order.
@[simp]
The at_bot filter for an open interval Iic a comes from the at_bot filter in the ambient
order.
The at_bot filter for an open interval Iic a comes from the at_bot filter in the ambient
order.
theorem
filter.tendsto_Ioi_at_top
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
{a : α}
{f : β → ↥(set.Ioi a)}
{l : filter β} :
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
theorem
filter.tendsto_at_top_at_top_of_monotone'
{ι : Type u_1}
{α : Type u_3}
[preorder ι]
[linear_order α]
{u : ι → α}
(h : monotone u)
(H : ¬bdd_above (set.range u)) :
If u is a monotone function with linear ordered codomain and the range of u is not bounded
above, then tendsto u at_top at_top.
theorem
filter.tendsto_at_bot_at_bot_of_monotone'
{ι : Type u_1}
{α : Type u_3}
[preorder ι]
[linear_order α]
{u : ι → α}
(h : monotone u)
(H : ¬bdd_below (set.range u)) :
If u is a monotone function with linear ordered codomain and the range of u is not bounded
below, then tendsto u at_bot at_bot.
theorem
filter.unbounded_of_tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
[no_max_order β]
{f : α → β}
(h : filter.tendsto f filter.at_top filter.at_top) :
theorem
filter.unbounded_of_tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
[no_min_order β]
{f : α → β}
(h : filter.tendsto f filter.at_top filter.at_bot) :
theorem
filter.unbounded_of_tendsto_at_top'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
[no_max_order β]
{f : α → β}
(h : filter.tendsto f filter.at_bot filter.at_top) :
theorem
filter.unbounded_of_tendsto_at_bot'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
[no_min_order β]
{f : α → β}
(h : filter.tendsto f filter.at_bot filter.at_bot) :
theorem
filter.tendsto_at_top_of_monotone_of_filter
{ι : Type u_1}
{α : Type u_3}
[preorder ι]
[preorder α]
{l : filter ι}
{u : ι → α}
(h : monotone u)
[l.ne_bot]
(hu : filter.tendsto u l filter.at_top) :
If a monotone function u : ι → α tends to at_top along some non-trivial filter l, then
it tends to at_top along at_top.
theorem
filter.tendsto_at_bot_of_monotone_of_filter
{ι : Type u_1}
{α : Type u_3}
[preorder ι]
[preorder α]
{l : filter ι}
{u : ι → α}
(h : monotone u)
[l.ne_bot]
(hu : filter.tendsto u l filter.at_bot) :
If a monotone function u : ι → α tends to at_bot along some non-trivial filter l, then
it tends to at_bot along at_bot.
theorem
filter.tendsto_at_top_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[preorder ι]
[preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : monotone u)
{l : filter ι'}
[l.ne_bot]
(H : filter.tendsto (u ∘ φ) l filter.at_top) :
theorem
filter.tendsto_at_bot_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[preorder ι]
[preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : monotone u)
{l : filter ι'}
[l.ne_bot]
(H : filter.tendsto (u ∘ φ) l filter.at_bot) :
theorem
filter.map_at_top_finset_prod_le_of_prod_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[comm_monoid α]
{f : β → α}
{g : γ → α}
(h_eq : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ ∏ (x : γ) in u', g x = ∏ (b : β) in v', f b)) :
filter.map (λ (s : finset β), ∏ (b : β) in s, f b) filter.at_top ≤ filter.map (λ (s : finset γ), ∏ (x : γ) in s, g x) filter.at_top
Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient
condition for comparison of the filter at_top.map (λ s, ∏ b in s, f b) with
at_top.map (λ s, ∏ b in s, g b). This is useful to compare the set of limit points of
Π b in s, f b as s → at_top with the similar set for g.
theorem
filter.map_at_top_finset_sum_le_of_sum_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[add_comm_monoid α]
{f : β → α}
{g : γ → α}
(h_eq : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ ∑ (x : γ) in u', g x = ∑ (b : β) in v', f b)) :
filter.map (λ (s : finset β), ∑ (b : β) in s, f b) filter.at_top ≤ filter.map (λ (s : finset γ), ∑ (x : γ) in s, g x) filter.at_top
theorem
filter.has_antitone_basis.tendsto
{ι : Type u_1}
{α : Type u_3}
[semilattice_sup ι]
[nonempty ι]
{l : filter α}
{s : ι → set α}
(hl : l.has_antitone_basis s)
{φ : ι → α}
(h : ∀ (i : ι), φ i ∈ s i) :
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 ι} :
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
@[simp]
theorem
order_iso.comap_at_top
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(e : α ≃o β) :
@[simp]
theorem
order_iso.comap_at_bot
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(e : α ≃o β) :
@[simp]
@[simp]
theorem
order_iso.tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(e : α ≃o β) :
theorem
order_iso.tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(e : α ≃o β) :
@[simp]
theorem
order_iso.tendsto_at_top_iff
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[preorder α]
[preorder β]
{l : filter γ}
{f : γ → α}
(e : α ≃o β) :
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
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 γ), ∑ (i : γ) in s, f (g i)) filter.at_top = filter.map (λ (s : finset β), ∑ (i : β) in s, f i) filter.at_top
Let g : γ → β be an injective function and f : β → α be a function from the codomain of g
to an additive commutative monoid. Suppose that f x = 0 outside of the range of g. Then the
filters at_top.map (λ s, ∑ i in s, f (g i)) and at_top.map (λ s, ∑ i in s, f i) coincide.
This lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under
the same assumptions.
theorem
function.injective.map_at_top_finset_prod_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[comm_monoid α]
{g : γ → β}
(hg : function.injective g)
{f : β → α}
(hf : ∀ (x : β), x ∉ set.range g → f 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.