ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)

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.

A finite Hausdorff space is discrete, and its diagonal is closed for the trivial reason that every subset of the square is

Example

Let $(X, T)$ be a Hausdorff space (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) whose underlying set is finite (Finite, countably infinite, countable, uncountable). Then:

$T$ is the discrete topology on $X$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies): every subset of $X$ is open.
$X \times X$ with the product topology (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space) is discrete as well, so every subset of it — the diagonal $Δ_{X}$ included — is both open and closed.

Clause 2 makes the diagonal criterion (A space is Hausdorff if and only if its diagonal is closed in the square carrying the product topology) true here for a reason that has nothing to do with the diagonal: in a discrete square every subset is closed. The example is worth recording precisely because it is the degenerate case, where the criterion carries no information.

Facts & Assumptions

Given: A Hausdorff space $(X, T)$ with $X$ finite, and $X \times X$ with the product topology.

[A1]

$X$ is finite, so every subset of $X$ is finite (Finite, countably infinite, countable, uncountable, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, fact (i)).

[A2]

The discrete topology on a set is the family of all its subsets; in it every subset is open, hence every subset is closed (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[A3]

The boxes $U \times W$ with $U, W \in T$ form a basis for the product topology on $X \times X$ , the index set being $2$ (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Basis and subbasis for a topology, and the topology generated by a family of sets, The diagonal $Δ_{X} \subseteq X \times X$ , the diagonal map $δ_{X}$ , and the pairing $⟨ f, g ⟩$ of two maps).

[L1]

Every Hausdorff space is $T_{1}$ (Every Urysohn space is Hausdorff, every Hausdorff space is $T_{1}$ and hence $T_{0}$ , and every regular $T_{1}$ space is Urysohn, claim 2, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[L2]

A space is $T_{1}$ exactly when every finite subset of it is closed (A space is $T_{1}$ if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology, clause (c)).

Verification

technique · direct

1.1

$X$ is $T_{1}$ , being Hausdorff.

2.1

Every subset $A \subseteq X$ is finite by [A1], hence closed by step 1.1 and [L2]; so every subset of $X$ is closed.

step 1.1A1L2

3.1

Every subset $A \subseteq X$ is open, its complement $X ∖ A$ being a subset of $X$ and therefore closed by step 2.1; so $T$ is the discrete topology, which is claim 1.

step 2.1A2

4.1

Every singleton ${(u, v)} = {u} \times {v}$ of $X \times X$ is a basic open box by step 3.1 and [A3], so every subset of $X \times X$ , being the union of the singletons of its elements, is open; hence $X \times X$ is discrete and every subset of it, $Δ_{X}$ included, is closed. This is claim 2.

step 3.1A2A3∎

Remarks

The finiteness is used only through "every subset is finite". Nothing about cardinality beyond that enters, and the argument gives, for an arbitrary $T_{1}$ space, that every finite subset is closed — which is the content of clause (c) of A space is $T_{1}$ if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology and is the real reason a finite $T_{1}$ space is discrete.
The Hausdorff hypothesis may be weakened to $T_{1}$ . Step 1.1 is the only place it is used, and it is used only to obtain $T_{1}$ ; so a finite $T_{1}$ space is already discrete, and a finite Hausdorff space is discrete because Hausdorff implies $T_{1}$ . Neither hypothesis can be dropped altogether: the indiscrete topology on a two-point set is finite and not discrete (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).
Why the diagonal is uninformative here. In a discrete square every subset is closed, so the closedness of $Δ_{X}$ is not evidence of anything about $X$ ; the criterion is a genuine test only where the square has proper nonempty non-closed subsets to be distinguished from.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

Discrete space (Wikipedia) (standard reference, not scraped)
Hausdorff space (Wikipedia) (standard reference, not scraped)
Topological Spaces lecture notes (University of Cambridge) (standard reference, not scraped)