LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Every open subset of the real line is a countable union of open intervals with rational endpoints

Statement

Every open set $U \subseteq R$ is a countable union of intervals $(a, b)$ with $a, b \in Q$ and $a < b$ . For $U = \emptyset$ , the indexing family is empty.

Facts & Assumptions

Given: An open subset $U$ of $R$ .

[L1]

For $n \geq 1$ , the rational open boxes form a countable basis for the product topology on $R^{n}$ ( $Q^{n}$ is a countable dense subset of $R^{n}$ , and rational open boxes form a countable basis).

[L2]

Every subset of an at most countable set is at most countable (Every subset of an at most countable set is at most countable).

Proof

technique · direct

1.1L1L2construct

Let $I_{U}$ be the family of rational open intervals contained in $U$ . By [L1] with $n = 1$ , this is a subfamily of a countable family, so [L2] makes it at most countable.

2.1step 1.1L1∎

Every member of $I_{U}$ lies in $U$ . Conversely, the basis clause of [L1] puts each $x \in U$ in some $I \in I_{U}$ . Thus $U = ⋃ I_{U}$ ; when $U$ is empty both sides are empty.

Depends on

Used by

Seven generating families for the Borel sigma-algebra on the real line Theorem

Dependency tree · two levels

23 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

R. F. Bass, Real Analysis for Graduate Students, version 5.0, Proposition 2.8 (standard reference, not scraped)