tendsto_subseq — Mathlib

English

In a first-countable space, a cluster point x of a sequence has a subsequence converging to x.

Русский

В пространстве с первой счётностью у кластера последовательности существует подпоследовательность, сходящаяся к кластерной точке x.

LaTeX

$$[FirstCountableTopology α] implies: ∃ subseq ψ such that Tendsto (u ∘ ψ) atTop (nhds x)$$

Lean4

/-- In a first-countable space, a cluster point `x` of a sequence
is the limit of some subsequence. -/
theorem tendsto_subseq [FirstCountableTopology α] {u : ℕ → α} {x : α} (hx : MapClusterPt x atTop u) :
    ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x) :=
  subseq_tendsto_of_neBot hx

Похожие утверждения