Enumerating a cofinitely convergent countable family by a sequence #
A countable family g : ι → α tending to a filter l along the cofinite filter can be listed,
with padding, as a sequence ℕ → α tending to l along atTop. The padding is a point b
lying in every member of l, such as the limit a when l = 𝓝 a. This turns a countable set
whose points outside each neighbourhood of a are finitely many into a sequence converging to
a, which is how null sequences are assembled from countably many finite sets.
theorem
Filter.Tendsto.exists_seq_tendsto_range_subset
{ι : Type u_1}
{α : Type u_2}
[Countable ι]
{g : ι → α}
{l : Filter α}
{b : α}
(hg : Tendsto g cofinite l)
(hb : pure b ≤ l)
:
A countable family tending to l along the cofinite filter is part of a sequence tending to
l, padded by a point b lying in every member of l.