English
If u is CauchySeq and f is a convergent subsequence of indices, then u converges to the same limit along atTop.
Русский
Если у есть КошиSeq, и подпоследовательность индексов сходится, то u сходится к той же границе вдоль atTop.
LaTeX
$$$\\text{CauchySeq}(u) \\Rightarrow \\forall ι, f:\\, ι\\to β,\\ p:Filter ι, \\text{Tendsto } f p atTop \\land \\text{Tendsto } (u\\circ f) p (nhds a) \\Rightarrow \\text{Tendsto } u atTop (nhds a).$$$
Lean4
/-- If a Cauchy sequence has a convergent subsequence, then it converges. -/
theorem tendsto_nhds_of_cauchySeq_of_subseq [Preorder β] {u : β → α} (hu : CauchySeq u) {ι : Type*} {f : ι → β}
{p : Filter ι} [NeBot p] (hf : Tendsto f p atTop) {a : α} (ha : Tendsto (u ∘ f) p (𝓝 a)) : Tendsto u atTop (𝓝 a) :=
le_nhds_of_cauchy_adhp hu (ha.mapClusterPt.of_comp hf)
