LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-22

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.

Collectionwise normal Moore spaces are screenable

Statement

In $Z F C$ every collectionwise normal Moore space is screenable: every open cover of the space has a refinement that is a countable union of pairwise disjoint families of open sets and covers the space (Moore spaces and developments, Normalized families and collectionwise normality, The Axiom of Choice).

Facts & Assumptions

Given: A collectionwise normal Moore space $X$ with a decreasing development $(G_{n})_{n \in N}$ (Moore spaces and developments) and an open cover $H = {H_{α} : α \in A}$ well-ordered by $W$ .

[F1]

Each $St (x, G_{n})$ is open and contains $x$ , and for open $D ∋ x$ there is $n$ with $St (x, G_{n}) \subseteq D$ ; members of $G_{m}$ are contained in members of $G_{n}$ when $n \leq m$ (Moore spaces and developments, Refinements, locally finite families, point-finite families, and star refinements).

[F2]

Collectionwise normality: every discrete family of closed sets has a pairwise disjoint open expansion (Normalized families and collectionwise normality, Discrete families and $σ$ -locally-finite and $σ$ -discrete bases).

[L1]

$z \in \overline{F}$ exactly when every neighbourhood of $z$ meets $F$ ; hence an open set disjoint from $F$ is disjoint from $\overline{F}$ (A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set).

[L2]

The well-ordering $W$ provides least elements, so "the $W$ -least $H$ with a property" is a definable description (The Axiom of Choice).

Proof

technique · direct

1.1

Fix $(G_{n})$ , $H$ and $W$ . For $n \in N$ and $α \in A$ put $X (α, n) : = {x \in X : x \in H_{α}, x \notin H_{β} for all β < α, every G \in G_{n} with x \in G satisfies G \subseteq H_{α}}$ .

givenF1L2

2.1

$⋃_{α, n} X (α, n) = X$ , and $X (α, n) \subseteq H_{α}$ for all $α, n$ : given $x$ , let $α$ be the $W$ -least index with $x \in H_{α}$ and choose $n$ with $St (x, G_{n}) \subseteq H_{α}$ ; every $G \in G_{n}$ containing $x$ is then contained in $H_{α}$ , so $x \in X (α, n)$ .

step 1.1F1L2

2.2

Each $X (α, n)$ is closed. Let $z \in \overline{X (α, n)}$ and $G \in G_{n}$ with $z \in G$ . By [L1] there is $y \in G \cap X (α, n)$ ; then $z, y \in G \in G_{n}$ , and since every member of $G_{n}$ containing $y$ lies in $H_{α}$ , we get $G \subseteq H_{α}$ ; hence every member of $G_{n}$ containing $z$ lies in $H_{α}$ . Also $z \in St (z, G_{n}) \subseteq H_{α}$ , and $z \notin H_{β}$ for $β < α$ because $H_{β} \cap X (α, n) = \emptyset$ with $H_{β}$ open and [L1]. So $z \in X (α, n)$ .

step 1.1F1L1

2.3

For each fixed $n$ the family ${X (α, n) : α \in A}$ is discrete. Let $x \in X$ , let $β$ be $W$ -least with $x \in H_{β}$ and choose $k \geq n$ with $St (x, G_{k}) \subseteq H_{β}$ . If $y \in St (x, G_{k}) \cap X (α, n)$ , pick $G \in G_{k}$ with $x, y \in G$ ; since $G$ lies in some $H \in G_{n}$ , we have $x \in St (y, G_{n}) \subseteq H_{α}$ , so $β \leq α$ . Also $y \in St (x, G_{k}) \subseteq H_{β}$ , so if $β < α$ then $y \in H_{β}$ contradicts $y \in X (α, n)$ ; hence $α = β$ and the open neighbourhood $St (x, G_{k})$ of $x$ meets at most one member.

step 1.1F1

3.1

For each $n$ , apply [F2] to the discrete family ${X (α, n) : α \in A}$ of closed sets, obtaining pairwise disjoint open sets $W (α, n) \supseteq X (α, n)$ , and put $Y (α, n) : = W (α, n) \cap H_{α}$ . Then each $Y (α, n)$ is open, contains $X (α, n)$ , lies in $H_{α}$ , and the family ${Y (α, n) : α \in A}$ is pairwise disjoint.

step 2.2step 2.3F2

4.1

Since $⋃_{α, n} X (α, n) = X$ by step 2.1, the family $⋃_{n} {Y (α, n) : α \in A}$ covers $X$ , refines $H$ by step 3.1, and is a countable union of pairwise disjoint families of open sets. Hence the arbitrary open cover $H$ has such a refinement and $X$ is screenable.

step 2.1step 2.2∎

Remarks

Bing's Theorem 9 is steps 1.1-4.1. The sets $X (α, n)$ are Bing's $x (h, i)$ , each $X_{i}$ is his discrete family of closed sets, and the well-order of the cover is exactly where choice enters; the proof of closedness follows his displayed argument, with the closure criterion used at the two places where an open set disjoint from a member must remain disjoint from its closure.
Collectionwise normality is used once, in step 3.1, and it is applied to a family of closed sets; the expansion is then intersected with the corresponding cover member so that the refinement property survives. A merely normal space would not suffice at this step.

Depends on

Used by

Collectionwise normal Moore spaces are metrizable Theorem

Dependency tree · two levels

19 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)