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

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.2L1F1

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.

1.3L1F1

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}$ .

1.4L1F1

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}$ .

2.1step 1.3step 1.4L1

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.

3.1step 1.2step 1.3step 2.1L2∎

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.

Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources