English
If every subsequence of a sequence x indexed by ι admits a further subsequence converging to f along the target filter f, then x converges to f along l. More precisely, whenever for all ns: ℕ → ι with Tendsto ns atTop l there exists a further index-mapping ms: ℕ → ℕ with Tendsto (x ∘ (ns ∘ ms)) atTop f, we have Tendsto x l f.
Русский
Если для любой подпоследовательности x_n индексации ι существует далее подпоследовательность, сходящаяся к пределy f по фильтру f, тогда исходная последовательность x удовлетворяет пределу f по фильтру l. Точнее: если для всех ns: ℕ → ι с Tendsto ns atTop l существует ms: ℕ → ℕ с Tendsto (x (ns (ms n))) atTop f, то x стремится к f по l.
LaTeX
$$$\\forall (ns: \\mathbb{N} \\to \\iota),\\ Tendsto\\ ns\\ atTop\\ l\\ \\Rightarrow\\ \\exists ms: \\mathbb{N} \\to \\mathbb{N},\\ Tendsto (x \\circ (ns \\circ ms))\\ atTop\\ f\\quad\\Rightarrow\\quad \\ Tendsto\\ x\\ l\\ f.$$$
Lean4
/-- A sequence converges if every subsequence has a convergent subsequence. -/
theorem tendsto_of_subseq_tendsto {ι : Type*} {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 := by
contrapose! hxy
obtain ⟨s, hs, hfreq⟩ : ∃ s ∈ f, ∃ᶠ n in l, x n ∉ s := by rwa [not_tendsto_iff_exists_frequently_notMem] at hxy
obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq
refine ⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩
rcases (hms_tendsto.eventually_mem hs).exists with ⟨n, hn⟩
exact absurd hn <| hy_freq _
