Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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.

For n at least one, open sets, closed sets, compact sets, open balls, boxes, rational open boxes, and rational half-open boxes generate the Borel sigma-algebra on R^n

Statement

Let nN with n1. In the product topology on Rn, each of the following families generates B(Rn): all open sets; all closed sets; all compact sets; all Euclidean open balls; all open boxes; all rational open boxes; and all rational half-open boxes i<n(ai,bi] with rational endpoints ai<bi.

Facts & Assumptions

Given: A natural number n1 and the product topology on Rn.

[L1]

The rational open boxes form a countable basis for the product topology on Rn, and Qn is countable and dense (Qn is a countable dense subset of Rn, and rational open boxes form a countable basis).

[L2]

In a metric topology, every point of an open set has an open ball contained in that set (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).

[L3]

The product topology on Rn is the Euclidean metric topology, and a subset is compact if and only if it is closed and bounded (A subset of Rn with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology).

[L4]

The real field is a complete ordered field (The Cauchy-sequence reals have the least-upper-bound property), so every real number is below some positive natural number (Every complete ordered field is Archimedean).

[L5]

For every positive real ε, some positive natural number m satisfies 1/m<ε (For every ε>0 in a complete ordered field there is a natural n1 with 1/n<ε).

[L6]

Families that lie in each other's generated sigma-algebras generate the same sigma-algebra (Two families generate the same sigma-algebra when each lies in the sigma-algebra generated by the other).

Proof

technique · direct
1.1

By [L1], every open set is the union of the subfamily of rational open boxes it contains, and that subfamily is countable. Thus the rational open boxes generate the open sets and hence B(Rn); all open boxes generate the same sigma-algebra.

L1
1.2

By rational density in [L1], every rational open box is the union of the rational half-open boxes contained in it. Conversely, i<n(ai,bi]=m1i<n(ai,bi+1/m) by [L5], so rational open and rational half-open boxes lie in each other's generated sigma-algebras.

L1L5algebra
1.3

Open and closed sets generate the same sigma-algebra by complementation. Euclidean balls with centres in Qn and radii 1/m form a countable basis: for a ball of radius r about x, use [L5] to choose m with 2/m<r, then use the density in [L1] to choose qQn with d(x,q)<1/m. Thus xB(q,1/m)B(x,r). By [L2] and [L3], every open set is therefore a countable union of open balls, while every open ball is open.

L1L2L3L5
2.1

By [L6], step 1.2 and step 1.1 identify the sigma-algebra generated by rational half-open boxes with B(Rn).

step 1.1step 1.2L6
3.1

By [L4], every closed FRn is m1(F[m,m]n). Each term is closed and bounded, hence compact by [L3], while every compact set is closed. Therefore compact sets and closed sets generate the same sigma-algebra. Combining this with steps 1.1, 2.1, and 1.3 proves the claim for all displayed families.

step 1.1step 2.1step 1.3L3L4L6

Depends on

Used by

Dependency tree · next 3 levels

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