tendsto_subseq — Mathlib

English

From frequently visited points in a seq-compact set, extract a subsequence converging to a point in the set.

Русский

Из часто встречающихся точек в seq-замкнутом множестве извлечь подпоследовательность, сходящуюся к точке множества.

LaTeX

$$$\text{IsSeqCompact}(s) \to \text{Frequently}(\lambda n. x_n\in s) \Rightarrow \exists a\in s, \exists \phi, \text{StrictMono}(\phi) \land \text{Tendsto}(x\circ \phi) atTop (\mathcal{N}(a))$$$

Lean4

theorem tendsto_subseq [SeqCompactSpace X] (x : ℕ → X) :
    ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a) :=
  let ⟨a, _, φ, mono, h⟩ := isSeqCompact_univ fun n => mem_univ (x n)
  ⟨a, φ, mono, h⟩

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