Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck 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.

A space is normal if and only if every closed A inside an open U admits an open V with A⊆V⊆V‾⊆U

Statement

Let (X,T) be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), with closures as in Interior, closure, boundary, exterior, derived set and isolated point in a topological space. The following two conditions are equivalent.

In particular, in a normal space any two disjoint closed sets A and D admit an open V⊇A with V‾∩D=∅: apply (b) to A and the open set X∖D. That corollary is the form in which normality is used later on this page.

Facts & Assumptions

Given: A topological space (X,T), a closed set A, an open set U with A⊆U, and disjoint closed sets A0,B0.

[L2]

A set is closed exactly when its complement is open, and complementation reverses inclusion (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct
1.1

Assume (a), and let A be closed with A⊆U and U open; then B:=X∖U is closed by [L2] and A∩B=∅, so [A1] gives disjoint open V⊇A and W⊇B.

A1L2assume-hyp
1.2

Assume (b), and let A0,B0 be disjoint closed sets; then U0:=X∖B0 is open by [L2] and contains A0, so (b) gives an open V0 with A0⊆V0⊆V0‾⊆U0.

L2assume-hyp
2.1

Under step 1.1: V⊆X∖W, since V∩W=∅, and X∖W is closed by [L2], so V‾⊆X∖W by [L1]; and X∖W⊆X∖B=U because B⊆W and complementation reverses inclusion.

step 1.1L1L2
2.2

Under step 1.2: put W0:=X∖V0‾, which is open by [L1] and [L2]; then V0∩W0=∅ because V0⊆V0‾, and B0=X∖U0⊆X∖V0‾=W0 because V0‾⊆U0.

step 1.2L1L2
3.1

Step 2.1 gives A⊆V⊆V‾⊆U with V open, so (a) implies (b).

step 2.1
3.2

Step 2.2 gives disjoint open V0⊇A0 and W0⊇B0, so (b) implies (a) by [A1].

step 2.2A1
4.1

Steps 3.1 and 3.2 make (a) and (b) equivalent.

step 3.1step 3.2
5.1

For the final assertion, let A and D be disjoint closed sets in a normal X; then X∖D is open by [L2] and contains A, so (b) gives an open V with A⊆V⊆V‾⊆X∖D, whence V‾∩D=∅.

step 4.1L2∎

Remarks

Depends on

Used by

Dependency tree · two levels

10 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