LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31‡ 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 3 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 ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. 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.

Jones's bound: under choice, a closed discrete subspace of a normal space cannot have more subsets than a dense set has subsets

Statement

Assume the Axiom of Choice. If $D$ is a closed discrete subspace of a normal space $X$ and $E\subseteq X$ is dense, then there is an injection $\mathcal P(D)\to\mathcal P(E)$ . In cardinal notation, $2^{|D|}\le 2^{|E|}$ .

Facts & Assumptions

Given: A normal space $X$ , a closed discrete $D\subseteq X$ , and a dense $E\subseteq X$ .

[A1]

The Axiom of Choice supplies a choice function for every family of nonempty sets (The Axiom of Choice).

[F1]

Every subset of a discrete subspace is closed in that subspace; because $D$ is closed in $X$ , each subset of $D$ is closed in $X$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F2]

Normality separates disjoint closed sets by disjoint open sets, and every nonempty open set meets a dense subset (Normal spaces and $T_4$ spaces, with the source disagreement over whether normality includes $T_1$ stated explicitly, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets).

[F3]

Under choice, $2^{\kappa}=|\mathcal P(\kappa)|$ for every cardinal $\kappa$ (Cardinal sum $\kappa \oplus \lambda$ , product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$ , and why they are written apart from the ordinal operations, Assuming the Axiom of Choice, $2^{\kappa} = \lvert \mathcal{P}(\kappa) \rvert$ , and Cantor's theorem in cardinal form: $\kappa < 2^{\kappa}$ ).

Proof

technique · direct

1.1

For every $A\subseteq D$ , the sets $A$ and $D\setminus A$ are disjoint closed subsets of $X$ . By normality there is an open $U_A$ containing $A$ and an open $V_A$ containing $D\setminus A$ with $U_A\cap V_A=\varnothing$ .

F1F2

2.1

Apply [A1] to choose one such pair $(U_A,V_A)$ for every $A\subseteq D$ , and define $\Phi(A)=U_A\cap E\subseteq E$ .

A1step 1.1

3.1

If $A\ne B$ , take $d\in A\setminus B$ after interchanging them if necessary. Then $d\in U_A\cap V_B$ , a nonempty open set meeting $E$ ; a point of $E\cap U_A\cap V_B$ lies in $\Phi(A)$ and not in $\Phi(B)$ .

F2step 2.1

4.1

Thus $\Phi$ is injective. By [F3], this is the asserted cardinal inequality.

F3step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 76 results over 22 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

G. Gruenhage, General Topology Course Notes, Jones's lemma (standard reference, not scraped)
Samuel Gomes da Silva, Closed discrete subsets of separable spaces and relative versions of normality, countable paracompactness and property (a) (standard reference, not scraped)