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 : α), filter.principal {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 : α), filter.principal {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 (has_pure.pure (f ⊤))
theorem
filter.tendsto_at_bot_pure
{α : Type u_3}
{β : Type u_4}
[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} :
(∀ᶠ (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} :
(∀ᶠ (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 : α), 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₂ : α → β⦄ :
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₂ : α → β⦄ :
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 : α → β} :
(∀ (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 : α → β} :
(∀ (n : α), f n ≤ g n) → filter.tendsto g l filter.at_bot → filter.tendsto f l filter.at_bot
Sequences
theorem
filter.inf_map_at_top_ne_bot_iff
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[nonempty α]
{F : filter β}
{u : α → β} :
(F ⊓ filter.map u filter.at_top).ne_bot ↔ ∀ (U : set β), U ∈ F → ∀ (N : α), ∃ (n : α) (H : n ≥ N), u n ∈ U
theorem
filter.inf_map_at_bot_ne_bot_iff
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[nonempty α]
{F : filter β}
{u : α → β} :
(F ⊓ filter.map u filter.at_bot).ne_bot ↔ ∀ (U : set β), U ∈ F → ∀ (N : α), ∃ (n : α) (H : n ≤ N), u n ∈ U
theorem
filter.extraction_of_frequently_at_top
{P : ℕ → Prop} :
(∃ᶠ (n : ℕ) in filter.at_top, P n) → (∃ (φ : ℕ → ℕ), strict_mono φ ∧ ∀ (n : ℕ), P (φ n))
theorem
filter.extraction_of_eventually_at_top
{P : ℕ → Prop} :
(∀ᶠ (n : ℕ) in filter.at_top, P n) → (∃ (φ : ℕ → ℕ), strict_mono φ ∧ ∀ (n : ℕ), P (φ n))
theorem
filter.exists_le_of_tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[preorder β]
{u : α → β}
(h : filter.tendsto u filter.at_top filter.at_top)
(a : α)
(b : β) :
@[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 : ℕ → β} :
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 : ℕ → β} :
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 : ℕ → β} :
filter.tendsto u filter.at_top filter.at_top → (∃ (φ : ℕ → ℕ), strict_mono φ ∧ strict_mono (u ∘ φ))
theorem
filter.strict_mono_subseq_of_id_le
{u : ℕ → ℕ} :
(∀ (n : ℕ), n ≤ u n) → (∃ (φ : ℕ → ℕ), strict_mono φ ∧ strict_mono (u ∘ φ))
theorem
filter.tendsto_at_top_add_nonneg_left'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β} :
(∀ᶠ (x : α) in l, 0 ≤ f x) → filter.tendsto g l filter.at_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 : α → β} :
(∀ᶠ (x : α) in l, f x ≤ 0) → 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 : α → β} :
(∀ (x : α), 0 ≤ f x) → 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 : α → β} :
(∀ (x : α), f x ≤ 0) → 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 : α → β} :
filter.tendsto f l filter.at_top → (∀ᶠ (x : α) in l, 0 ≤ g x) → filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_right'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β} :
filter.tendsto f l filter.at_bot → (∀ᶠ (x : α) in l, g x ≤ 0) → filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_nonneg_right
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β} :
filter.tendsto f l filter.at_top → (∀ (x : α), 0 ≤ g x) → filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_nonpos_right
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β} :
filter.tendsto f l filter.at_bot → (∀ (x : α), g x ≤ 0) → filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_monoid β]
{l : filter α}
{f g : α → β} :
filter.tendsto f l filter.at_top → 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 : α → β} :
filter.tendsto f l filter.at_bot → 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 : β) :
filter.tendsto (λ (x : α), C + f x) l filter.at_top → filter.tendsto f 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 : β) :
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 : β) :
filter.tendsto (λ (x : α), f x + C) l filter.at_top → filter.tendsto f 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 : β) :
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 : β) :
(∀ᶠ (x : α) in l, 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 : β) :
(∀ᶠ (x : α) in l, 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_left
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(C : β) :
(∀ (x : α), f x ≤ C) → filter.tendsto (λ (x : α), f x + g x) l filter.at_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 : β) :
(∀ (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 : β) :
(∀ᶠ (x : α) in l, 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 : β) :
(∀ᶠ (x : α) in l, 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_of_add_bdd_above_right
{α : Type u_3}
{β : Type u_4}
[ordered_cancel_add_comm_monoid β]
{l : filter α}
{f g : α → β}
(C : β) :
(∀ (x : α), g x ≤ C) → filter.tendsto (λ (x : α), f x + g x) l filter.at_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 : β) :
(∀ (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 : β) :
(∀ᶠ (x : α) in l, C ≤ f x) → 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 : β) :
(∀ᶠ (x : α) in l, f x ≤ C) → 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 : β) :
(∀ (x : α), C ≤ f x) → 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 : β) :
(∀ (x : α), f x ≤ C) → 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 : β) :
filter.tendsto f l filter.at_top → (∀ᶠ (x : α) in l, C ≤ g x) → filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_right_of_ge'
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_group β]
(l : filter α)
{f g : α → β}
(C : β) :
filter.tendsto f l filter.at_bot → (∀ᶠ (x : α) in l, g x ≤ C) → filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_right_of_le
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_group β]
(l : filter α)
{f g : α → β}
(C : β) :
filter.tendsto f l filter.at_top → (∀ (x : α), C ≤ g x) → filter.tendsto (λ (x : α), f x + g x) l filter.at_top
theorem
filter.tendsto_at_bot_add_right_of_ge
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_group β]
(l : filter α)
{f g : α → β}
(C : β) :
filter.tendsto f l filter.at_bot → (∀ (x : α), g x ≤ C) → filter.tendsto (λ (x : α), f x + g x) l filter.at_bot
theorem
filter.tendsto_at_top_add_const_left
{α : Type u_3}
{β : Type u_4}
[ordered_add_comm_group β]
(l : filter α)
{f : α → β}
(C : β) :
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 : β) :
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 : β) :
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 : β) :
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 (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_embedding
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[preorder β]
[preorder γ]
{f : α → β}
{e : β → γ}
{l : filter α} :
(∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) → (∀ (c : γ), ∃ (b : β), c ≤ e b) → (filter.tendsto (e ∘ f) l filter.at_top ↔ filter.tendsto f l filter.at_top)
A function f grows to +∞ independent of an order-preserving embedding e.
theorem
filter.tendsto_at_bot_embedding
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[preorder β]
[preorder γ]
{f : α → β}
{e : β → γ}
{l : filter α} :
(∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) → (∀ (c : γ), ∃ (b : β), e b ≤ c) → (filter.tendsto (e ∘ f) l filter.at_bot ↔ filter.tendsto f l filter.at_bot)
A function f goes to -∞ independent of an order-preserving embedding e.
theorem
filter.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
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 : α → β} :
monotone f → (∀ (b : β), ∃ (a : α), b ≤ f a) → filter.tendsto f filter.at_top filter.at_top
theorem
filter.tendsto_at_bot_at_bot_of_monotone
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : α → β} :
monotone f → (∀ (b : β), ∃ (a : α), f a ≤ b) → filter.tendsto f filter.at_bot filter.at_bot
theorem
filter.tendsto_at_top_at_top_iff_of_monotone
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
{f : α → β} :
monotone f → (filter.tendsto f filter.at_top filter.at_top ↔ ∀ (b : β), ∃ (a : α), b ≤ f a)
theorem
filter.tendsto_at_bot_at_bot_iff_of_monotone
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
{f : α → β} :
monotone f → (filter.tendsto f filter.at_bot filter.at_bot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b)
theorem
filter.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 α} :
monotone f → (∀ (x : α), ∃ (n : β), x ∈ f n) → filter.tendsto f filter.at_top filter.at_top
If f is a monotone sequence of finsets and each x belongs to one of f n, then
tendsto f at_top at_top.
theorem
filter.tendsto_finset_image_at_top_at_top
{β : Type u_4}
{γ : Type u_5}
{i : β → γ}
{j : γ → β} :
theorem
filter.tendsto_finset_preimage_at_top_at_top
{α : Type u_3}
{β : Type u_4}
{f : α → β}
(hf : function.injective f) :
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).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.map_at_top_eq_of_gc
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[semilattice_sup β]
{f : α → β}
(g : β → α)
(b' : β) :
monotone f → (∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)) → (∀ (b : β), b ≥ b' → b ≤ f (g b)) → filter.map f filter.at_top = filter.at_top
A function f maps upwards closed sets (at_top sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connetion above b'.
theorem
filter.map_at_bot_eq_of_gc
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[semilattice_inf β]
{f : α → β}
(g : β → α)
(b' : β) :
monotone f → (∀ (a : α) (b : β), b ≤ b' → (b ≤ f a ↔ g b ≤ a)) → (∀ (b : β), b ≤ b' → f (g b) ≤ b) → filter.map f filter.at_bot = filter.at_bot
theorem
filter.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 : ℕ) :
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 : ι → α} :
monotone u → ¬bdd_above (set.range u) → filter.tendsto u filter.at_top filter.at_top
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 : ι → α} :
monotone u → ¬bdd_below (set.range u) → filter.tendsto u filter.at_bot filter.at_bot
If u is a monotone function with linear ordered codomain and the range of u is not bounded
below, then tendsto u at_bot at_bot.
theorem
filter.unbounded_of_tendsto_at_top
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
[no_top_order β]
{f : α → β} :
theorem
filter.unbounded_of_tendsto_at_bot
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_sup α]
[preorder β]
[no_bot_order β]
{f : α → β} :
theorem
filter.unbounded_of_tendsto_at_top'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
[no_top_order β]
{f : α → β} :
theorem
filter.unbounded_of_tendsto_at_bot'
{α : Type u_3}
{β : Type u_4}
[nonempty α]
[semilattice_inf α]
[preorder β]
[no_bot_order β]
{f : α → β} :
theorem
filter.tendsto_at_top_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[preorder ι]
[preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : monotone u)
{l : filter ι'}
[l.ne_bot] :
filter.tendsto (u ∘ φ) l filter.at_top → filter.tendsto u filter.at_top 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] :
filter.tendsto (u ∘ φ) l filter.at_bot → filter.tendsto u filter.at_bot filter.at_bot
theorem
filter.map_at_top_finset_sum_le_of_sum_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[add_comm_monoid α]
{f : β → α}
{g : γ → α} :
(∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ 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
theorem
filter.map_at_top_finset_prod_le_of_prod_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[comm_monoid α]
{f : β → α}
{g : γ → α} :
(∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ 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.has_antimono_basis.tendsto
{ι : Type u_1}
{α : Type u_3}
[semilattice_sup ι]
[nonempty ι]
{l : filter α}
{p : ι → Prop}
{s : ι → set α}
(hl : l.has_antimono_basis p s)
{φ : ι → α} :
(∀ (i : ι), φ i ∈ s i) → filter.tendsto φ filter.at_top l
theorem
filter.is_countably_generated.tendsto_iff_seq_tendsto
{α : Type u_3}
{β : Type u_4}
{f : α → β}
{k : filter α}
{l : filter β} :
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 β} :
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.is_countably_generated.subseq_tendsto
{α : Type u_3}
{f : filter α}
(hf : f.is_countably_generated)
{u : ℕ → α} :
(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 : β → α} :
(∀ (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.
theorem
function.injective.map_at_top_finset_prod_eq
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[comm_monoid α]
{g : γ → β}
(hg : function.injective g)
{f : β → α} :
(∀ (x : β), x ∉ set.range g → f x = 1) → filter.map (λ (s : finset γ), s.prod (λ (i : γ), f (g i))) filter.at_top = filter.map (λ (s : finset β), s.prod (λ (i : β), 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.