English
Let X be a topological space and S a subset of X. Then S is sequentially closed if every sequence (x_n) in S that converges in X has its limit p in S.
Русский
Пусть X — топологическое пространство и S — подмножество X. Тогда S последовательносно замкнуто, если для любой последовательности (x_n) из S, сходящейся к точке p в X, предел p принадлежит S.
LaTeX
$$$\\text{IsSeqClosed}(S) \\iff \\forall x: \\mathbb{N} \\to X, \\forall p \\in X, (\\forall n, x(n) \\in S) \\to \\text{Tendsto}\\, x\\,\\text{atTop}\\, (\\mathcal{N} p) \\to p \\in S$$$
Lean4
/-- A set `s` is sequentially closed if for any converging sequence `x n` of elements of `s`, the
limit belongs to `s` as well. Note that the sequential closure of a set is not guaranteed to be
sequentially closed. -/
def IsSeqClosed (s : Set X) : Prop :=
∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ n, x n ∈ s) → Tendsto x atTop (𝓝 p) → p ∈ s
