isSeqCompact — Mathlib

English

In a SeqCompactSpace X, every sequence has a subsequence converging to some limit.

Русский

В SeqCompactSpace X каждая последовательность имеет подпоследовательность, сходящуюся к пределу.

LaTeX

$$$[SeqCompactSpace X] (x: \mathbb{N} \to X) \Rightarrow \exists a: X, \exists \phi: \mathbb{N} \to \mathbb{N}, \text{StrictMono}(\phi) \land \text{Tendsto}(x \circ \phi) atTop (\mathcal{N}(a))$$$

Lean4

protected theorem isSeqCompact {s : Set X} (hs : IsCompact s) : IsSeqCompact s := fun _x x_in =>
  let ⟨a, a_in, ha⟩ := hs (tendsto_principal.mpr (Eventually.of_forall x_in))
  ⟨a, a_in, tendsto_subseq ha⟩

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