ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (claude-sonnet-5 + deepseek-v4-pro)verified 2026-08-05 (claude-sonnet-5)

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 the Axiom of Choice, compactness of $[0,1]$ derived from the subbase lemma alone, using only the rays as a subbasis and the least upper bound property

Example

Let $L := [0,1] = \{\, t \in \mathbb{R} : 0 \le t \le 1 \,\}$ (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length) be linearly ordered by the order of $\mathbb{R}$ (Order on the reals) and carry the order topology of that order (The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua), whose subbasis is the family

$\mathcal{S} \;:=\; \{\, L_{<b} : b \in L \,\} \cup \{\, L_{>a} : a \in L \,\}, \qquad L_{<b} = \{t \in L : t < b\}, \quad L_{>a} = \{t \in L : a < t\}.$

Then, assuming the Axiom of Choice, $L$ is compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right), and the proof below uses only Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma, which is where that hypothesis is spent, and the least upper bound property of $\mathbb{R}$ (Complete ordered field (least-upper-bound property)): no bisection, no metric, and no sequence.

This is a genuinely different route to the same conclusion. Compactness of $[0,1]$ also follows from Heine-Borel, and that is how it is obtained on the companion page; the point of the present derivation is that the subbase lemma reduces the problem to covers by rays, where the least upper bound property does all the work in one step.

Facts & Assumptions

Given: $L = [0,1]$ with the order inherited from $\mathbb{R}$ , its order topology, and the subbasis $\mathcal{S}$ of open rays.

[L1]

Alexander's subbase lemma, assuming the Axiom of Choice in the form of Zorn's lemma: if $\mathcal{S}$ is a subbasis for the topology of a space $Z$ and every family $\mathcal{S}_0 \subseteq \mathcal{S}$ with $\bigcup \mathcal{S}_0 = Z$ has a finite subfamily with union $Z$ , then $Z$ is compact (Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma, Basis and subbasis for a topology, and the topology generated by a family of sets).

[L2]

$\mathcal{S}$ is a subbasis for the order topology of $L$ (The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L3]

Every nonempty subset of $\mathbb{R}$ bounded above has a least upper bound, and for such a set $S$ and an upper bound $u$ one has $u = \sup S$ exactly when every real $\varepsilon > 0$ admits $s \in S$ with $u - \varepsilon < s$ (Complete ordered field (least-upper-bound property), Epsilon characterisation of the supremum, Upper bound, least upper bound, and strict upper bound).

[L4]

The order of Order on the reals makes $\mathbb{R}$ a totally ordered field, so any two reals are comparable (The reals form a totally ordered field); and $0 \le t \le 1$ for every $t \in L$ (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

Verification

technique · direct

1.1

Let $\mathcal{S}_0 \subseteq \mathcal{S}$ satisfy $\bigcup \mathcal{S}_0 = L$ , and put $A := \{\, b \in L : L_{<b} \in \mathcal{S}_0 \,\}$ and $B := \{\, a \in L : L_{>a} \in \mathcal{S}_0 \,\}$ , so that $\mathcal{S}_0$ consists of the rays $L_{<b}$ with $b \in A$ and the rays $L_{>a}$ with $a \in B$ .

L2construct

1.2

The point $0$ lies in no $L_{>a}$ with $a \in L$ , since $a < 0$ is impossible in $L$ by [L4]; so $0$ lies in some $L_{<b}$ with $b \in A$ , and in particular $A$ is nonempty and $0 < b$ for that $b$ .

L4construct

2.1

Put $C := \{\, t \in L : t < b \text{ for some } b \in A \,\}$ , which contains $0$ by step 1.2 and is bounded above by $1$ ; so [L3] gives $s := \sup C$ , and $0 \le s \le 1$ , that is $s \in L$ .

L3L4step 1.1step 1.2

3.1

$s$ lies in some member of $\mathcal{S}_0$ , and that member cannot be a ray $L_{<b}$ with $b \in A$ : if it were, then $s < b$ , and the point $t := (s+b)/2$ would satisfy $s < t < b \le 1$ and $t \ge s \ge 0$ , so $t \in L$ and $t \in C$ by the definition of $C$ , contradicting $s = \sup C$ . So $s \in L_{>a}$ for some $a \in B$ , with $a < s$ .

L3L4step 1.1step 2.1

4.1

By [L3] there is $t \in C$ with $a < t \le s$ , and by the definition of $C$ there is $b \in A$ with $t < b$ ; in particular $a < b$ . Then $L = L_{<b} \cup L_{>a}$ : a point $u \in L$ has $u < b$ , or else $u \ge b > a$ and $u \in L_{>a}$ .

L3L4step 2.1step 3.1

5.1

So the two members $L_{<b}$ and $L_{>a}$ of $\mathcal{S}_0$ cover $L$ . As $\mathcal{S}_0$ was an arbitrary cover of $L$ by members of $\mathcal{S}$ , [L1] and [L2] make $L$ compact.

L1L2step 3.1step 4.1∎

Remarks

The order topology of $L$ and the subspace topology $L$ inherits from the usual topology of $\mathbb{R}$ are compared nowhere below; every statement here is about the order topology alone (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, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, The absolute value makes $\mathbb{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, 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).

Where the least upper bound property enters. Exactly once, at step 2.1, to produce $s$ ; everything after that is bookkeeping about which of the two kinds of ray contains $s$ . That is the whole content of the compactness of a closed interval, and the subbase lemma is what allows the argument to be run against rays only, which is why it comes out so short.

The cost is the Axiom of Choice, and it is inherited. Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma is proved from Zorn's lemma, so this derivation spends the Axiom of Choice, whereas the bisection proof of Heine-Borel spends nothing. The two routes therefore have different prices for the same conclusion, and the cheaper one is the metric one.

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: 110 results over 22 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

Alexander subbase theorem (Wikipedia) (standard reference, not scraped)
Heine-Borel theorem (Wikipedia) (standard reference, not scraped)
Stacks Project, Lemma 5.12.15: Alexander subbase theorem (standard reference, not scraped)

Assuming the Axiom of Choice, compactness of [0,1][0,1][0,1] derived from the subbase lemma alone, using only the rays as a subbasis and the least upper bound property