Alphabeta MathMetrization: Urysohn, Nagata–Smirnov, Bing, Smirnov
About this page
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.
✓ 4 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Real Analysis
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Suprema and Infima
Set Theory
Topology
- Compactness
- Compactness in Metric Spaces
- Countability Axioms and Cardinal Functions
- Discrete bases in metric spaces
- Metric Spaces
- Partitions of Unity and Paracompactness
- Separation Axioms: the Hierarchy
- Subspaces, Products, and Quotients
- Topological Spaces and Continuity
- Urysohn's Lemma and the Tietze Extension Theorem
2 · Logical flowchart
3 · Items
Definition
Discrete families and σ-locally-finite and σ-discrete bases
Lemma
Every discrete family is locally finite, so every σ-discrete basis is σ-locally finite
Definition
A locally metrizable space: every point has a metrizable open neighbourhood
Definition
Compatible normal sequences of open covers
Lemma
A T₁ space with a compatible normal sequence of open covers is metrizable
Lemma
Under choice, every metric space has a σ-locally-finite basis
Theorem
Under choice, a space is metrizable if and only if it is regular, T₁, and has a σ-locally-finite basis
Theorem
Under choice, a space is metrizable if and only if it is regular, T₁, and has a σ-discrete basis
Corollary
Under choice, every regular T₁ second-countable space is metrizable
Lemma
A closure-controlled locally finite open cover transfers relative σ-locally-finite bases to the whole space
Theorem
Under choice, a space is metrizable if and only if it is paracompact, Hausdorff, and locally metrizable
Sources
- Encyclopedia of Mathematics, Metrizable space
- R. Engelking, General Topology, metrization theorems
- Umeå University, The Smirnov- and Bing–Nagata–Smirnov Metrization Theorems
- ProofWiki, Nagata-Smirnov Metrization Theorem, sufficient-condition Hilbert-coordinate outline; details independently checked below
- R. H. Bing, Metrization of Topological Spaces
- UCR, Partitions of Unity and a Metrization Theorem of Smirnov