Theorems · Theorem · general topology

Filter.tendsto_of_subseq_tendsto

∀ {α : Type u_1} {ι : Type u_3} {x : ι → α} {f : Filter α} {l : Filter ι} [l.IsCountablyGenerated],
  (∀ (ns : ℕ → ι), Filter.Tendsto ns Filter.atTop l → ∃ ms, Filter.Tendsto (fun n => x (ns (ms n))) Filter.atTop f) →
    Filter.Tendsto x l f

A sequence converges if every subsequence has a convergent subsequence.

Defined in

Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Cited by

3 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Filter.IsCountablyGenerated