# Convergence to infinity and countably generated filters #

In this file we prove that

- `Filter.atTop` and `Filter.atBot` filters on a countable type are countably generated;
- `Filter.exists_seq_tendsto`: if `f` is a nontrivial countably generated filter, then there exists a sequence that converges. to `f`;
- `Filter.tendsto_iff_seq_tendsto`: convergence along a countably generated filter is equivalent to convergence along all sequences that converge to this filter.

source
@[instance 200]
instance Filter.atTop.isCountablyGenerated {α : Type u_1} [Preorder α] [Countable α] :
atTop.IsCountablyGenerated
source
@[instance 200]
instance Filter.atBot.isCountablyGenerated {α : Type u_1} [Preorder α] [Countable α] :
atBot.IsCountablyGenerated
source
instance Filter.instIsCountablyGeneratedAtTopProd {α : Type u_1} {β : Type u_2} [Preorder α] [atTop.IsCountablyGenerated] [Preorder β] [atTop.IsCountablyGenerated] :
atTop.IsCountablyGenerated
source
instance Filter.instIsCountablyGeneratedAtBotProd {α : Type u_1} {β : Type u_2} [Preorder α] [atBot.IsCountablyGenerated] [Preorder β] [atBot.IsCountablyGenerated] :
atBot.IsCountablyGenerated
source
instance OrderDual.instIsCountablyGeneratedAtTop {α : Type u_1} [Preorder α] [Filter.atBot.IsCountablyGenerated] :
Filter.atTop.IsCountablyGenerated
source
instance OrderDual.instIsCountablyGeneratedAtBot {α : Type u_1} [Preorder α] [Filter.atTop.IsCountablyGenerated] :
Filter.atBot.IsCountablyGenerated
source
theorem Filter.atTop_countable_basis {α : Type u_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] [Countable α] :
atTop.HasCountableBasis (fun (x : α) => True) Set.Ici
source
theorem Filter.atBot_countable_basis {α : Type u_1} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] [Countable α] :
atBot.HasCountableBasis (fun (x : α) => True) Set.Iic
source
theorem Filter.exists_seq_tendsto {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated] [f.NeBot] :
∃ (x : ℕ → α), Tendsto x atTop f

If `f` is a nontrivial countably generated filter, then there exists a sequence that converges to `f`.

source
theorem Filter.exists_seq_monotone_tendsto_atTop_atTop (α : Type u_3) [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [atTop.IsCountablyGenerated] :
∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
source
theorem Filter.exists_seq_antitone_tendsto_atTop_atBot (α : Type u_3) [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [atBot.IsCountablyGenerated] :
∃ (xs : ℕ → α), Antitone xs ∧ Tendsto xs atTop atBot
source
theorem Filter.tendsto_iff_seq_tendsto {α : Type u_1} {β : Type u_2} {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop 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`.

source
theorem Filter.tendsto_of_seq_tendsto {α : Type u_1} {β : Type u_2} {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
(∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l) → Tendsto f k l
source
theorem Filter.eventually_iff_seq_eventually {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
(∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
source
theorem Filter.frequently_iff_seq_frequently {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
(∃ᶠ (n : ι) in l, p n) ↔ ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
source
theorem Filter.exists_seq_forall_of_frequently {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] (h : ∃ᶠ (n : ι) in l, p n) :
∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
source
theorem Filter.frequently_iff_seq_forall {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
(∃ᶠ (n : ι) in l, p n) ↔ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
source
theorem Filter.tendsto_of_subseq_tendsto {α : Type u_1} {ι : Type u_3} {x : ι → α} {f : Filter α} {l : Filter ι} [l.IsCountablyGenerated] (hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ (ms : ℕ → ℕ), Tendsto (fun (n : ℕ) => x (ns (ms n))) atTop f) :
Tendsto x l f

A sequence converges if every subsequence has a convergent subsequence.

source
theorem Filter.subseq_tendsto_of_neBot {α : Type u_1} {f : Filter α} [f.IsCountablyGenerated] {u : ℕ → α} (hx : (f ⊓ map u atTop).NeBot) :
∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f