TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22‡ rests on unproved material (inherited)

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.

‡ Rests on 2 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Under choice, every metric space has a σ-discrete basis and ‡ Under choice, a regular T₁ space with a σ-locally-finite basis has a compatible normal sequence. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Normal screenable Moore spaces are metrizable

Statement

In $Z F C$ every normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) screenable Moore space is metrizable. Here a space is screenable when every open cover has a refinement that is a countable union of pairwise disjoint families of open sets and covers the space (Refinements, locally finite families, point-finite families, and star refinements).

Facts & Assumptions

Given: A normal Moore space $X$ with a decreasing development $(G_{n})_{n \in N}$ (Moore spaces and developments), and for every open cover $U$ of $X$ a refinement $⋃_{i \in N} H_{i}$ of $U$ by pairwise disjoint families of open sets covering $X$ .

[F1]

A Moore space is regular $T_{1}$ and developable, and a development may be taken decreasing (Moore spaces and developments). Together with the normality in the Given clause, this supplies the normal-Moore-space hypothesis of A sigma-cellular base metrizes a normal Moore space.

[F2]

A base of a space is a family of open sets such that every open set is a union of members; equivalently every point of an open set has a base member between it and the set (Basis and subbasis for a topology, and the topology generated by a family of sets).

[F3]

Screenability applied to an open cover yields a covering refinement that is a countable union of pairwise disjoint open families; a refinement of a cover is a family each of whose members lies in a member of the cover (Refinements, locally finite families, point-finite families, and star refinements, the definition of screenable in the Statement).

[L1]

Countably many choices are available: selecting one screening of $G_{n}$ for each $n \in N$ uses countable choice, which is a theorem of $Z F C$ (The Axiom of Choice).

Proof

technique · direct

1.1

Fix $(G_{n})$ and, for each $n$ , a screening of the open cover $G_{n}$ , say $⋃_{i \in N} H_{n, i}$ , where each $H_{n, i}$ is a pairwise disjoint family of open sets and $⋃_{i} H_{n, i}$ covers $X$ and refines $G_{n}$ .

givenF3L1

2.1

The family $⋃_{(n, i) \in N \times N} H_{n, i}$ is a base for $X$ : let $D$ be open and $x \in D$ . Choose $n$ with $St (x, G_{n}) \subseteq D$ and then $i$ and $H \in H_{n, i}$ with $x \in H$ . Since $H_{n, i}$ refines $G_{n}$ there is $G \in G_{n}$ with $H \subseteq G$ , so $x \in G$ and therefore $G \subseteq St (x, G_{n}) \subseteq D$ ; hence $x \in H \subseteq D$ and $H$ is a member of the displayed family.

step 1.1F1F2F3

3.1

Each $H_{n, i}$ is a pairwise disjoint family of open sets, and the index set $N \times N$ is countable, so the base of step 2.1 is $σ$ -cellular in the sense of A sigma-cellular base metrizes a normal Moore space.

step 2.1

4.1

The Given clause and [F1] say that $X$ is a normal Moore space, and step 3.1 supplies its $σ$ -cellular base. Therefore A sigma-cellular base metrizes a normal Moore space supplies a metric whose metric topology is the topology of $X$ , so $X$ is metrizable.

givenstep 3.1F1∎

Remarks

Relation to Bing's route. Bing proves this theorem by showing that a normal screenable developable space is strongly screenable (Theorem 8), that strongly screenable developable spaces are perfectly screenable (Theorem 6), and that perfectly screenable regular spaces are metrizable (Theorems 3 and 7). Steps 1.1-2.2 above are the first two of those reductions in the equivalent language of a $σ$ -cellular base, and step 3.1 replaces Bing's displayed weighted metric by the explicit level metric of A sigma-cellular base metrizes a normal Moore space; the conclusion is the same.
Where normality enters. Screenability produces the $σ$ -cellular base in steps 1.1-3.1. Normality is then an essential hypothesis of A sigma-cellular base metrizes a normal Moore space, whose proof uses normal shrinking to turn the cellular levels into a $σ$ -discrete base. Thus normality is used at step 4.1 rather than in the screening construction itself.
Choice. The only choice is the countable selection of one screening per development level in step 1.1; the metric is then defined by a formula.

Depends on

Used by

Collectionwise normal Moore spaces are metrizable Theorem

Dependency tree · two levels

39 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. H. Bing, Metrization of topological spaces (standard reference, not scraped)