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.
A space with a compatible normal sequence of open covers is metrizable
Statement
If a space has a compatible normal sequence of open covers, then it is metrizable.
Facts & Assumptions
Given: A space and a compatible normal sequence .
A metric topology is generated by its open metric balls (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric).
Proof
Put . Each is symmetric, contains the diagonal, and normality gives : two successive -links lie in the star of one member, which is contained in a member of .
Define as the smaller of and the infimum of over finite chains with , taking the infimum of an empty collection to be . Reversing a chain gives symmetry. Concatenation gives the triangle inequality within a chain-connected component, while points in different components have distance ; truncation at preserves the triangle inequality. The diagonal chains give .
The containment in step 1.1 lets every chain of total weight below be compressed, from its finest links upward, to a -link. Hence implies ; conversely gives .
Compatibility (i) and step 3.1 show when . Compatibility (ii), the two bounds in step 3.1, and [L1] show that the -balls and the original neighbourhoods contain one another at every point. Thus is a metric inducing the given topology.
Depends on
- Compatible normal sequences of open covers
- $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces
- Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 74 results over 13 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
- Umeå University, The Smirnov- and Bing–Nagata–Smirnov Metrization Theorems (standard reference, not scraped)