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.
Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly
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 regular when a point can be separated from a closed set not containing it: for every closed and every there are with
- is when it is regular and ( (Kolmogorov) and (Frechet) spaces).
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), regularity reads: and have disjoint open neighbourhoods. The case is allowed and is satisfied by , , so no nonemptiness is hidden in the condition.
The convention fork, and this library's side of it. Textbooks disagree about whether the word regular carries a hypothesis. Munkres builds it in, defining a regular space to be one in which points are closed and the separation condition above holds; Kelley, Willard and Engelking do not, and reserve for the conjunction. This library takes the second side: regular names the separation condition alone, names regular plus , and every statement that needs points to be closed writes the hypothesis out. The reason is that the two halves are genuinely independent and each is used alone below: the indiscrete topology on a two-point set is regular and not (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies), and the cofinite topology on an infinite set is and not regular, both witnessed on the companion page.
Regularity alone implies no other separation axiom. It does not imply , or Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not): in the indiscrete topology on a set the only closed sets are and , so the only pair to be separated has , and , separates it; yet no two distinct points are distinguished by any open set. Conversely does not imply regularity. It is the conjunction that sits above Hausdorff in the hierarchy, and the proof of that is three items below.
Remarks
-
A regular space is not required to separate two closed sets, which is the stronger condition of normality defined later on this page; and a normal space is not required to separate a point from a closed set, since a point need not be closed. Normality does not imply regularity, and the witness is Sierpinski space on the companion page. Whether regularity implies normality is a question this page leaves open, and no statement here asserts an answer (Normal spaces and spaces, with the source disagreement over whether normality includes stated explicitly).
-
What regularity is really about. The reformulation proved next — every point has a neighbourhood base of closed neighbourhoods — is the form in which regularity is used in practice, and the form in which it is verified for the ordinal spaces later on this page, whose basis consists of clopen sets.
-
The numeral. Because of the fork above, "" in the literature may mean either what is defined here or the bare separation condition. This library always writes the numeral for the conjunction and never uses it to abbreviate the separation condition alone (Conventions on this page, and the one implication of the classical chain that is not available at this point in the reading order).
Depends on
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
(Kolmogorov) and (Frechet) spaces
Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies