LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The sequential closure is contained in the closure, continuity implies sequential continuity, and sequential limits need not be unique

Statement

Let $X$ and $Y$ be topological spaces, with convergence, sequential closure and sequential continuity as in Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure. Then:

$A \subseteq seqcl (A) \subseteq \overline{A}$ for every $A \subseteq X$ .
If $f : X \to Y$ is continuous at $p \in X$ (Continuity of a map of topological spaces at a point and globally) then $f$ is sequentially continuous at $p$ .
Sequential limits need not be unique. In the indiscrete topology on a set $X$ with at least two points (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies), every sequence in $X$ converges to every point of $X$ .

Claim 3 is why this library never writes $\lim_{k} x_{k}$ for a sequence in a general topological space: the symbol would not denote.

Facts & Assumptions

Given: Topological spaces $X$ and $Y$ , a subset $A \subseteq X$ , a point $p \in X$ , a function $f : X \to Y$ , and a sequence $(x_{k})$ in $X$ .

[A1]

$x_{k} \to p$ means that for every neighbourhood $N$ of $p$ there is $K \in N$ with $x_{k} \in N$ for all $k \geq K$ ; $seqcl (A)$ is the set of points to which some sequence with all terms in $A$ converges; $f$ is sequentially continuous at $p$ when $x_{k} \to p$ implies $f (x_{k}) \to f (p)$ (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure).

[A2]

$f$ is continuous at $p$ when $f^{- 1} [V]$ is a neighbourhood of $p$ for every neighbourhood $V$ of $f (p)$ (Continuity of a map of topological spaces at a point and globally).

[L1]

$p \in \overline{A}$ if and only if every neighbourhood of $p$ meets $A$ (A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set, clause (b)).

[L2]

Every point lies in each of its neighbourhoods, since $x \in U \subseteq N$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

[L3]

In the indiscrete topology on $X$ the only open sets are $\emptyset$ and $X$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).

Proof

technique · direct

1.1

$A \subseteq seqcl (A)$ : for $a \in A$ the constant sequence $x_{k} : = a$ has all its terms in $A$ , and it converges to $a$ because every neighbourhood of $a$ contains $a$ , so the condition holds with $K = 0$ .

A1L2

1.2

Let $p \in seqcl (A)$ and fix a sequence $(x_{k})$ with $x_{k} \in A$ for all $k$ and $x_{k} \to p$ ; let $N$ be any neighbourhood of $p$ . Then $x_{k} \in N$ for all $k \geq K$ for some $K$ , and in particular $x_{K} \in N \cap A$ , so $N$ meets $A$ .

A1choose

1.3

Assume $f$ is continuous at $p$ and let $(x_{k})$ be a sequence with $x_{k} \to p$ ; let $V$ be a neighbourhood of $f (p)$ . Then $f^{- 1} [V]$ is a neighbourhood of $p$ , so $x_{k} \in f^{- 1} [V]$ for all $k \geq K$ for some $K$ , that is $f (x_{k}) \in V$ for all $k \geq K$ .

assume-hypA1A2

1.4

In the indiscrete topology, a neighbourhood $N$ of a point $p$ satisfies $p \in U \subseteq N$ for some open $U$ ; since $p \in U$ forces $U \neq \emptyset$ and hence $U = X$ , the only neighbourhood of any point is $X$ itself.

L3L2

2.1

By step 1.2 every neighbourhood of $p$ meets $A$ , so $p \in \overline{A}$ ; as $p$ was an arbitrary point of $seqcl (A)$ this gives $seqcl (A) \subseteq \overline{A}$ , and with step 1.1 it gives claim 1.

step 1.1step 1.2L1

2.2

By step 1.3 the sequence $(f (x_{k}))$ is eventually in every neighbourhood of $f (p)$ , that is $f (x_{k}) \to f (p)$ ; as $(x_{k})$ was an arbitrary sequence converging to $p$ , $f$ is sequentially continuous at $p$ , which is claim 2.

step 1.3A1

2.3

By step 1.4, for every $p \in X$ and every sequence $(x_{k})$ in $X$ the only neighbourhood to be tested is $X$ , and $x_{k} \in X$ for every $k$ ; so $x_{k} \to p$ for every $p \in X$ . With at least two points in $X$ the limit is therefore not unique, which is claim 3.

step 1.4A1

3.1

Claims 1, 2 and 3 are established by step 2.1, step 2.2 and step 2.3 respectively.

step 2.1step 2.2step 2.3∎

Remarks

The second inclusion of claim 1 does not reverse, and the implication of claim 2 does not reverse either. The witnesses are on the companion page and are both in the cocountable topology on $R$ : the sequential closure of $[0, 1]$ is $[0, 1]$ while its closure is all of $R$ (In the cocountable topology on $R$ the sequential closure of $[0, 1]$ is $[0, 1]$ while its closure is all of $R$ ↗), and the identity from the cocountable topology to the usual topology is sequentially continuous and not continuous (The identity from the cocountable topology on $R$ to the usual topology is sequentially continuous and not continuous ↗). This lemma therefore asserts the two inclusions and the one implication and nothing more.
A countability hypothesis repairs both, assuming countable choice. Under the Axiom of Countable Choice, in a first countable space the inclusion of claim 1, $seqcl (A) \subseteq \overline{A}$ , is an equality and the implication of claim 2 reverses; that is the theorem two items below, and it is where the choice hypothesis is spent.
Claim 3 is not an artefact of a strange space. It is the generic situation: uniqueness of sequential limits is equivalent to a separation property of the space, and it holds in every metric space (A sequence in a metric space has at most one limit) because distinct points there are separated by disjoint balls.

Depends on

Used by

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sequential space (Wikipedia) (standard reference, not scraped)
Limit of a sequence (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §21 (standard reference, not scraped)