Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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 cocountable topology on R is T1, has unique sequential limits, and is neither Hausdorff nor regular nor normal

Example

Give R the cocountable topology Tcoc={∅}∪{ U⊆R:R∖U is at most countable } (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies), whose closed sets are R together with the at most countable subsets of R (Finite, countably infinite, countable, uncountable). Then:

  1. (R,Tcoc) is T1 (T0 (Kolmogorov) and T1 (Frechet) spaces).
  2. Every convergent sequence is eventually constant, so every sequence has at most one limit (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure).
  3. No two nonempty open sets are disjoint. Consequently the space is not Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not), not regular (Regular spaces and T3 spaces, with the source disagreement over whether regularity includes T1 stated explicitly) and not normal (Normal spaces and T4 spaces, with the source disagreement over whether normality includes T1 stated explicitly).

Clauses 1, 2 and the Hausdorff half of clause 3 are what refute the claim that unique sequential limits force the Hausdorff condition (FALSE: a space in which every sequence has at most one limit is Hausdorff); clause 3's other two halves place the space in the hierarchy exactly where the cofinite topology sits, at T1 and no higher.

Facts & Assumptions

Given: R with the cocountable topology Tcoc, a sequence (xk)k∈N in R, and points p,q,u,v,w∈R.

[A2]

xk→p means: for every neighbourhood N of p there is K∈N with xk∈N for all k≥K; an open set containing p is such a neighbourhood (Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure).

[L2]

The range of a sequence is nonempty and at most countable, and a subset of an at most countable set is at most countable (A nonempty set is at most countable iff it is a surjective image of N, Every subset of an at most countable set is at most countable).

[L3]

A union of two at most countable sets is at most countable: this is the two-set instance of Countable unions of at most countable sets, assuming ACω padded with copies of ∅, and it needs no choice principle, as The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies records.

[L4]

R is uncountable (R is uncountable (Cantor's nested intervals, 1874)), so in particular it has at least three distinct points.

Verification

technique · direct
1.1

The cofinite topology on R is contained in Tcoc, a finite complement being at most countable, so the space is T1, which is claim 1.

A1L1
1.2

Fix three distinct points u,v,w of R, for instance 0, 1 and 2.

L4
1.3

Suppose xk→p and put R:={ xk:k∈N }∖{p}, at most countable by [L2]; then R∖R is open by [A1] and contains p, so [A2] gives K with xk∉R for all k≥K.

A1A2L2assume-hyp
1.4

Let U,V be nonempty open sets and suppose U∩V=∅; then R=(R∖U)∪(R∖V) is at most countable by [A1] and [L3], contradicting [L4]. So no two nonempty open sets are disjoint.

A1L3L4assume-hyp
2.1

Under step 1.3: for k≥K the point xk lies in the range of the sequence and outside R, hence equals p; so the sequence is eventually constant with value p.

step 1.3
2.2

Any open U∋u and open V∋v are nonempty, hence meet by step 1.4, so the space is not Hausdorff.

step 1.2step 1.4L5
2.3

{v} is at most countable, hence closed by [A1], and u∉{v}; any open U∋u and open V⊇{v} are nonempty, hence meet by step 1.4, so the space is not regular.

step 1.2step 1.4A1L5
2.4

{v} and {w} are disjoint nonempty closed sets by [A1] and step 1.2; any open sets containing them are nonempty, hence meet by step 1.4, so the space is not normal.

step 1.2step 1.4A1L5
3.1

Under step 1.3: if also xk→q with q≠p, then R∖{p} is open by [A1] and contains q, so [A2] gives K′ with xk≠p for all k≥K′, contradicting step 2.1 at any index at least both K and K′. So a sequence has at most one limit, which with step 2.1 is claim 2.

step 2.1A1A2
4.1

Steps 2.2, 2.3 and 2.4 complete claim 3, step 3.1 is claim 2 and step 1.1 is claim 1.

step 1.1step 3.1step 2.2step 2.3step 2.4∎

Remarks

  • Sequences cannot see this topology. A sequence reaches at most countably many points, and every at most countable set is closed, so the complement of the values other than the limit is an open set that forces the sequence to be eventually constant. Uniqueness of limits is therefore free, and it carries no separation information at all — which is the point of FALSE: a space in which every sequence has at most one limit is Hausdorff.

  • The failure of T2, T3 and T4 has the same one-line cause as in the cofinite case: two at most countable sets cannot cover an uncountable one, so two nonempty open sets always meet. What changes between the two examples is only how large a set has to be for the topology to be interesting: infinite for cofinite, uncountable for cocountable.

  • On an at most countable set the cocountable topology is discrete (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies), so the uncountability of R is doing real work here and not merely supplying a familiar underlying set.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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