Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

In a metric space any two separated sets have disjoint open neighbourhoods, so every metrizable space is completely normal

Statement

Let (X,d)(X,d) be a metric space (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric) with its metric topology (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 let A,BXA, B \subseteq X be separated (Separated sets: AB=AB=\overline{A} \cap B = A \cap \overline{B} = \varnothing). Then there are disjoint open sets UAU \supseteq A and VBV \supseteq B.

Consequently every metrizable space (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not) is completely normal, and hence normal (Completely normal (T5T_5) and perfectly normal (T6T_6) spaces, Normal spaces and T4T_4 spaces, with the source disagreement over whether normality includes T1T_1 stated explicitly).

No choice principle is used. The two open sets are unions indexed by the points of AA and of BB, and the radius attached to a point is the number d(a,B)/2d(a,B)/2, which is determined by aa, by BB and by dd; nothing is selected.

Facts & Assumptions

Given: A metric space (X,d)(X,d) and separated sets A,BXA, B \subseteq X, so that AB=AB=\overline{A} \cap B = A \cap \overline{B} = \varnothing, with closures taken in the metric topology.

[A1]

AA and BB are separated: AB=\overline{A} \cap B = \varnothing and AB=A \cap \overline{B} = \varnothing (Separated sets: AB=AB=\overline{A} \cap B = A \cap \overline{B} = \varnothing).

[L1]

For nonempty SXS \subseteq X and xXx \in X the distance d(x,S)=inf{d(x,s):sS}d(x,S) = \inf\{\, d(x,s) : s \in S \,\} exists in R\mathbb{R}, is a lower bound of that set, and satisfies d(x,S)0d(x,S) \ge 0 (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Greatest lower bound (infimum), Every nonempty set bounded below has an infimum, Nonnegativity of a metric is a consequence of the other axioms, not an axiom).

[L2]

For nonempty SXS \subseteq X, S={xX:d(x,S)=0}\overline{S} = \{\, x \in X : d(x,S) = 0 \,\} (The closure of a nonempty AA is {x:d(x,A)=0}\{x : d(x,A) = 0\}, equals AA together with its limit points, and is the smallest closed superset, claim 1).

[L4]

xB(x,r)x \in B(x,r) for every r>0r > 0, and yB(x,r)y \in B(x,r) means d(x,y)<rd(x,y) < r (Open ball, closed ball and sphere in a metric space).

[L5]

The triangle inequality d(p,q)d(p,x)+d(x,q)d(p,q) \le d(p,x) + d(x,q) and symmetry d(p,q)=d(q,p)d(p,q) = d(q,p) (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L6]

A two-element set of reals has a maximum, which is one of the two and is at least the other (Maximum and minimum of a set).

Proof

technique · direct
1.1

If A=A = \varnothing then U:=U := \varnothing and V:=XV := X are disjoint open sets with AUA \subseteq U and BVB \subseteq V; if B=B = \varnothing then U:=XU := X and V:=V := \varnothing do the same.

L3construct
1.2

Assume from here that AA and BB are both nonempty, so that d(x,A)d(x,A) and d(x,B)d(x,B) are defined for every xXx \in X.

L1assume-hyp
2.1

For aAa \in A: aBa \notin \overline{B} by [A1], so d(a,B)0d(a,B) \ne 0 by [L2], and d(a,B)0d(a,B) \ge 0 by [L1]; hence ra:=d(a,B)/2>0r_a := d(a,B)/2 > 0. Symmetrically sb:=d(b,A)/2>0s_b := d(b,A)/2 > 0 for bBb \in B.

step 1.2A1L1L2
3.1

Define U:=aAB(a,ra)U := \bigcup_{a \in A} B(a, r_a) and V:=bBB(b,sb)V := \bigcup_{b \in B} B(b, s_b); both are open by [L3], and AUA \subseteq U and BVB \subseteq V by [L4].

step 2.1L3L4construct
4.1

Suppose xUVx \in U \cap V; then there are aAa \in A and bBb \in B with d(a,x)<rad(a,x) < r_a and d(b,x)<sbd(b,x) < s_b.

step 3.1L4assume-hyp
5.1

Under step 4.1: d(a,b)d(a,x)+d(x,b)<ra+sbd(a,b) \le d(a,x) + d(x,b) < r_a + s_b, using symmetry for d(x,b)=d(b,x)d(x,b) = d(b,x).

step 4.1L5
5.2

Under step 4.1: ra+sb2max{ra,sb}=max{d(a,B), d(b,A)}r_a + s_b \le 2\max\{r_a, s_b\} = \max\{d(a,B),\ d(b,A)\}, by [L6] and the definitions of rar_a and sbs_b.

step 2.1step 4.1L6
5.3

d(a,B)d(a,b)d(a,B) \le d(a,b), since bBb \in B makes d(a,b)d(a,b) a member of the set whose infimum is d(a,B)d(a,B); and d(b,A)d(b,a)=d(a,b)d(b,A) \le d(b,a) = d(a,b) for the same reason with the roles exchanged.

step 4.1L1L5
6.1

By steps 5.1, 5.2 and 5.3, d(a,b)<max{d(a,B),d(b,A)}d(a,b)d(a,b) < \max\{d(a,B), d(b,A)\} \le d(a,b), which is impossible; so no such xx exists and UV=U \cap V = \varnothing.

step 5.1step 5.2step 5.3
7.1

By steps 1.1, 3.1 and 6.1 the separated pair A,BA, B has disjoint open supersets in every case.

step 1.1step 3.1step 6.1
8.1

If (Y,T)(Y,\mathcal{T}) is metrizable, fix a metric dd inducing T\mathcal{T}; separation of two subsets is a statement about the closure operator, and the topological closure of a metrizable space is the metric closure of any inducing metric, so step 7.1 applies verbatim and YY is completely normal, hence normal.

step 7.1L2

Remarks

  • The halving is what makes the balls miss each other. Radii d(a,B)d(a,B) and d(b,A)d(b,A) without the factor 22 would not do: two balls of those radii can meet, and the triangle inequality then gives no contradiction. With the halving the sum of the two radii is at most the larger of the two distances, which is at most d(a,b)d(a,b).

  • Separated, not merely disjoint, is exactly the right hypothesis. For disjoint sets the radii can fail to be positive: in R\mathbb{R} the disjoint sets (0,1)(0,1) and [1,2)[1,2) have d(1,(0,1))=0d(1, (0,1)) = 0, and indeed they are not separated. What the hypothesis buys is positivity of every radius, and nothing else.

  • The corresponding statement for R\mathbb{R} needs no new proof. R\mathbb{R} with its usual topology is metrizable by the usual metric (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), so it is completely normal, and so is every Rn\mathbb{R}^n and every subspace of a metrizable space.

Depends on

Used by

Dependency tree · next 3 levels

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