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 : α), 𝓟 {b : α | a ≤ b}
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 : α), 𝓟 {b : α | b ≤ a}
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.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
theorem
filter.is_countably_generated_at_top
{α : Type u_3}
[nonempty α]
[semilattice_sup α]
[encodable α] :
theorem
filter.is_countably_generated_at_bot
{α : Type u_3}
[nonempty α]
[semilattice_inf α]
[encodable α] :
theorem
filter.tendsto_at_top_pure
{α : Type u_3}
{β : Type u_4}
[order_top α]
(f : α → β) :
filter.tendsto f filter.at_top (pure (f ⊤))
theorem
filter.tendsto_at_bot_pure
{α : Type u_3}
{β : Type u_4}
[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_top_order α]
{p : α → Prop} :
(∃ᶠ (x : α) in filter.at_top, p x) ↔ ∀ (a : α), ∃ (b : α) (H : b > a), p b
theorem
filter.frequently_at_bot'
{α : Type u_3}
[semilattice_inf α]
[nonempty α]
[no_bot_order α]
{p : α → Prop} :
(∃ᶠ (x : α) in filter.at_bot, p x) ↔ ∀ (a : α), ∃ (b : α) (H : b < a), p b
theorem
filter.frequently.forall_exists_of_at_top
{α : Type u_3}
[semilattice_sup α]
[nonempty α]
{p : α → Prop}
(h : ∃ᶠ (x : α) in filter.at_top, p x)
(a : α) :
∃ (b : α) (H : b ≥ a), p b
theorem
filter.frequently.forall_exists_of_at_bot
{α : Type u_3}
[semilattice_inf α]
[nonempty α]
{p : α → Prop}
(h : ∃ᶠ (x : α) in filter.at_bot, p x)
(a : α) :
∃ (b : α) (H : b ≤ a), p b
theorem
filter.map_at_top_eq
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
{f : α → β} :
filter.map f filter.at_top = ⨅ (a : α), 𝓟 (f '' {a' : α | a ≤ a'})
theorem
filter.map_at_bot_eq
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
{f : α → β} :
filter.map f filter.at_bot = ⨅ (a : α), 𝓟 (f '' {a' : α | a' ≤ a})
theorem
filter.tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[preorder β]
(m : α → β)
(f : filter α) :
filter.tendsto m f filter.at_top ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
theorem
filter.tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[preorder β]
(m : α → β)
(f : filter α) :
filter.tendsto m f filter.at_bot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
theorem
filter.tendsto_at_top_mono'
{α : Type u_3}
{β : Type u_4}
[preorder β]
(l : filter α)
⦃f₁ f₂ : α → β⦄
(h : f₁ ≤ᶠ[l] f₂)
(a : 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₂)
(a : 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)
(a : filter.tendsto f 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)
(a : filter.tendsto g l filter.at_bot) :
Sequences
theorem
filter.inf_map_at_top_ne_bot_iff
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[nonempty α]
{F : filter β}
{u : α → β} :
(F ⊓ filter.map u filter.at_top).ne_bot ↔ ∀ (U : set β), U ∈ F → ∀ (N : α), ∃ (n : α) (H : n ≥ N), u n ∈ U
theorem
filter.inf_map_at_bot_ne_bot_iff
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[nonempty α]
{F : filter β}
{u : α → β} :
(F ⊓ filter.map u filter.at_bot).ne_bot ↔ ∀ (U : set β), U ∈ F → ∀ (N : α), ∃ (n : α) (H : n ≤ N), u n ∈ U
theorem
filter.extraction_of_frequently_at_top
{P : ℕ → Prop}
(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.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_top_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_bot_order β]
{u : α → β}
(h : filter.tendsto u filter.at_top filter.at_bot)
(a : α)
(b : β) :
theorem
filter.high_scores
{β : Type u_4}
[linear_order β]
[no_top_order β]
{u : ℕ → β}
(hu : filter.tendsto u filter.at_top filter.at_top)
(N : ℕ) :
If u is a sequence which is unbounded above,
then after any point, it reaches a value strictly greater than all previous values.
@[nolint]
theorem
filter.low_scores
{β : Type u_4}
[linear_order β]
[no_bot_order β]
{u : ℕ → β}
(hu : filter.tendsto u filter.at_top filter.at_bot)
(N : ℕ) :
If u is a sequence which is unbounded below,
then after any point, it reaches a value strictly smaller than all previous values.
theorem
filter.frequently_high_scores
{β : Type u_4}
[linear_order β]
[no_top_order β]
{u : ℕ → β}
(hu : filter.tendsto u filter.at_top filter.at_top) :
∃ᶠ (n : ℕ) in filter.at_top, ∀ (k : ℕ), k < 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_bot_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_top_order β]
{u : ℕ → β}
(hu : filter.tendsto u filter.at_top filter.at_top) :
∃ (φ : ℕ → ℕ), strict_mono φ ∧ strict_mono (u ∘ φ)
theorem
filter.strict_mono_subseq_of_id_le
{u : ℕ → ℕ}
(hu : ∀ (n : ℕ), n ≤ u n) :
∃ (φ : ℕ → ℕ), strict_mono φ ∧ strict_mono (u ∘ φ)
theorem
filter.tendsto_at_top_add_nonneg_left'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ᶠ (x : α) in l, 0 ≤ f x)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_left'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ᶠ (x : α) in l, f x ≤ 0)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_left
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ (x : α), 0 ≤ f x)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_left
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : ∀ (x : α), f x ≤ 0)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_right'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_top)
(hg : ∀ᶠ (x : α) in l, 0 ≤ g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_right'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_bot)
(hg : ∀ᶠ (x : α) in l, g x ≤ 0) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_right
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_top)
(hg : ∀ (x : α), 0 ≤ g x) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_right
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_bot)
(hg : ∀ (x : α), g x ≤ 0) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_top)
(hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l filter.at_bot)
(hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_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)
(a : 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 : α), C ≤ f x)
(a : 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 : α) 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)
(a : 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 : α), C ≤ g x)
(a : 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 : α) 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'
{α : 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
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
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.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_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_top_order β]
{f : α → β}
(h : filter.tendsto f filter.at_top filter.at_top) :
theorem
filter.unbounded_of_tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
[no_bot_order β]
{f : α → β}
(h : filter.tendsto f filter.at_top filter.at_bot) :
theorem
filter.unbounded_of_tendsto_at_top'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
[no_top_order β]
{f : α → β}
(h : filter.tendsto f filter.at_bot filter.at_top) :
theorem
filter.unbounded_of_tendsto_at_bot'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
[no_bot_order β]
{f : α → β}
(h : filter.tendsto f filter.at_bot filter.at_bot) :
theorem
filter.tendsto_at_top_of_monotone_of_filter
{ι : Type u_1}
{α : Type u_3}
[preorder ι]
[preorder α]
{l : filter ι}
{u : ι → α}
(h : monotone u)
[l.ne_bot]
(hu : filter.tendsto u l filter.at_top) :
If a monotone function u : ι → α tends to at_top along some non-trivial filter l, then
it tends to at_top along at_top.
theorem
filter.tendsto_at_bot_of_monotone_of_filter
{ι : Type u_1}
{α : Type u_3}
[preorder ι]
[preorder α]
{l : filter ι}
{u : ι → α}
(h : monotone u)
[l.ne_bot]
(hu : filter.tendsto u l filter.at_bot) :
If a monotone function u : ι → α tends to at_bot along some non-trivial filter l, then
it tends to at_bot along at_bot.
theorem
filter.tendsto_at_top_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[preorder ι]
[preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : monotone u)
{l : filter ι'}
[l.ne_bot]
(H : filter.tendsto (u ∘ φ) l filter.at_top) :
theorem
filter.tendsto_at_bot_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[preorder ι]
[preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : monotone u)
{l : filter ι'}
[l.ne_bot]
(H : filter.tendsto (u ∘ φ) l filter.at_bot) :
theorem
filter.map_at_top_finset_prod_le_of_prod_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[comm_monoid α]
{f : β → α}
{g : γ → α}
(h_eq : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ ∏ (x : γ) in u', g x = ∏ (b : β) in v', f b)) :
filter.map (λ (s : finset β), ∏ (b : β) in s, f b) filter.at_top ≤ filter.map (λ (s : finset γ), ∏ (x : γ) in s, g x) filter.at_top
Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient
condition for comparison of the filter at_top.map (λ s, ∏ b in s, f b) with
at_top.map (λ s, ∏ b in s, g b). This is useful to compare the set of limit points of
Π b in s, f b as s → at_top with the similar set for g.
theorem
filter.map_at_top_finset_sum_le_of_sum_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[add_comm_monoid α]
{f : β → α}
{g : γ → α}
(h_eq : ∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ ∑ (x : γ) in u', g x = ∑ (b : β) in v', f b)) :
filter.map (λ (s : finset β), ∑ (b : β) in s, f b) filter.at_top ≤ filter.map (λ (s : finset γ), ∑ (x : γ) in s, g x) filter.at_top
theorem
filter.has_antimono_basis.tendsto
{ι : Type u_1}
{α : Type u_3}
[semilattice_sup ι]
[nonempty ι]
{l : filter α}
{p : ι → Prop}
{s : ι → set α}
(hl : l.has_antimono_basis p s)
{φ : ι → α}
(h : ∀ (i : ι), φ i ∈ s i) :
theorem
filter.is_countably_generated.tendsto_iff_seq_tendsto
{α : Type u_3}
{β : Type u_4}
{f : α → β}
{k : filter α}
{l : filter β}
(hcb : k.is_countably_generated) :
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.is_countably_generated.tendsto_of_seq_tendsto
{α : Type u_3}
{β : Type u_4}
{f : α → β}
{k : filter α}
{l : filter β}
(hcb : k.is_countably_generated)
(a : ∀ (x : ℕ → α), filter.tendsto x filter.at_top k → filter.tendsto (f ∘ x) filter.at_top l) :
filter.tendsto f k l
theorem
filter.is_countably_generated.subseq_tendsto
{α : Type u_3}
{f : filter α}
(hf : f.is_countably_generated)
{u : ℕ → α}
(hx : (f ⊓ filter.map u filter.at_top).ne_bot) :
∃ (θ : ℕ → ℕ), strict_mono θ ∧ filter.tendsto (u ∘ θ) filter.at_top f
theorem
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.