LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Metrizable spaces are collectionwise normal

Statement

In $Z F$ , every metrizable space (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not) is collectionwise normal (Normalized families and collectionwise normality).

Facts & Assumptions

Given: A metrizable space $(X, T)$ together with one metric $d$ with $T = T_{d}$ (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement), and a discrete family $F = {F_{i} : i \in I}$ of closed subsets of $X$ (Discrete families and $σ$ -locally-finite and $σ$ -discrete bases).

[F1]

A discrete family is locally finite, and a locally finite union of closed sets is closed; hence every subunion $⋃_{i \in J} F_{i}$ is closed (Every discrete family is locally finite, so every $σ$ -discrete basis is $σ$ -locally finite, Locally finite families remain locally finite after taking closures, closure commutes with their union, and a locally finite union of closed sets is closed).

[F2]

Collectionwise normality asks that a discrete family of closed sets be separated, that is, have a pairwise disjoint open expansion (Normalized families and collectionwise normality).

[L1]

For nonempty $A \subseteq X$ and $u \in X$ the distance $d (u, A) = \inf {d (u, a) : a \in A}$ exists, is $\geq 0$ , and equals $0$ when $u \in A$ ; the map $u \mapsto d (u, A)$ differs by at most $d (u, v)$ at two points $u, v$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz).

[L2]

If $A \subseteq B$ are nonempty then $d (u, B) \leq d (u, A)$ , because every lower bound of the set of distances to $B$ is one for $A$ and the infimum is the greatest lower bound (Greatest lower bound (infimum)). If $A$ is closed and $u \notin A$ then $d (u, A) > 0$ : $d (u, A) = 0$ would let balls of every radius about $u$ meet $A$ , so $u$ would lie in the closure of $A$ and hence in $A$ (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · direct

1.1givenF1

Fix $d$ and $F$ as in the Given. For each $i \in I$ put $G_{i} : = ⋃_{j \neq i} F_{j}$ , a possibly empty closed set by [F1].

2.1step 1.1L1

For each $i$ , define $U_{i}$ by cases: $U_{i} : = \emptyset$ if $F_{i} = \emptyset$ ; $U_{i} : = X$ if $F_{i} \neq \emptyset$ and $G_{i} = \emptyset$ ; and $U_{i} : = {x \in X : d (x, F_{i}) < \frac{1}{3} d (x, G_{i})}$ if both $F_{i}$ and $G_{i}$ are nonempty. This definition is a formula in $F_{i}$ and $G_{i}$ , so the assignment $i \mapsto U_{i}$ is a single definable function and no selection is used.

3.1step 2.1L1

Each $U_{i}$ is open. The first two cases are clear. In the third, let $x \in U_{i}$ and put $c : = d (x, F_{i}) \geq 0$ and $h : = d (x, G_{i}) > 0$ , so $3 c < h$ by definition of $U_{i}$ ; set $r : = (h - 3 c) / 8 > 0$ . For $y$ with $d (x, y) < r$ we get $d (y, F_{i}) \leq c + r$ and $d (y, G_{i}) \geq h - r$ , and $3 c + 3 r = 3 c + \frac{3}{8} (h - 3 c) < \frac{1}{2} (h + 3 c) < h - r$ , where the last inequality is $3 c < h$ ; hence $3 d (y, F_{i}) < d (y, G_{i})$ and $y \in U_{i}$ . So every point of $U_{i}$ has a ball around it inside $U_{i}$ , and $U_{i}$ is open in the metric topology (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

3.2step 2.1L1L2

Each $F_{i} \subseteq U_{i}$ . If $F_{i} = \emptyset$ this is clear; if $G_{i} = \emptyset$ then $U_{i} = X$ ; otherwise $y \in F_{i}$ gives $d (y, F_{i}) = 0$ and $d (y, G_{i}) > 0$ because $G_{i}$ is closed and $y \notin G_{i}$ , so $0 < \frac{1}{3} d (y, G_{i})$ and $y \in U_{i}$ .

3.3step 2.1L1L2

The sets $U_{i}$ are pairwise disjoint. Let $x \in U_{i} \cap U_{k}$ with $i \neq k$ . If either of the first two cases produced $U_{i}$ or $U_{k}$ , then one of them is empty and the other is $X$ only when every $F_{j}$ with $j \neq i$ is empty, in which case $U_{k} = \emptyset$ for $k \neq i$ ; so both sets are given by the third case. Then $F_{k} \subseteq G_{i}$ and $F_{i} \subseteq G_{k}$ give by [L2] that $d (x, F_{i}) < \frac{1}{3} d (x, G_{i}) \leq \frac{1}{3} d (x, F_{k})$ and $d (x, F_{k}) < \frac{1}{3} d (x, G_{k}) \leq \frac{1}{3} d (x, F_{i})$ , hence $d (x, F_{i}) < \frac{1}{9} d (x, F_{i})$ , so that $d (x, F_{i}) = 0$ and then $d (x, F_{k}) < 0$ , contradicting $d (x, F_{k}) \geq 0$ .

4.1step 3.1step 3.2step 3.3F2∎

By steps 3.1, 3.2 and 3.3 the family $(U_{i})_{i \in I}$ is a pairwise disjoint open expansion of $F$ , so $F$ is separated and $X$ is collectionwise normal by [F2].

Remarks

The empty cases are real cases. If $F_{i} = \emptyset$ then $G_{i}$ may be everything, and the formula $\frac{1}{3} d (x, G_{i})$ with $G_{i} = X$ would give $d (x, X) = 0$ and force $U_{i} = \emptyset$ ; the first case records that directly. If all other $F_{j}$ are empty, $G_{i} = \emptyset$ and the distance $d (x, G_{i})$ is undefined, which is why the second case is separated out. Both are decided by the given data, so no choice enters.
No choice anywhere. One metric is fixed by the hypothesis, the sets $U_{i}$ are defined by a formula, and the three cases are decided by definable conditions; the argument therefore runs in $Z F$ .

Depends on

Used by

Dependency tree · two levels

46 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

GMU Math 631 course notes, Axioms of separation (standard reference, not scraped)