LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement

Statement

Let $n \geq 1$ and let $B_{0}, \dots, B_{m - 1}$ be a finite list of half-open boxes in $R^{n}$ (Half-open boxes in $R^{n}$ and their volume), where $B_{j} = B (a^{j}, b^{j})$ . For $i < n$ put

$C_{i} : = {- \infty, + \infty} \cup {a_{i}^{j} : j < m} \cup {b_{i}^{j} : j < m} \subseteq \overline{R},$

a finite set with at least two members, and let $c_{i, 0} < c_{i, 1} < \dots < c_{i, N_{i}}$ be its increasing enumeration, so that $c_{i, 0} = - \infty$ , $c_{i, N_{i}} = + \infty$ and $N_{i} \geq 1$ . The cells of the grid generated by the list are the half-open boxes

$Q_{k} : = B ((c_{i, k_{i}})_{i < n}, (c_{i, k_{i} + 1})_{i < n}), k_{i} < N_{i} (i < n) .$

Then:

the cells are pairwise disjoint and their union is $R^{n}$ ;
for every $j < m$ , a cell that meets $B_{j}$ is contained in $B_{j}$ , and $B_{j}$ is the union of the cells contained in it;
consequently every elementary set (Elementary sets: the finite unions of half-open boxes in $R^{n}$ ) is the union of a finite list of pairwise disjoint half-open boxes.

Facts & Assumptions

Given: A natural number $n \geq 1$ , a finite list $B_{0}, \dots, B_{m - 1}$ of half-open boxes with parameter pairs $(a^{j}, b^{j})$ , and the sets $C_{i}$ and cells $Q_{k}$ displayed in the Statement.

[L1]

$B (a, b) : = {x \in R^{n} : a_{i} < x_{i} \leq b_{i} for every i < n}$ (Half-open boxes in $R^{n}$ and their volume).

[L2]

A subset $E \subseteq R^{n}$ is an elementary set when there are a natural number $m$ and a list $B_{0}, \dots, B_{m - 1}$ of half-open boxes with $E = ⋃_{j < m} B_{j}$ (Elementary sets: the finite unions of half-open boxes in $R^{n}$ ).

[F1]

$(\overline{R}, \leq)$ is a totally ordered set, and the inclusion of $R$ preserves and reflects the order; $- \infty$ is the least and $+ \infty$ the greatest element of $\overline{R}$ , and $- \infty < x < + \infty$ for every $x \in R$ (The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined).

Proof

technique · direct

1.1

Each $C_{i}$ is a finite subset of the totally ordered set $\overline{R}$ containing the two distinct elements $- \infty$ and $+ \infty$ , so it has a unique strictly increasing enumeration $c_{i, 0} < \dots < c_{i, N_{i}}$ with $N_{i} \geq 1$ , and its least and greatest members are $c_{i, 0} = - \infty$ and $c_{i, N_{i}} = + \infty$ .

1.2

For claim 1, distinct multi-indices $k \neq k^{'}$ differ at some $i$ , say $k_{i} < k_{i}^{'}$ , whence $k_{i} + 1 \leq k_{i}^{'}$ and $c_{i, k_{i} + 1} \leq c_{i, k_{i}^{'}}$ ; a common point $x$ would satisfy both $x_{i} \leq c_{i, k_{i} + 1}$ and $c_{i, k_{i}^{'}} < x_{i}$ , which is impossible, so the cells are pairwise disjoint.

L1F1

1.3

For claim 1 again, given $x \in R^{n}$ and $i < n$ , the set ${r \leq N_{i} : c_{i, r} < x_{i}}$ contains $0$ because $c_{i, 0} = - \infty < x_{i}$ and omits $N_{i}$ because $c_{i, N_{i}} = + \infty$ is not below the real $x_{i}$ , so it has a greatest member $k_{i}$ with $k_{i} < N_{i}$ , and then $c_{i, k_{i}} < x_{i} \leq c_{i, k_{i} + 1}$ ; the multi-index $k$ so obtained puts $x$ in $Q_{k}$ .

L1F1

1.4

For claim 2, suppose $x \in Q_{k} \cap B_{j}$ and fix $i < n$ . From $a_{i}^{j} < x_{i} \leq c_{i, k_{i} + 1}$ and $a_{i}^{j} \in C_{i}$ it follows that $a_{i}^{j} < c_{i, k_{i} + 1}$ , and the members of $C_{i}$ strictly below $c_{i, k_{i} + 1}$ are exactly $c_{i, 0}, \dots, c_{i, k_{i}}$ , so $a_{i}^{j} \leq c_{i, k_{i}}$ ; from $c_{i, k_{i}} < x_{i} \leq b_{i}^{j}$ and $b_{i}^{j} \in C_{i}$ it follows that $c_{i, k_{i}} < b_{i}^{j}$ , and the members of $C_{i}$ strictly above $c_{i, k_{i}}$ are exactly $c_{i, k_{i} + 1}, \dots, c_{i, N_{i}}$ , so $c_{i, k_{i} + 1} \leq b_{i}^{j}$ .

L1F1

2.1

For claim 2, step 1.4 gives $a_{i}^{j} \leq c_{i, k_{i}}$ and $c_{i, k_{i} + 1} \leq b_{i}^{j}$ in every coordinate, hence $Q_{k} \subseteq B_{j}$ ; and every point of $B_{j}$ lies in some cell by step 1.3, that cell then meeting $B_{j}$ and so contained in it, so $B_{j}$ is exactly the union of the cells contained in it.

step 1.3step 1.4L1

3.1

For claim 3, let $E = ⋃_{j < m} B_{j}$ be elementary; by step 2.1 each $B_{j}$ is the union of the cells contained in it, so $E$ is the union of those cells that are contained in at least one $B_{j}$ , and by step 1.2 these finitely many cells are pairwise disjoint; listing them proves claim 3, while claims 1 and 2 are steps 1.2, 1.3 and 2.1.

step 1.2step 1.3step 2.1L2∎

Depends on

Used by

Dependency tree · two levels

14 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

T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.1 (standard reference, not scraped)
E. A. Carlen, Notes on Lebesgue Measure on $\mathbb{R}^n$ and $S^{n-1}$ (Rutgers Math 501), Section 1 (standard reference, not scraped)