Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31
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.

Assuming countable choice, the deleted Tychonoff plank is a regular nonnormal open subspace of a compact Hausdorff normal space

Statement

Assume the Axiom of Countable Choice. Let P=(ω1+1)×(ω+1) with the product of its ordinal order topologies, let p=(ω1,ω), and let T=P∖{p}. Then P is compact, Hausdorff, and normal, while T is an open regular subspace that is not normal.

Facts & Assumptions

Given: The Axiom of Countable Choice and the ordinal product P above.

[F2]

The ordinal order-topology basis gives neighbourhoods (α,ω1] of ω1, singleton neighbourhoods {n} of n<ω, and neighbourhoods (m,ω] of ω (The order topology on an ordinal, with the half-open intervals (α,β] and the initial segments [0,β] as a basis, Every ordinal with its order topology has a basis of clopen sets, and is T1, Hausdorff and regular).

Proof

technique · contradiction
1.1

The factors ω1+1 and ω+1 are compact and T3 by [L1], so [L2] makes P compact, Hausdorff, regular, and normal.

L1L2
1.2

Since P is T1, {p} is closed; hence T is open. Its regularity follows from the hereditary regularity conclusion in [L2].

L2
1.3

Put E={ω1}×ω and F=ω1×{ω}, regarded as subsets of T. The clopen ordinal basis shows that they are disjoint closed subsets of T.

F2
2.1

Suppose, for a contradiction, that T is normal. Choose disjoint open U,V⊆T with E⊆U and F⊆V.

F1step 1.3assume-contra
3.1

For n<ω, let Cn={ξ<ω1:(ξ,ω1]×{n}⊆U}. By [F2] each Cn is nonempty; [A1] chooses αn∈Cn simultaneously. The countable set {αn:n<ω} is bounded by some α<ω1.

A1F2step 2.1
3.2

Put β=α+1<ω1. Since (β,ω)∈V, [F2] gives γ<β and m<ω with (γ,β]×(m,ω]⊆V.

F2step 2.1
4.1

The point (β,m+1) lies in V by step 3.2 and in U by step 3.1, because β>α≥αm+1. This contradicts U∩V=∅, so T is not normal; together with steps 1.1 and 1.2 this proves all the stated properties.

step 1.1step 1.2step 3.1step 3.2discharge-contradiction∎

Depends on

Used by

Dependency tree · two levels

71 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