ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 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.

The nested intervals $[0, 1 / k]$ intersect in exactly ${0}$

Example

For $k \geq 1$ let $I_{k} : = [0, 1 / k]$ , a nonempty closed bounded interval (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). The family is nested, its lengths tend to $0$ , and

$⋂_{k \geq 1} [0, \frac{1}{k}] = {0} .$

This is the standard instance of the single-point case of A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ , and the intersection is computed twice over: once by the theorem, which says the intersection is a single point, and once by inspection, which says that point is $0$ .

Indexing. Written on $N$ , the family is $J_{j} : = [0, 1 / (j + 1)]$ for $j \in N$ , which is the same family under the substitution $k = j + 1$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences). The verification uses $(J_{j})$ .

Facts & Assumptions

Given: For $j \in N$ the closed bounded interval $J_{j} : = [0, 1 / (j + 1)]$ , where $j + 1$ denotes the canonical natural $(j + 1) \cdot 1_{R}$ , which is positive and hence invertible; and the lengths $ℓ_{j} : = 1 / (j + 1) - 0 = 1 / (j + 1)$ .

[L1]

Intervals: $[a, b] = {x : a \leq x \leq b}$ is a closed bounded interval, nonempty exactly when $a \leq b$ , of length $b - a$ ; and $[a, a] = {a}$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

Nested interval property: a nested sequence of nonempty closed bounded intervals has nonempty intersection, and that intersection is a single point exactly when the lengths tend to $0$ (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ ).

[L3]

Canonical naturals: $n \cdot 1_{R} > 0$ for $n \geq 1$ , and $m \mapsto m \cdot 1_{R}$ is strictly increasing (Canonical naturals are positive and strictly increasing).

[L4]

Reciprocals: $a > 0$ gives $1 / a > 0$ , and $0 < a < b$ gives $0 < 1 / b < 1 / a$ (Inverses of positives are positive, and reciprocation reverses order).

[L5]

Reciprocal Archimedean property: for every real $ε > 0$ there is a natural $n \geq 1$ with $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean).

[L6]

Absolute value: $∣ t ∣ = t$ when $t \geq 0$ (Basic properties of the absolute value).

[L7]

Convergence of a sequence of reals to $0$ ; it suffices to test a real $ε > 0$ (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L8]

Trichotomy of the order on $R$ (Complete ordered field (least-upper-bound property), Ordered field).

Verification

technique · direct

1.1

Each $J_{j}$ is a nonempty closed bounded interval: $j + 1 \geq 1$ gives $1 / (j + 1) > 0$ , so $0 \leq 1 / (j + 1)$ and [L1] applies; its length is $ℓ_{j} = 1 / (j + 1)$ .

givenL1L3L4

2.1

The family is nested: $0 < (j + 1) < (j + 2)$ gives $0 < 1 / (j + 2) < 1 / (j + 1)$ , so $0 \leq x \leq 1 / (j + 2)$ implies $0 \leq x \leq 1 / (j + 1)$ , that is $J_{j + 1} \subseteq J_{j}$ .

step 1.1L3L4

2.2

The lengths tend to $0$ . Let $ε > 0$ be real and use [L5] to fix a natural $n \geq 1$ with $1 / n < ε$ . For every $j \geq n$ we have $0 < n \leq j + 1$ , hence $0 < 1 / (j + 1) \leq 1 / n < ε$ , and $∣ ℓ_{j} - 0 ∣ = ℓ_{j} < ε$ since $ℓ_{j} > 0$ .

step 1.1L3L4L5L6L7L8

3.1

By [L2] applied to steps 1.1, 2.1 and 2.2, the intersection $⋂_{j} J_{j}$ is nonempty and is a single point.

step 1.1step 2.1step 2.2L2

4.1

That point is $0$ : indeed $0 \in J_{j}$ for every $j$ , since $0 \leq 0 \leq 1 / (j + 1)$ , so $0$ lies in the intersection, and a set that is a single point and contains $0$ is ${0}$ .

step 3.1step 1.1L1

5.1

Hence $⋂_{j} J_{j} = {0}$ , which in the notation of the statement is $⋂_{k \geq 1} [0, 1 / k] = {0}$ .

step 3.1step 4.1L1∎

Remarks

The two computations are independent and both are needed. That the intersection is a single point comes from A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ and uses that the lengths are null; that the point is $0$ comes from inspection. Without the theorem one would still have to rule out the intersection being larger than ${0}$ , which is exactly the content of the length condition.
The Archimedean property is the whole of step 2.2. In a non-Archimedean ordered field the same family has lengths that do not tend to $0$ , and the intersection contains every positive infinitesimal, so it is not a single point. What makes the example come out as stated is For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ .
Compare the open version. Removing the left endpoint gives $(0, 1 / k)$ , whose intersection is empty (The nested open intervals $(0, 1 / k)$ have empty intersection). The two computations differ in exactly one respect, whether the common point $0$ belongs to the sets, and that is the hypothesis of closedness in the theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

Nested intervals (Wikipedia) (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)

The nested intervals [0,1/k][0,1/k] intersect in exactly {0}{0}