Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-31
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 T4T_4 spaces, with the source disagreement over whether normality includes T1T_1 stated explicitly

Definition

Let (X,T)(X, \mathcal{T}) be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

  • XX is normal when any two disjoint closed sets can be separated by disjoint open sets: for all closed A,BXA, B \subseteq X with AB=A \cap B = \varnothing there are U,VTU, V \in \mathcal{T} with AU,BV,UV=.A \subseteq U, \qquad B \subseteq V, \qquad U \cap V = \varnothing .
  • XX is T4T_4 when it is normal and T1T_1 (T0T_0 (Kolmogorov) and T1T_1 (Frechet) spaces).

Either of AA, BB may be empty, and those cases are met by U=U = \varnothing or V=V = \varnothing together with XX; 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: AB=AB=\overline{A} \cap B = A \cap \overline{B} = \varnothing, 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 T1T_1 hypothesis. Munkres builds it in; Kelley, Willard and Engelking do not. This library takes the second side: normal names the separation condition alone, T4T_4 names normal plus T1T_1, and the T1T_1 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 T1T_1 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 \varnothing and the whole space, and it is not even T0T_0; Sierpinski space is normal, T0T_0 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 T3T_3, 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 T1T_1 hypothesis in T4T_4, and the theorem two items below is where it is spent.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 45 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources