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.

@[instance 200]

instance Filter.atTop.isCountablyGenerated {α : Type u_1} [Preorder α] [Countable α] : atTop.IsCountablyGenerated

@[instance 200]

instance Filter.atBot.isCountablyGenerated {α : Type u_1} [Preorder α] [Countable α] : atBot.IsCountablyGenerated

instance Filter.instIsCountablyGeneratedAtTopProd {α : Type u_1} {β : Type u_2} [Preorder α] [atTop.IsCountablyGenerated] [Preorder β] [atTop.IsCountablyGenerated] : atTop.IsCountablyGenerated

instance Filter.instIsCountablyGeneratedAtBotProd {α : Type u_1} {β : Type u_2} [Preorder α] [atBot.IsCountablyGenerated] [Preorder β] [atBot.IsCountablyGenerated] : atBot.IsCountablyGenerated

instance OrderDual.instIsCountablyGeneratedAtTop {α : Type u_1} [Preorder α] [Filter.atBot.IsCountablyGenerated] : Filter.atTop.IsCountablyGenerated

instance OrderDual.instIsCountablyGeneratedAtBot {α : Type u_1} [Preorder α] [Filter.atTop.IsCountablyGenerated] : Filter.atBot.IsCountablyGenerated

theorem Filter.atTop_countable_basis {α : Type u_1} [Preorder α] [IsDirectedOrder α] [Nonempty α] [Countable α] : atTop.HasCountableBasis (fun (x : α) => True) Set.Ici

theorem Filter.atBot_countable_basis {α : Type u_1} [Preorder α] [IsCodirectedOrder α] [Nonempty α] [Countable α] : atBot.HasCountableBasis (fun (x : α) => True) Set.Iic

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.

theorem Filter.exists_seq_monotone_tendsto_atTop_atTop (α : Type u_3) [Preorder α] [Nonempty α] [IsDirectedOrder α] [atTop.IsCountablyGenerated] : ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop

theorem Filter.exists_seq_antitone_tendsto_atTop_atBot (α : Type u_3) [Preorder α] [Nonempty α] [IsCodirectedOrder α] [atBot.IsCountablyGenerated] : ∃ (xs : ℕ → α), Antitone xs ∧ Tendsto xs atTop atBot

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.

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

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)

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)

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)

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)

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.

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

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