Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

The antidiagonal {(x,x)}\{(x,-x)\} is an uncountable discrete subspace of the Sorgenfrey plane, so having a countable dense subset is not a hereditary property

Statement refuted

Refuted: that the property "has a countable dense subset" is hereditary (Hereditary, open-hereditary and closed-hereditary properties of topological spaces, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets).

Witness. In the Sorgenfrey plane S×SS \times S (The Sorgenfrey plane: the product of two half-open-interval lines has the rectangles [a,b)×[c,d)[a,b) \times [c,d) as a basis and Q×Q\mathbb{Q} \times \mathbb{Q} as a countable dense subset), which has the countable dense subset Q×Q\mathbb{Q}\times\mathbb{Q}, take the antidiagonal

L  :=  {(x,x):xR}L \;:=\; \{\, (x,-x) : x \in \mathbb{R} \,\}

with the subspace topology (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). Then:

  1. LL is discrete: for every xx, the basic rectangle [x, x+1)×[x, x+1)[x,\ x+1) \times [-x,\ -x+1) meets LL exactly in {(x,x)}\{(x,-x)\}, so every singleton of LL is open in LL and the subspace topology is the discrete one (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).
  2. LL is uncountable (Finite, countably infinite, countable, uncountable), being in bijection with R\mathbb{R} (R\mathbb{R} is uncountable (Cantor's nested intervals, 1874)).
  3. The only dense subset of LL is LL itself, since in a discrete space every subset is closed. So LL has no countable dense subset, although the space it sits inside has one.

The word separable is not used: it is not defined at this point in the reading order, and the three claims above say in full what it would abbreviate.

Facts & Assumptions

Given: The Sorgenfrey plane S×SS \times S with the rectangles [a,b)×[c,d)[a,b)\times[c,d) as a basis, the antidiagonal LL with the subspace topology, and a subset DLD \subseteq L.

[A1]

The rectangles [a,b)×[c,d)[a,b)\times[c,d) with a<ba<b and c<dc<d form a basis for S×SS \times S, and Q×Q\mathbb{Q}\times\mathbb{Q} is a countable dense subset of it (The Sorgenfrey plane: the product of two half-open-interval lines has the rectangles [a,b)×[c,d)[a,b) \times [c,d) as a basis and Q×Q\mathbb{Q} \times \mathbb{Q} as a countable dense subset).

[A2]

The open sets of LL are the traces BLB \cap L with BB open in S×SS \times S, and a basis of them is the family of traces of basic open sets (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).

[L1]

[a,b)={t:at<b}[a,b) = \{\, t : a \le t < b \,\} (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

[L3]

R\mathbb{R} is uncountable: there is no surjection NR\mathbb{N} \to \mathbb{R} (R\mathbb{R} is uncountable (Cantor's nested intervals, 1874), Finite, countably infinite, countable, uncountable). A nonempty at most countable set admits a surjection from N\mathbb{N} (A nonempty set is at most countable iff it is a surjective image of N\mathbb{N}), and a composite of surjections is a surjection (Injection, surjection, bijection).

Counterexample

technique · direct
1.1

For xRx \in \mathbb{R} put Bx:=[x, x+1)×[x, x+1)B_x := [x,\ x+1) \times [-x,\ -x+1), a basic open set of S×SS \times S containing (x,x)(x,-x), by [A1] and [L1].

A1L1
1.2

The map φ:RL\varphi : \mathbb{R} \to L, φ(x):=(x,x)\varphi(x) := (x,-x), is a surjection, every point of LL being of that form.

given
2.1

BxL={(x,x)}B_x \cap L = \{(x,-x)\}: a point of LL is (t,t)(t,-t), and it lies in BxB_x exactly when xt<x+1x \le t < x+1 and xt<x+1-x \le -t < -x+1; the second pair of inequalities says x1<txx - 1 < t \le x, and together with xtx \le t this forces t=xt = x.

step 1.1L1
2.2

LL is uncountable: if LL were at most countable then, being nonempty, it would admit a surjection NL\mathbb{N} \to L by [L3]; composing that with the surjection LRL \to \mathbb{R}, (x,x)x(x,-x) \mapsto x, would give a surjection NR\mathbb{N} \to \mathbb{R}, contradicting [L3]. This is claim 2.

step 1.2L3
3.1

By steps 1.1 and 2.1 with [A2], every singleton {(x,x)}\{(x,-x)\} is open in LL; hence every subset of LL is a union of singletons and so is open, and the subspace topology on LL is the discrete one. This is claim 1.

step 1.1step 2.1A2A3
4.1

By step 3.1 and [A3] every subset of LL is closed in LL, so D=D\overline{D} = D for every DLD \subseteq L, and DD is dense in LL exactly when D=LD = L by [L2]. With step 2.2 the only dense subset of LL is uncountable, so LL has no countable dense subset. This is claim 3.

step 3.1step 2.2A3L2
5.1

By [A1] the space S×SS \times S has a countable dense subset and by step 4.1 its subspace LL has none, so the property "has a countable dense subset" is not hereditary, which refutes the claim.

step 4.1A1

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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