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.
FALSE: every regular space is metrizable
Statement
Every regular space is metrizable.
Facts & Assumptions
Given: Under the Axiom of Choice, the lower-limit topology on .
The lower-limit line is regular and has the half-open intervals as basic neighbourhoods (The lower-limit line has a clopen basis, is regular, and is Lindelöf under countable choice, The lower-limit topology on , with the half-open intervals as a basis).
The real line is uncountable ( is uncountable (Cantor's nested intervals, 1874)).
Refutation
Suppose the displayed assertion is true. By [L1], the lower-limit line would be metrizable.
The direct basis argument assigns to each the least member of a putative countable basis contained in and containing ; equality of assigned members forces equality of their left endpoints. Thus no countable basis exists, since it would inject into , contrary to [L2].
The rational-density argument makes the line separable, so metrizability from step 1.1 would imply second countability by Assuming countable choice, a metrizable space is second countable if and only if it is separable if and only if it is Lindelöf, contradicting step 1.2.
Hence the regular lower-limit line refutes the displayed assertion.
Depends on
- The lower-limit topology on $\mathbb{R}$, with the half-open intervals $[a,b)$ as a basis
- The lower-limit line has a clopen basis, is regular, and is Lindelöf under countable choice
- Separability: the existence of an at most countable dense subset
- Second countability: an at most countable basis for the topology
- Assuming countable choice, a metrizable space is second countable if and only if it is separable if and only if it is Lindelöf
- $\mathbb{Q}$ is countably infinite
- The rationals embed densely in the reals
- $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874)
- Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 141 results over 34 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
- L. A. Steen and J. Seebach, Counterexamples in Topology (standard reference, not scraped)