# Basic results on `Filter.atTop` and `Filter.atBot` filters #

In this file we prove many lemmas like “if `f → +∞`, then `f ± c → +∞`”.

source
theorem Filter.hasAntitoneBasis_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] :
atTop.HasAntitoneBasis Set.Ici
source
theorem Filter.atTop_basis {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] :
atTop.HasBasis (fun (x : α) => True) Set.Ici
source
theorem Filter.atTop_basis_Ioi {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] [NoMaxOrder α] :
atTop.HasBasis (fun (x : α) => True) Set.Ioi
source
theorem Filter.atTop_basis_Ioi' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [NoMaxOrder α] (a : α) :
atTop.HasBasis (fun (x : α) => a < x) Set.Ioi
source
theorem Filter.atTop_basis' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (a : α) :
atTop.HasBasis (fun (x : α) => a ≤ x) Set.Ici
source
instance Filter.atTop_neBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] :
atTop.NeBot
source
theorem Filter.atTop_neBot_iff {α : Type u_6} [Preorder α] :
atTop.NeBot ↔ Nonempty α ∧ IsDirected α fun (x1 x2 : α) => x1 ≤ x2
source
theorem Filter.atBot_neBot_iff {α : Type u_6} [Preorder α] :
atBot.NeBot ↔ Nonempty α ∧ IsDirected α fun (x1 x2 : α) => x1 ≥ x2
source
@[simp]
theorem Filter.mem_atTop_sets {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] {s : Set α} :
s ∈ atTop ↔ ∃ (a : α), ∀ b ≥ a, b ∈ s
source
@[simp]
theorem Filter.eventually_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {p : α → Prop} [Nonempty α] :
(∀ᶠ (x : α) in atTop, p x) ↔ ∃ (a : α), ∀ b ≥ a, p b
source
theorem Filter.frequently_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {p : α → Prop} [Nonempty α] :
(∃ᶠ (x : α) in atTop, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b
source
theorem Filter.Eventually.exists_forall_of_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {p : α → Prop} [Nonempty α] :
(∀ᶠ (x : α) in atTop, p x) → ∃ (a : α), ∀ b ≥ a, p b

Alias of the forward direction of `Filter.eventually_atTop`.

source
theorem Filter.exists_eventually_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] {r : α → β → Prop} :
(∃ (b : β), ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ (b : β), ∀ a ≥ a₀, r a b
source
theorem Filter.map_atTop_eq {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] {f : α → β} :
map f atTop = ⨅ (a : α), principal (f '' {a' : α | a ≤ a'})
source
theorem Filter.frequently_atTop' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {p : α → Prop} [Nonempty α] [NoMaxOrder α] :
(∃ᶠ (x : α) in atTop, p x) ↔ ∀ (a : α), ∃ b > a, p b
source
theorem Filter.atBot_basis_Iio {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] [NoMinOrder α] :
atBot.HasBasis (fun (x : α) => True) Set.Iio
source
theorem Filter.atBot_basis_Iio' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [NoMinOrder α] (a : α) :
atBot.HasBasis (fun (x : α) => x < a) Set.Iio
source
theorem Filter.atBot_basis' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] (a : α) :
atBot.HasBasis (fun (x : α) => x ≤ a) Set.Iic
source
theorem Filter.atBot_basis {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] :
atBot.HasBasis (fun (x : α) => True) Set.Iic
source
instance Filter.atBot_neBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] :
atBot.NeBot
source
@[simp]
theorem Filter.mem_atBot_sets {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] {s : Set α} :
s ∈ atBot ↔ ∃ (a : α), ∀ b ≤ a, b ∈ s
source
@[simp]
theorem Filter.eventually_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {p : α → Prop} [Nonempty α] :
(∀ᶠ (x : α) in atBot, p x) ↔ ∃ (a : α), ∀ b ≤ a, p b
source
theorem Filter.frequently_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {p : α → Prop} [Nonempty α] :
(∃ᶠ (x : α) in atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b
source
theorem Filter.Eventually.exists_forall_of_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {p : α → Prop} [Nonempty α] :
(∀ᶠ (x : α) in atBot, p x) → ∃ (a : α), ∀ b ≤ a, p b

Alias of the forward direction of `Filter.eventually_atBot`.

source
theorem Filter.exists_eventually_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] {r : α → β → Prop} :
(∃ (b : β), ∀ᶠ (a : α) in atBot, r a b) ↔ ∀ᶠ (a₀ : α) in atBot, ∃ (b : β), ∀ a ≤ a₀, r a b
source
theorem Filter.map_atBot_eq {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] {f : α → β} :
map f atBot = ⨅ (a : α), principal (f '' {a' : α | a' ≤ a})
source
theorem Filter.frequently_atBot' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {p : α → Prop} [Nonempty α] [NoMinOrder α] :
(∃ᶠ (x : α) in atBot, p x) ↔ ∀ (a : α), ∃ b < a, p b

### Sequences #

source
theorem Filter.extraction_of_frequently_atTop {P : ℕ → Prop} (h : ∃ᶠ (n : ℕ) in atTop, P n) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
source
theorem Filter.extraction_of_eventually_atTop {P : ℕ → Prop} (h : ∀ᶠ (n : ℕ) in atTop, P n) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
source
theorem Filter.extraction_forall_of_frequently {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
source
theorem Filter.extraction_forall_of_eventually {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
source
theorem Filter.extraction_forall_of_eventually' {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, P n k) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
source
theorem Filter.inf_map_atTop_neBot_iff {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {F : Filter β} {u : α → β} [Nonempty α] :
(F ⊓ map u atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
source
theorem Filter.exists_le_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {u : α → β} [Preorder β] (h : Tendsto u atTop atTop) (a : α) (b : β) :
∃ a' ≥ a, b ≤ u a'
source
theorem Filter.exists_le_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {u : α → β} [Preorder β] (h : Tendsto u atTop atBot) (a : α) (b : β) :
∃ a' ≥ a, u a' ≤ b
source
theorem Filter.exists_lt_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {u : α → β} [Preorder β] [NoMaxOrder β] (h : Tendsto u atTop atTop) (a : α) (b : β) :
∃ a' ≥ a, b < u a'
source
theorem Filter.exists_lt_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {u : α → β} [Preorder β] [NoMinOrder β] (h : Tendsto u atTop atBot) (a : α) (b : β) :
∃ a' ≥ a, u a' < b
source
theorem Filter.inf_map_atBot_neBot_iff {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {F : Filter β} {u : α → β} :
(F ⊓ map u atBot).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U
source
theorem Filter.tendsto_atTop' {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} {l : Filter β} :
Tendsto f atTop l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≥ a, f b ∈ s
source
theorem Filter.tendsto_atTop_principal {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} {s : Set β} :
Tendsto f atTop (principal s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
source
theorem Filter.tendsto_atTop_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} [Preorder β] :
Tendsto f atTop atTop ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≤ f a

A function `f` grows to `+∞` independent of an order-preserving embedding `e`.

source
theorem Filter.tendsto_atTop_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} [Preorder β] :
Tendsto f atTop atBot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → f a ≤ b
source
theorem Filter.tendsto_atTop_atTop_iff_of_monotone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} [Preorder β] (hf : Monotone f) :
Tendsto f atTop atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
source
theorem Filter.tendsto_atTop_atBot_iff_of_antitone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} [Preorder β] (hf : Antitone f) :
Tendsto f atTop atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
source
theorem Filter.tendsto_atBot' {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} {l : Filter β} :
Tendsto f atBot l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≤ a, f b ∈ s
source
theorem Filter.tendsto_atBot_principal {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} {s : Set β} :
Tendsto f atBot (principal s) ↔ ∃ (N : α), ∀ n ≤ N, f n ∈ s
source
theorem Filter.tendsto_atBot_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} [Preorder β] :
Tendsto f atBot atTop ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, b ≤ f a
source
theorem Filter.tendsto_atBot_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} [Preorder β] :
Tendsto f atBot atBot ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, f a ≤ b
source
theorem Filter.tendsto_atBot_atBot_iff_of_monotone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} [Preorder β] (hf : Monotone f) :
Tendsto f atBot atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
source
theorem Filter.tendsto_atBot_atTop_iff_of_antitone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} [Preorder β] (hf : Antitone f) :
Tendsto f atBot atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
source
theorem Monotone.tendsto_atTop_atTop_iff {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {f : α → β} [Preorder β] (hf : Monotone f) :
Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a

Alias of `Filter.tendsto_atTop_atTop_iff_of_monotone`.

source
theorem Monotone.tendsto_atBot_atBot_iff {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {f : α → β} [Preorder β] (hf : Monotone f) :
Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b

Alias of `Filter.tendsto_atBot_atBot_iff_of_monotone`.

source
theorem Filter.Tendsto.subseq_mem {α : Type u_3} {F : Filter α} {V : ℕ → Set α} (h : ∀ (n : ℕ), V n ∈ F) {u : ℕ → α} (hu : Tendsto u atTop F) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), u (φ n) ∈ V n
source
theorem Filter.map_atTop_eq_of_gc_preorder {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {f : α → β} (hf : Monotone f) (b : β) (hgi : ∀ c ≥ b, ∃ (x : α), f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x) :
map f atTop = atTop

A function `f` maps upwards closed sets (atTop 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 connection above `b`.

source
theorem Filter.map_atTop_eq_of_gc {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [PartialOrder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {f : α → β} (g : β → α) (b : β) (hf : Monotone f) (gc : ∀ (a : α), ∀ c ≥ b, f a ≤ c ↔ a ≤ g c) (hgi : ∀ c ≥ b, c ≤ f (g c)) :
map f atTop = atTop

A function `f` maps upwards closed sets (atTop 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 connection above `b`.

source
theorem Filter.map_atBot_eq_of_gc_preorder {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] {f : α → β} (hf : Monotone f) (b : β) (hgi : ∀ c ≤ b, ∃ (x : α), f x = c ∧ ∀ (a : α), c ≤ f a ↔ x ≤ a) :
map f atBot = atBot
source
theorem Filter.map_atBot_eq_of_gc {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [PartialOrder β] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] {f : α → β} (g : β → α) (b' : β) (hf : Monotone f) (gc : ∀ (a : α), ∀ b ≤ b', b ≤ f a ↔ g b ≤ a) (hgi : ∀ b ≤ b', f (g b) ≤ b) :
map f atBot = atBot
source
theorem Filter.map_val_atTop_of_Ici_subset {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {a : α} {s : Set α} (h : Set.Ici a ⊆ s) :
map Subtype.val atTop = atTop
source
@[simp]
theorem Nat.map_cast_int_atTop :
Filter.map Nat.cast Filter.atTop = Filter.atTop
source
@[simp]
theorem Filter.map_val_Ici_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (a : α) :
map Subtype.val atTop = atTop

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

source
@[simp]
theorem Filter.map_val_Ioi_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [NoMaxOrder α] (a : α) :
map Subtype.val atTop = atTop

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

source
theorem Filter.atTop_Ioi_eq {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (a : α) :
atTop = comap Subtype.val atTop

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

source
theorem Filter.atTop_Ici_eq {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (a : α) :
atTop = comap Subtype.val atTop

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

source
@[simp]
theorem Filter.map_val_Iio_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [NoMinOrder α] (a : α) :
map Subtype.val atBot = atBot

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

source
theorem Filter.atBot_Iio_eq {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] (a : α) :
atBot = comap Subtype.val atBot

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

source
@[simp]
theorem Filter.map_val_Iic_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] (a : α) :
map Subtype.val atBot = atBot

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

source
theorem Filter.atBot_Iic_eq {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] (a : α) :
atBot = comap Subtype.val atBot

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

source
theorem Filter.tendsto_Ioi_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {a : α} {f : β → ↑(Set.Ioi a)} {l : Filter β} :
Tendsto f l atTop ↔ Tendsto (fun (x : β) => ↑(f x)) l atTop
source
theorem Filter.tendsto_Iio_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {a : α} {f : β → ↑(Set.Iio a)} {l : Filter β} :
Tendsto f l atBot ↔ Tendsto (fun (x : β) => ↑(f x)) l atBot
source
theorem Filter.tendsto_Ici_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {a : α} {f : β → ↑(Set.Ici a)} {l : Filter β} :
Tendsto f l atTop ↔ Tendsto (fun (x : β) => ↑(f x)) l atTop
source
theorem Filter.tendsto_Iic_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {a : α} {f : β → ↑(Set.Iic a)} {l : Filter β} :
Tendsto f l atBot ↔ Tendsto (fun (x : β) => ↑(f x)) l atBot
source
@[simp]
theorem Filter.tendsto_comp_val_Ioi_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [NoMaxOrder α] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun (x : ↑(Set.Ioi a)) => f ↑x) atTop l ↔ Tendsto f atTop l
source
@[simp]
theorem Filter.tendsto_comp_val_Ici_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun (x : ↑(Set.Ici a)) => f ↑x) atTop l ↔ Tendsto f atTop l
source
@[simp]
theorem Filter.tendsto_comp_val_Iio_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [NoMinOrder α] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun (x : ↑(Set.Iio a)) => f ↑x) atBot l ↔ Tendsto f atBot l
source
@[simp]
theorem Filter.tendsto_comp_val_Iic_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun (x : ↑(Set.Iic a)) => f ↑x) atBot l ↔ Tendsto f atBot l
source
theorem Filter.map_add_atTop_eq_nat (k : ℕ) :
map (fun (a : ℕ) => a + k) atTop = atTop
source
theorem Filter.map_sub_atTop_eq_nat (k : ℕ) :
map (fun (a : ℕ) => a - k) atTop = atTop
source
theorem Filter.tendsto_add_atTop_nat (k : ℕ) :
Tendsto (fun (a : ℕ) => a + k) atTop atTop
source
theorem Filter.tendsto_sub_atTop_nat (k : ℕ) :
Tendsto (fun (a : ℕ) => a - k) atTop atTop
source
theorem Filter.tendsto_add_atTop_iff_nat {α : Type u_3} {f : ℕ → α} {l : Filter α} (k : ℕ) :
Tendsto (fun (n : ℕ) => f (n + k)) atTop l ↔ Tendsto f atTop l
source
theorem Filter.map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) :
map (fun (a : ℕ) => a / k) atTop = atTop
source
theorem Filter.not_bddAbove_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMaxOrder β] (h : Tendsto f l atTop) :
¬BddAbove (Set.range f)
source
theorem Filter.not_bddBelow_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMinOrder β] (h : Tendsto f l atBot) :
¬BddBelow (Set.range f)
source
@[deprecated Filter.not_bddAbove_of_tendsto_atTop (since := "2025-04-28")]
theorem Filter.unbounded_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMaxOrder β] (h : Tendsto f l atTop) :
¬BddAbove (Set.range f)

Alias of `Filter.not_bddAbove_of_tendsto_atTop`.

source
@[deprecated Filter.not_bddBelow_of_tendsto_atBot (since := "2025-04-28")]
theorem Filter.unbounded_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMinOrder β] (h : Tendsto f l atBot) :
¬BddBelow (Set.range f)

Alias of `Filter.not_bddBelow_of_tendsto_atBot`.

source
@[deprecated Filter.not_bddAbove_of_tendsto_atTop (since := "2025-04-28")]
theorem Filter.unbounded_of_tendsto_atTop' {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMaxOrder β] (h : Tendsto f l atTop) :
¬BddAbove (Set.range f)

Alias of `Filter.not_bddAbove_of_tendsto_atTop`.

source
@[deprecated Filter.not_bddBelow_of_tendsto_atBot (since := "2025-04-28")]
theorem Filter.unbounded_of_tendsto_atBot' {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMinOrder β] (h : Tendsto f l atBot) :
¬BddBelow (Set.range f)

Alias of `Filter.not_bddBelow_of_tendsto_atBot`.

source
theorem Filter.HasAntitoneBasis.eventually_subset {ι : Type u_1} {α : Type u_3} [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {t : Set α} (ht : t ∈ l) :
∀ᶠ (i : ι) in atTop, s i ⊆ t
source
theorem Filter.HasAntitoneBasis.tendsto {ι : Type u_1} {α : Type u_3} [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {φ : ι → α} (h : ∀ (i : ι), φ i ∈ s i) :
Tendsto φ atTop l
source
theorem Filter.HasAntitoneBasis.comp_mono {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Nonempty ι] [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Preorder ι'] {l : Filter α} {s : ι' → Set α} (hs : l.HasAntitoneBasis s) {φ : ι → ι'} (φ_mono : Monotone φ) (hφ : Tendsto φ atTop atTop) :
l.HasAntitoneBasis (s ∘ φ)
source
theorem Filter.HasAntitoneBasis.comp_strictMono {α : Type u_3} {l : Filter α} {s : ℕ → Set α} (hs : l.HasAntitoneBasis s) {φ : ℕ → ℕ} (hφ : StrictMono φ) :
l.HasAntitoneBasis (s ∘ φ)
source
theorem Filter.subseq_forall_of_frequently {ι : Type u_6} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι} (h_tendsto : Tendsto x atTop l) (h : ∃ᶠ (n : ℕ) in atTop, p (x n)) :
∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))