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

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

Statement

Let $n \geq 1$ , assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), and let $a_{i} \leq b_{i}$ be reals for $i < n$ . Write

$R^{\circ} : = {x \in R^{n} : a_{i} < x_{i} < b_{i} for every i < n}, \overline{R} : = [a, b] = {x \in R^{n} : a_{i} \leq x_{i} \leq b_{i} for every i < n}$

(Axis-parallel rectangles in $R^{m}$ and their volume). Then $R^{\circ}$ is open and $\overline{R}$ is closed, so both are Borel and Lebesgue measurable, and every set $R$ with $R^{\circ} \subseteq R \subseteq \overline{R}$ is Lebesgue measurable with

$λ_{n} (R) = \prod_{i < n} (b_{i} - a_{i}) .$

In particular this covers the four one-dimensional face conventions in each coordinate — the open box, the closed box $[a, b]$ , the half-open box $B (a, b) = \prod_{i < n} (a_{i}, b_{i}]$ of Half-open boxes in $R^{n}$ and their volume, and every mixture of them, in any combination of coordinates — and it gives measure $0$ to all of them whenever $a_{i} = b_{i}$ for some $i < n$ . For a half-open box with infinite parameters the value is already $λ_{n} (B) = vol (B)$ (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

Statement references

The Axiom of Countable Choice ( ${A C}_{ω}$ )

Axis-parallel rectangles in $R^{m}$ and their volume

Half-open boxes in $R^{n}$ and their volume

Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume

Facts & Assumptions

Given: A natural number $n \geq 1$ , the Axiom of Countable Choice, reals $a_{i} \leq b_{i}$ for $i < n$ , and the sets $R^{\circ}$ , $\overline{R}$ displayed in the Statement.

[L1]

Assuming countable choice, $L (R^{n})$ is a sigma-algebra, $λ_{n}$ is a complete measure on it, every set of Lebesgue outer measure zero is Lebesgue measurable of measure zero, and $λ_{n} (B) = vol (B)$ for every half-open box $B$ (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

[L2]

Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable (Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable).

[L3]

Assuming countable choice, $λ_{n}^{*}$ is an outer measure on $R^{n}$ (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume), so it is monotone and countably subadditive (Outer measures, Lebesgue outer measure on $R^{n}$ ).

[L4]

For a nonempty box $vol (B) : = \prod_{i < n} (b_{i} - a_{i})$ when every $a_{i}$ and every $b_{i}$ is real, and a box is nonempty exactly when $a_{i} < b_{i}$ for every $i < n$ (Half-open boxes in $R^{n}$ and their volume).

[F1]

$[a, b] : = {x \in R^{m} : a_{j} \leq x_{j} \leq b_{j} (j < m)}$ and $vol [a, b] : = \prod_{j < m} (b_{j} - a_{j})$ (Axis-parallel rectangles in $R^{m}$ and their volume).

[F2]

A measure on $(X, A)$ is a function $μ : A \to [0, + \infty]$ with $μ (\emptyset) = 0$ that is countably additive on pairwise disjoint sequences (Measures on sigma-algebras).

[F3]

For every real $ε > 0$ there is a natural number $k \geq 1$ with $1 / k < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F4]

$\prod_{k < n} (a_{k} b_{k}) = (\prod_{k < n} a_{k}) (\prod_{k < n} b_{k})$ ; if $a_{k} \geq 0$ for all $k < n$ then $\prod_{k < n} a_{k} \geq 0$ , with $\prod_{k < n} a_{k} > 0$ when every $a_{k} > 0$ ; and finite products are defined by the recursion $Π_{0} = 1$ , $Π_{σ (n)} = Π_{n} \cdot a_{n}$ (Laws of finite sums and finite products, claim 6; Finite sums and finite products, by recursion).

[F5]

A subset $U \subseteq X$ is open in $(X, d)$ if for every $x \in U$ there is a real $r > 0$ with $B (x, r) \subseteq U$ ; a subset $F$ is closed if its complement is open (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).

[F6]

The forms $[a, b)$ and $(a, b]$ are half-open, and an interval is open when both of its written endpoints are excluded, closed when both are included (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1L2F1F5F6

$R^{\circ}$ is open and $\overline{R}$ is closed in $(R^{n}, d_{2})$ , by the same coordinatewise estimate in each case, so both are Borel and hence Lebesgue measurable.

1.2L1L3L4F1F3F4

A closed rectangle with a degenerate side is Lebesgue null: let $u_{i} \leq v_{i}$ be reals with $u_{i_{0}} = v_{i_{0}} = c$ for some $i_{0} < n$ , and let $η$ be a positive real; the half-open box with parameter pairs $(u_{i} - 1, v_{i}]$ for $i \neq i_{0}$ and $(c - η, c]$ in coordinate $i_{0}$ is nonempty, contains $[u, v]$ , and has volume $η C$ where $C : = \prod_{i < n} w_{i} > 0$ with $w_{i_{0}} : = 1$ and $w_{i} : = v_{i} - u_{i} + 1$ otherwise, so monotonicity of the outer measure gives $λ_{n}^{*} ([u, v]) \leq η C$ for every positive real $η$ and hence $λ_{n}^{*} ([u, v]) = 0$ .

2.1step 1.2L1L3

The difference $\overline{R} ∖ R^{\circ}$ is contained in the union of the $2 n$ closed rectangles obtained from $[a, b]$ by replacing the $i$ -th side by the degenerate side $[a_{i}, a_{i}]$ or by $[b_{i}, b_{i}]$ , each of which is Lebesgue null by step 1.2, so countable subadditivity of the outer measure, applied to that finite list padded with empty sets, gives $λ_{n}^{*} (\overline{R} ∖ R^{\circ}) = 0$ ; every subset of $\overline{R} ∖ R^{\circ}$ is therefore Lebesgue measurable of measure $0$ .

2.2step 1.2L1F4

Suppose instead $a_{i_{0}} = b_{i_{0}}$ for some $i_{0} < n$ . Then $R^{\circ} = \emptyset$ , the rectangle $\overline{R}$ is Lebesgue null by step 1.2, every $R$ between them is a subset of it and so is measurable of measure $0$ , and the product $\prod_{i < n} (b_{i} - a_{i})$ has the factor $0$ and is therefore $0$ as well.

3.1step 2.1L1L4F2

Suppose first that $a_{i} < b_{i}$ for every $i < n$ . Then $B (a, b)$ is a nonempty half-open box with $R^{\circ} \subseteq B (a, b) \subseteq \overline{R}$ and $λ_{n} (B (a, b)) = vol (B (a, b)) = \prod_{i < n} (b_{i} - a_{i})$ . For $R$ with $R^{\circ} \subseteq R \subseteq \overline{R}$ , both $R ∖ B (a, b)$ and $B (a, b) ∖ R$ are contained in $\overline{R} ∖ R^{\circ}$ , hence are measurable of measure $0$ by step 2.1, so $R = (B (a, b) ∖ (B (a, b) ∖ R)) \cup (R ∖ B (a, b))$ is measurable, and additivity on the two disjoint decompositions $R = (R \cap B (a, b)) ⊔ (R ∖ B (a, b))$ and $B (a, b) = (R \cap B (a, b)) ⊔ (B (a, b) ∖ R)$ gives $λ_{n} (R) = λ_{n} (R \cap B (a, b)) = λ_{n} (B (a, b))$ .

4.1step 1.1step 2.2step 3.1∎

Steps 3.1 and 2.2 exhaust the two cases and give the displayed value in each, and step 1.1 supplies the Borel and measurability clauses for $R^{\circ}$ and $\overline{R}$ .

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

A box in RnRn with parameters ai≤biai​≤bi​ is Lebesgue measurable of measure ∏i<n(bi−ai)∏i<n​(bi​−ai​), whichever of its faces are included

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included