English
The sequential closure of a set s ⊆ X is the set of all a ∈ X that arise as limits of sequences in s.
Русский
Последовательное замыкание множества s — это множество всех пределов последовательностей, лежащих в s.
LaTeX
$$$\mathrm{seqClosure}(s) = \{ a \in X : \exists x: \mathbb{N} \to X, (\forall n, x(n) \in s) \land Tendsto x\,\mathrm{atTop} \\mathcal{N}(a) \}$$$
Lean4
/-- The sequential closure of a set `s : Set X` in a topological space `X` is the set of all `a : X`
which arise as limit of sequences in `s`. Note that the sequential closure of a set is not
guaranteed to be sequentially closed. -/
def seqClosure (s : Set X) : Set X :=
{a | ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a)}
