English
A subset S of a topological space X is sequentially compact if every sequence taking values in S has a convergent subsequence.
Русский
Подмножество S пространства X последовательносно компактно, если каждая последовательность из S имеет сходящуюся подпоследовательность.
LaTeX
$$$\\text{IsSeqCompact}(S) \\iff \\forall x: \\mathbb{N} \\to X, (\\forall n, x(n) \\in S) \\to \\exists a \\in S, \\exists \\phi: \\mathbb{N} \\to \\mathbb{N}, \\text{StrictMono}(\\phi) \\land \\text{Tendsto} (x \\circ \\phi) \\text{atTop} (\\mathcal{N} a)$$$
Lean4
/-- A set `s` is sequentially compact if every sequence taking values in `s` has a
converging subsequence. -/
def IsSeqCompact (s : Set X) :=
∀ ⦃x : ℕ → X⦄, (∀ n, x n ∈ s) → ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
