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.
(Kolmogorov) and (Frechet) spaces
Definition
Let be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).
- is , or a Kolmogorov space, when any two distinct points are topologically distinguishable: for all with there is an open set containing exactly one of and .
- is , or a Frechet space, when each of any two distinct points has an open set containing it and missing the other: for all with there are with
Nothing is asserted about a pair of equal points, so a space with at most one point satisfies both conditions vacuously.
Since an open set containing a point is an open neighbourhood of it (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open), both conditions may be read with "open neighbourhood" in place of "open set"; and by the same equivalence recorded in Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open they may be read with arbitrary neighbourhoods, since a neighbourhood of contains an open one and an open neighbourhood is a neighbourhood.
Every space is , and this is discharged here rather than left to the reader, because it is the bottom arrow of the whole hierarchy on this page. Let and take as in the condition. Then is an open set containing and not , so it contains exactly one of the two points, which is the condition. Only the first half of the condition is used, so the implication does not reverse formally, and it does not reverse in fact: Sierpinski space is a witness, recorded on the companion page.
The two conditions differ exactly in symmetry. asks for one open set that tells the pair apart, with no control over which of the two it contains; asks for both separations at once. In Sierpinski space of The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies the open set contains and not , so the space is ; but the only open set containing is the whole space, which also contains , so it is not .
Neither condition is a property of a set alone. Both are properties of the pair , and both are inherited upwards along the comparison order of Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison: if and is , respectively , then so is , since the separating open sets of the coarser topology lie in the finer one. In particular the discrete topology satisfies both, and the indiscrete topology on a set with at least two points satisfies neither.
Remarks
-
The names. The numbering is Alexandroff and Hopf's Trennungsaxiome; the individual names honour Kolmogorov and Frechet. This page fixes each axiom by its condition and treats the numeral as an abbreviation, because the numerals above are used inconsistently in the literature (Conventions on this page, and the one implication of the classical chain that is not available at this point in the reading order).
-
What says about closures. is equivalent to the closedness of every singleton, and hence to for every point (Interior, closure, boundary, exterior, derived set and isolated point in a topological space); that equivalence is the next item and is a theorem, not a restatement. The corresponding characterisation of , that distinct points have distinct closures, is not needed on this page and is not proved here.
-
No separation is built into the word space. Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison assumes none; every separation property on this page is a hypothesis written out where it is used.
Depends on
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Interior, closure, boundary, exterior, derived set and isolated point in a topological space
The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies