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.
Normal spaces and spaces, with the source disagreement over whether normality 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 normal when any two disjoint closed sets can be separated by disjoint open sets: for all closed with there are with
- is when it is normal and ( (Kolmogorov) and (Frechet) spaces).
Either of , may be empty, and those cases are met by or together with ; so the condition hides no nonemptiness hypothesis. As with regularity, "disjoint open sets" may equivalently be read as "disjoint open neighbourhoods of the two sets" (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).
Normality is the special case of complete normality at a disjoint closed pair. Disjoint closed sets are separated in the sense of Separated sets: , since the closure of a closed set is itself; so a space in which every separated pair can be put into disjoint open sets is in particular normal. That stronger condition is defined later on this page, and the implication is proved there.
The convention fork, and this library's side of it. Exactly as for regularity, textbooks disagree about whether normal carries a hypothesis. Munkres builds it in; Kelley, Willard and Engelking do not. This library takes the second side: normal names the separation condition alone, names normal plus , and the hypothesis is written out wherever it is used. The reason is again that the two halves are independent, and here the point is sharp: normality without implies nothing at all in the hierarchy. The indiscrete topology on a two-point set (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies) is normal, its only closed sets being and the whole space, and it is not even ; Sierpinski space is normal, and not regular. Both are recorded on this page, the first as a false statement and both on the companion page.
Remarks
-
Normality does not imply regularity, and the failure is witnessed by Sierpinski space on the companion page, which is normal and not regular. Whether regularity implies normality is a question this page leaves open: any witness reachable from the material here would need cardinal arithmetic or the hereditary behaviour of regularity. This page's own prerequisites still supply neither: cardinal arithmetic and cofinality is now built, but below this one, and nothing here draws on it; the hereditary and productive behaviour of the separation axioms is developed later in the reading order. So nothing above asserts an answer and no false statement asserting one is planted here (Conventions on this page, and the one implication of the classical chain that is not available at this point in the reading order).
-
Normality is the axiom that behaves worst, and the companion page shows one symptom: the deleted Tychonoff plank, a subspace of a product of two ordinal spaces each of which is , is Hausdorff and not normal. Whether normality is inherited by subspaces or preserved by products is a question this page does not answer, and nothing here asserts an answer; the plank is presented only as a Hausdorff space that fails normality.
-
What the definition does not say. It says nothing about separating a point from a closed set, because a point need not be closed; that is the content of the hypothesis in , and the theorem two items below is where it is spent.
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
Separated sets:
The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open