ExampleConstruction: 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 Sorgenfrey plane: the product of two half-open-interval lines has the rectangles $[a, b) \times [c, d)$ as a basis and $Q \times Q$ as a countable dense subset

Example

Let $B : = {[a, b) : a, b \in R, a < b}$ be the family of bounded half-open intervals of $R$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). Then:

$B$ is a basis for a topology $T_{S}$ on $R$ (A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis); the space $S : = (R, T_{S})$ is the Sorgenfrey line, and $T_{S}$ is finer than the usual topology (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).
The Sorgenfrey plane is $S \times S$ with the product topology (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space). The rectangles $[a, b) \times [c, d) (a < b, c < d)$ form a basis for it.
$Q \times Q$ is a dense subset of $S \times S$ (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets) and is at most countable ( $Q$ is countably infinite, A product of two at most countable sets is at most countable, Finite, countably infinite, countable, uncountable). So the Sorgenfrey plane has a countable dense subset.

The word separable is not used here: it is not defined at this point in the reading order, and claim 3 says in full what it would abbreviate. Claim 1 restates, and reproves from the basis criterion, the construction of the Sorgenfrey line; the level-8 worked example of that line is linked in the remarks rather than depended on, since it lives on an examples page.

Facts & Assumptions

Given: The family $B$ above; the Sorgenfrey line $S$ ; the product $S \times S$ with the product topology; reals $a < b$ , $c < d$ and points $x, y \in R$ .

[A1]

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

[A2]

A basis for the product topology on a product of two spaces is the family of boxes $U \times V$ with $U$ open in the first factor and $V$ open in the second (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[L1]

A family is a basis for a topology on a set exactly when it covers the set and every point of an intersection of two members lies in a member inside that intersection; the topology is then the family of unions of its members, and is unique (A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis, Basis and subbasis for a topology, and the topology generated by a family of sets).

[L2]

$U \subseteq R$ is open in the usual topology exactly when every point of $U$ has a bounded open interval around it inside $U$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L3]

A subset is dense exactly when it meets every nonempty member of a basis (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set, clause (d)).

[L4]

Strictly between any two reals lies a rational (The rationals embed densely in the reals); $Q$ is at most countable and a product of two at most countable sets is at most countable ( $Q$ is countably infinite, A product of two at most countable sets is at most countable, Finite, countably infinite, countable, uncountable).

[L5]

The order of $R$ is total, so a two-element set of reals has a maximum and a minimum (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum); a topology is a family of subsets of the underlying set (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Verification

technique · direct

1.1

$B$ covers $R$ : for $x \in R$ one has $x < x + 1$ , so $[x, x + 1) \in B$ and $x \in [x, x + 1)$ .

A1L5

1.2

$B$ satisfies the intersection condition: for $x \in [a, b) \cap [c, d)$ put $a^{'} : = \max {a, c}$ and $b^{'} : = \min {b, d}$ , available by [L5]; then $[a, b) \cap [c, d) = [a^{'}, b^{'})$ , and $a^{'} \leq x < b^{'}$ gives $a^{'} < b^{'}$ , so this is a member of $B$ containing $x$ .

A1L5

1.3

Every bounded open interval is a union of members of $B$ : $(a, b) = ⋃ {[t, b) : a < t < b}$ , since every $s \in (a, b)$ lies in $[s, b)$ and every such $[t, b)$ lies in $(a, b)$ .

1.4

Every nonempty $[a, b) \in B$ contains a rational, by [L4] applied to $a < b$ : a rational $p$ with $a < p < b$ satisfies $p \in [a, b)$ .

A1L4

2.1

By steps 1.1 and 1.2 with [L1], $B$ is a basis for a unique topology $T_{S}$ on $R$ .

step 1.1step 1.2L1

3.1

$T_{S}$ is finer than the usual topology: a set open in the usual topology is a union of bounded open intervals by [L2], and each of those is a union of members of $B$ by step 1.3, hence lies in $T_{S}$ by [L1]. With step 2.1 this is claim 1.

step 1.3step 2.1L1L2

3.2

The rectangles $[a, b) \times [c, d)$ form a basis for $S \times S$ : they are boxes with open factors, hence open by [A2] and step 2.1; and given a box $U \times V$ with $U, V \in T_{S}$ and $(x, y) \in U \times V$ , step 2.1 and [L1] supply $[a, b) \subseteq U$ containing $x$ and $[c, d) \subseteq V$ containing $y$ , whence $(x, y) \in [a, b) \times [c, d) \subseteq U \times V$ . So every basic open box of $S \times S$ is a union of such rectangles, and [L1] applies. This is claim 2.

step 2.1A2L1L5

4.1

$Q \times Q$ meets every nonempty rectangle $[a, b) \times [c, d)$ : by step 1.4 there are rationals $p \in [a, b)$ and $r \in [c, d)$ , and $(p, r)$ lies in the rectangle. By step 3.2 and [L3] the set $Q \times Q$ is therefore dense in $S \times S$ ; and it is at most countable by [L4]. This is claim 3.

step 1.4step 3.2L3L4∎

Remarks

The half-open basis is reintroduced here rather than imported. The Sorgenfrey line is worked out in full at level 8, in The Sorgenfrey line: $R$ with the half-open intervals $[a, b)$ as a basis is strictly finer than the usual topology, is first countable, has a countable dense subset, and its sequences converge only from the right, including its first countability and the fact that its sequences converge only from the right. That item lives on an examples page and so may not be a dependency of anything; the verification above repeats only the part needed here, directly from A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis.
The plane is genuinely finer than the Euclidean plane. Every open rectangle $(a, b) \times (c, d)$ is open in $S \times S$ by step 3.1 and [A2], while $[0, 1) \times [0, 1)$ is open in $S \times S$ and is not open in $R^{2}$ , since no Euclidean ball around $(0, 0)$ lies inside it. Nothing above depends on that comparison, and it is recorded here for orientation.
What makes this example worth having is its subspace, not the plane itself. The next item exhibits an uncountable discrete subspace of $S \times S$ , which by claim 3 shows that "has a countable dense subset" is not a hereditary property.

Depends on

Used by

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

Dependency tree · next 3 levels

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

Sorgenfrey plane (Wikipedia) (standard reference, not scraped)
Lower limit topology (Wikipedia) (standard reference, not scraped)

The Sorgenfrey plane: the product of two half-open-interval lines has the rectangles [a,b)×[c,d)[a,b)×[c,d) as a basis and Q×QQ×Q as a countable dense subset