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.
Half-open boxes are closed under intersection, and the complement of a half-open box is a finite disjoint union of half-open boxes
Statement
Let and let half-open boxes be as in Half-open boxes in and their volume.
- Intersection. For parameter pairs and , the extremes taken in the total order of . Consequently the intersection of the members of a finite list of half-open boxes is a half-open box, the empty list giving .
- Complement. For every parameter pair there is a finite list of pairwise disjoint half-open boxes whose union is . When the list may be taken to have members, indexed by a coordinate and a side.
Facts & Assumptions
Given: A natural number and parameter pairs , , that is, pairs of functions .
, and (Half-open boxes in and their volume).
A box is nonempty exactly when for every (Half-open boxes in and their volume).
is a totally ordered set, and the inclusion of preserves and reflects the order (The extended real line , its order, and the arithmetic that is left undefined).
Proof
For claim 1, a point lies in exactly when and for every ; the order being total, each two-element set has a greatest member and each a least member , and for a real the conjunction and says exactly while and says exactly , so the intersection is ; iterating along a list of length gives the finite case by induction on , with the empty list giving .
For claim 2 in the degenerate case, if then , a list with the single member , whose members are vacuously pairwise disjoint.
For claim 2 in the remaining case, assume , so for every , and for define two parameter pairs and by setting, in coordinates , and ; in coordinate , and ; and in coordinates , and .
Still for claim 2, every lies in one of these boxes: the set of with is a nonempty subset of , so it has a least member ; then for every , and by totality either , putting in , or , putting in , the coordinates being unconstrained in both.
Still for claim 2, each of the boxes is disjoint from , since its points satisfy or ; and two of them are disjoint from one another, because for a point of a box with index fails while a point of a box with index satisfies it, and for a common a point of both would satisfy , contradicting .
Claim 1 is step 1.1, and claim 2 is step 1.2 in the empty case and steps 2.1 and 2.2 in the nonempty case, the union of the boxes being exactly .
Depends on
Used by
Dependency tree · two levels
13 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
- E. A. Carlen, Notes on Lebesgue Measure on $\mathbb{R}^n$ and $S^{n-1}$ (Rutgers Math 501), Section 1 (standard reference, not scraped)
- T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.1 (standard reference, not scraped)