PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The elementary sets form an algebra of subsets of $R^{n}$ containing every half-open box

Statement

Let $n \geq 1$ . The family $E_{n}$ of elementary subsets of $R^{n}$ (Elementary sets: the finite unions of half-open boxes in $R^{n}$ ) is an algebra of subsets of $R^{n}$ (Algebras of subsets): it contains $\emptyset$ , it is closed under complement in $R^{n}$ , and it is closed under union of two members. It contains every half-open box, and it is closed under intersection of two members and under difference.

Facts & Assumptions

Given: A natural number $n \geq 1$ and the family $E_{n}$ of finite unions of half-open boxes in $R^{n}$ .

[L1]

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}$ ; at $m = 0$ the union is empty, so $\emptyset \in E_{n}$ ; at $m = 1$ every half-open box is elementary, $R^{n} = (- \infty, + \infty]^{n}$ included (Elementary sets: the finite unions of half-open boxes in $R^{n}$ ).

[L2]

The intersection of the members of a finite list of half-open boxes is a half-open box, the empty list giving $R^{n}$ (Half-open boxes are closed under intersection, and the complement of a half-open box is a finite disjoint union of half-open boxes).

[L3]

For every parameter pair $(a, b)$ there is a finite list of pairwise disjoint half-open boxes whose union is $R^{n} ∖ B (a, b)$ (Half-open boxes are closed under intersection, and the complement of a half-open box is a finite disjoint union of half-open boxes).

[F1]

An algebra of subsets of $X$ is a family $A \subseteq P (X)$ such that $\emptyset \in A$ ; if $A \in A$ , then $X ∖ A \in A$ ; and if $A, B \in A$ , then $A \cup B \in A$ (Algebras of subsets).

[F2]

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

Proof

technique · direct

1.1

The empty list of boxes has union $\emptyset$ and the one-member list $B$ has union $B$ , so $\emptyset \in E_{n}$ , every half-open box lies in $E_{n}$ , and $R^{n} \in E_{n}$ .

1.2

If $E = ⋃_{j < m} B_{j}$ and $F = ⋃_{k < p} C_{k}$ are presentations, then concatenating the two lists into a list of length $m + p$ presents $E \cup F$ , so $E_{n}$ is closed under the union of two members.

1.3

With the same presentations, $E \cap F = ⋃_{j < m} ⋃_{k < p} (B_{j} \cap C_{k})$ , each $B_{j} \cap C_{k}$ is a half-open box, and the $m p$ boxes can be listed by a bijection of ${q \in N : q < m p}$ with the pairs $(j, k)$ , so $E \cap F \in E_{n}$ .

L1L2F2algebra

1.4

The complement of a single half-open box is a finite union of half-open boxes, hence lies in $E_{n}$ .

L3L1

2.1

For a presentation $E = ⋃_{j < m} B_{j}$ one has $R^{n} ∖ E = ⋂_{j < m} (R^{n} ∖ B_{j})$ ; putting $F_{0} : = R^{n}$ and $F_{q + 1} : = F_{q} \cap (R^{n} ∖ B_{q})$ , an induction on $q \leq m$ using step 1.1 for $F_{0}$ and steps 1.3 and 1.4 for the successor case gives $F_{q} \in E_{n}$ for every $q \leq m$ , and $F_{m} = R^{n} ∖ E$ .

step 1.1step 1.3step 1.4algebra

3.1

Steps 1.1, 1.2 and 2.1 are the three clauses of [F1], so $E_{n}$ is an algebra of subsets of $R^{n}$ ; it contains every half-open box by step 1.1, is closed under binary intersection by step 1.3, and is closed under difference because $E ∖ F = E \cap (R^{n} ∖ F)$ .

step 1.1step 1.2step 1.3step 2.1F1∎

Depends on

Used by

Dependency tree · two levels

10 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)

The elementary sets form an algebra of subsets of RnRn containing every half-open box