CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 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.

In the cocountable topology on $R$ the sequential closure of $[0, 1]$ is $[0, 1]$ while its closure is all of $R$

Statement refuted

Refuted: that the sequential closure of a subset of a topological space equals its closure. The sequential closure is contained in the closure, continuity implies sequential continuity, and sequential limits need not be unique asserts only the inclusion $seqcl (A) \subseteq \overline{A}$ , and asserts it without any hypothesis; the witness below shows that the inclusion can be as far from an equality as it is possible to be, the two sides differing by all but a bounded interval.

Witness. Give $R$ the cocountable topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, In the cocountable topology on $R$ the closed sets are the countable sets and $R$ , and a sequence converges iff it is eventually constant) and take $A : = [0, 1]$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). Then $seqcl (A) = [0, 1] ⊊ R = \overline{A} .$

Facts & Assumptions

Given: $R$ with the cocountable topology, and the set $A = [0, 1] = {t \in R : 0 \leq t \leq 1}$ .

[A1]

$seqcl (A)$ is the set of points to which some sequence with all terms in $A$ converges (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure).

[L1]

In the cocountable topology on $R$ a sequence converges if and only if it is eventually constant, and it then converges to its eventual value and to no other point (In the cocountable topology on $R$ the closed sets are the countable sets and $R$ , and a sequence converges iff it is eventually constant, claim 3).

[L2]

In the cocountable topology on $R$ the closure of an uncountable set is $R$ (In the cocountable topology on $R$ the closed sets are the countable sets and $R$ , and a sequence converges iff it is eventually constant, claim 2).

[L3]

For $a < b$ the interval $[a, b]$ is uncountable (Every nondegenerate interval of $R$ is uncountable, Finite, countably infinite, countable, uncountable); $0 < 1$ (The multiplicative identity is positive).

[L4]

$seqcl (A) \subseteq \overline{A}$ in every topological space (The sequential closure is contained in the closure, continuity implies sequential continuity, and sequential limits need not be unique, claim 1), and $\overline{A}$ is the smallest closed superset of $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, claim 2).

Counterexample

technique · direct

1.1

$0 < 1$ by [L3], so $[0, 1]$ is a nondegenerate closed interval and is uncountable by [L3].

1.2

Let $(x_{k})$ be a sequence with $x_{k} \in [0, 1]$ for every $k$ and suppose $x_{k} \to p$ in the cocountable topology. By [L1] the sequence is eventually constant with value $p$ , so $p = x_{K}$ for some index $K$ , and $x_{K} \in [0, 1]$ ; hence $p \in [0, 1]$ .

A1L1

1.3

Conversely every $a \in [0, 1]$ lies in $seqcl ([0, 1])$ , the constant sequence with value $a$ having all its terms in $[0, 1]$ and converging to $a$ by [L1].

A1L1

2.1

By steps 1.2 and 1.3, $seqcl ([0, 1]) = [0, 1]$ .

step 1.2step 1.3

2.2

By step 1.1 the set $[0, 1]$ is uncountable, so $\overline{[0, 1]} = R$ by [L2].

step 1.1L2

3.1

The inclusion $[0, 1] \subseteq R$ is strict, since $2 \notin [0, 1]$ ; so by steps 2.1 and 2.2 the sequential closure of $[0, 1]$ is strictly smaller than its closure, and the inclusion of [L4] cannot in general be improved to an equality.

step 2.1step 2.2L4∎

Remarks

The set $[0, 1]$ plays no special role beyond being uncountable and not all of $R$ . Any uncountable proper subset would do, and by claim 3 of In the cocountable topology on $R$ the closed sets are the countable sets and $R$ , and a sequence converges iff it is eventually constant the sequential closure of any subset of this space is the subset itself, so the sequential closure operator here is the identity while the closure operator is far from it.
What the witness rules out. It shows that no theorem of the form " $seqcl = \overline{\cdot}$ in every space" is available, so the countability hypothesis of Assuming Countable Choice, in a first countable space sequential closure equals closure and sequential continuity at a point equals continuity there is doing real work. Assuming the Axiom of Countable Choice, as that theorem does, it also shows that the cocountable topology on $R$ is not first countable.
Sequences are the wrong index set here, not the wrong idea. Replacing sequences by nets or filters restores the equality in every space; neither is developed in this library at this point, and the failure above is exactly the reason they exist.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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)
Cocountable topology (Wikipedia) (standard reference, not scraped)

In the cocountable topology on RR the sequential closure of [0,1][0,1] is [0,1][0,1] while its closure is all of RR