TheoremStatement: 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.

Moore spaces are subparacompact

Statement

In $Z F C$ every Moore space is subparacompact: every open cover of the space has a refinement that is a countable union of discrete families of closed sets and covers the space (Moore spaces and developments, Discrete families and $σ$ -locally-finite and $σ$ -discrete bases).

The single use of choice is the well-ordering of the given open cover, which is why the statement is formulated in $Z F C$ rather than $Z F$ (The Axiom of Choice).

Facts & Assumptions

Given: A Moore space $X$ , a decreasing development $(G_{n})_{n \in N}$ of $X$ , and an open cover $U$ of $X$ together with a well-ordering $<_{W}$ of the set $U$ itself.

[F1]

A Moore space is regular $T_{1}$ and developable, and a development may be assumed decreasing: every member of $G_{m}$ is contained in a member of $G_{n}$ when $n \leq m$ (Moore spaces and developments).

[F2]

A development's stars form a local base: for $x$ and open $D ∋ x$ there is $n$ with $St (x, G_{n}) \subseteq D$ ; each $St (x, G_{n})$ is open and contains $x$ (Moore spaces and developments, Refinements, locally finite families, point-finite families, and star refinements).

[F3]

A family is discrete when every point has a neighbourhood meeting at most one member (Discrete families and $σ$ -locally-finite and $σ$ -discrete bases), and a countable union of discrete families is what the conclusion asks for.

[L1]

Well-ordering principle: since $W$ well-orders $U$ , every nonempty subfamily of $U$ has a $W$ -least element, and "the $W$ -least $U$ with a property" is a definable description (The Axiom of Choice).

[L2]

Point $z$ lies in $\overline{F}$ exactly when every neighbourhood of $z$ meets $F$ ; consequently 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).

Proof

technique · direct

1.1

Fix $(G_{n})$ , $U$ and $<_{W}$ . For $n \in N$ and $U \in U$ put $F (U, n) : = {x \in X : x \in U, x \notin V for every V <_{W} U, St (x, G_{n}) \subseteq U}$ .

givenF1L1

2.1

Every $F (U, n)$ is contained in $U$ , and $⋃_{U \in U, n} F (U, n) = X$ : given $x$ , let $U$ be the $<_{W}$ -least cover member containing $x$ , which exists by [L1], and choose $n$ with $St (x, G_{n}) \subseteq U$ by [F2]; then $x \in F (U, n)$ .

step 1.1F2L1

2.2

Every $F (U, n)$ is closed. Let $z \in \overline{F (U, n)}$ and let $G \in G_{n}$ contain $z$ . By [L2] and openness of $G$ there is $y \in G \cap F (U, n)$ ; then $G \subseteq St (y, G_{n}) \subseteq U$ . Thus every member of $G_{n}$ containing $z$ lies in $U$ , so $St (z, G_{n}) \subseteq U$ and in particular $z \in U$ . If $V <_{W} U$ , then $V \cap F (U, n) = \emptyset$ by definition, and openness of $V$ with [L2] gives $z \notin V$ . Hence $z \in F (U, n)$ by step 1.1.

step 1.1F2L2

2.3

For fixed $n$ the family ${F (U, n) : U \in U}$ is discrete. Let $x \in X$ , let $V$ be the $<_{W}$ -least cover member containing $x$ , and choose $k \geq n$ with $St (x, G_{k}) \subseteq V$ . Suppose $y \in St (x, G_{k}) \cap F (U, n)$ . Some $G \in G_{k}$ contains $x, y$ ; as $G_{k}$ refines $G_{n}$ , some $H \in G_{n}$ contains $G$ . Hence $x \in St (y, G_{n}) \subseteq U$ , so minimality gives either $V = U$ or $V <_{W} U$ . But $y \in V$ , and the second alternative contradicts the defining exclusion in $F (U, n)$ . Therefore $U = V$ , and the open neighbourhood $St (x, G_{k})$ meets at most the one family member $F (V, n)$ .

step 1.1F1F2F3L1

3.1

The family $⋃_{n} {F (U, n) : U \in U}$ is a countable union of discrete families of closed sets (steps 2.2 and 2.3), covers $X$ (step 2.1), and refines $U$ because $F (U, n) \subseteq U$ . Hence $X$ is subparacompact.

step 2.1step 2.2step 2.3∎

Remarks

Where the choice is spent. The development is a single given sequence and the sets $F (U, n)$ are defined by a formula, but the well-ordering $W$ of the cover is an application of the well-ordering principle and is used in step 2.1 to select the least cover member containing a point. Without it the same construction is not available, which is why the item is stated over $Z F C$ .
Discreteness, not just local finiteness. The argument produces, for each $n$ , one open neighbourhood of each point meeting at most one member, which is discreteness and not merely local finiteness; no local-finiteness closure lemma is needed, because closedness of each $F (U, n)$ is proved directly in step 2.2.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Dennis K. Burke, The Normal Moore Space Problem (standard reference, not scraped)