Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it

Statement

Let n≥1, let μ0 be elementary volume on the elementary sets En (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition, Elementary sets: the finite unions of half-open boxes in Rn), and for A∈En and a real δ>0 put

A+δ  :=  ⋃ { A+s  :  s∈Rn with ∣si∣≤δ for every i<n },

the translates being those of Translation of a subset of Rn. Then:

  1. A+δ is an elementary set, it is determined by A and δ alone, it contains A, and every point of A is an interior point of A+δ in (Rn,d2) (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it).
  2. For every real ε>0 there is m∈N with μ0(A+1/(m+1))≤μ0(A)+ε.
  3. If μ0(A)<+∞, then for every real ε>0 there are an elementary set A′ and a compact set K⊆Rn (Open cover, subcover, compact metric space, and compact subset of a metric space) with A′⊆K⊆A and μ0(A)≤μ0(A′)+ε.

Nothing in claim 1 or claim 2 depends on a presentation of A, so the assignment δ↦A+δ and the least m satisfying claim 2 are both functions of the data and involve no selection.

Facts & Assumptions

Given: A natural number n≥1, an elementary set A⊆Rn, and a real δ>0. A presentation of A is written A=⋃j<qBj with Bj=B(aj,bj) pairwise disjoint half-open boxes, and ℓij:=bij−aij when these are real.

[L1]

B(a,b):={ x∈Rn:ai<xi≤bi  for every i<n }; a box is nonempty exactly when ai<bi for every i<n; vol⁡(∅):=0; and for a nonempty box vol⁡(B):=+∞ when ai=−∞ or bi=+∞ for some i<n, and vol⁡(B):=∏i<n(bi−ai) when every ai and every bi is real (Half-open boxes in Rn and their volume).

[L2]

Every elementary set is the union of a finite list of pairwise disjoint half-open boxes, and a subset E⊆Rn is an elementary set when there are a natural number m and a list B0,…,Bm−1 of half-open boxes with E=⋃j<mBj (Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement, Elementary sets: the finite unions of half-open boxes in Rn).

[L3]

For every n≥1, there is exactly one function μ0:En→[0,+∞] whose value at A is the sum of the volumes of the members of any presentation of A by a finite list of pairwise disjoint half-open boxes (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition).

[L4]

Elementary volume is finitely additive on pairwise disjoint elementary sets, monotone, and finitely subadditive (Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra).

[F1]

The translate of E⊆Rn by a is E+a:={x+a:x∈E} (Translation of a subset of Rn).

[F2]

d2(x,y):= ∑k<n(xk−yk)2  and d∞(x,y):=max⁡{ ∣xk−yk∣:k<n } are metrics on Rn for n≥1 (Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it).

[F4]

x is an interior point of A if B(x,r)⊆A for some r, where B(x,r):={ y∈X:d(x,y)<r }, and a subset U is open in (X,d) if every x∈U has such a ball inside U (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, Open ball, closed ball and sphere in a metric space, 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).

[F5]

For reals ak≤bk (k<n) the box Q={ x∈Rn:ak≤xk≤bk for every k<n } is a compact subset of (Rn,d2), and a subset K⊆Rn is compact if and only if K is closed in Rn and bounded (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, claims 1 and 2; Axis-parallel rectangles in Rm and their volume).

[F6]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).

[F7]

If n≥1 and U0,…,Un−1 are open, then U0∩⋯∩Un−1 is open (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, claim 3).

[F8]

A is bounded if A=∅ or there are x0∈X and a real r>0 with A⊆B(x0,r) (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[F9]

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

[F10]

For sequences of reals, ∑k<n(ak+bk)=∑k<nak+∑k<nbk; ∑k<nλak=λ∑k<nak; if ak≤bk whenever 0≤k<n then ∑k<nak≤∑k<nbk; and ∏k<n(akbk)=(∏k<nak)(∏k<nbk) (Laws of finite sums and finite products, claims 1, 2, 4 and 6).

[F11]

Finite sums and finite products of a sequence of reals are defined by the recursions Σ0=0, Σσ(n)=Σn+an and Π0=1, Πσ(n)=Πn⋅an (Finite sums and finite products, by recursion).

[F12]

For a,b∈R‾, a+b:=+∞ when a=+∞ and b≠−∞, or b=+∞ and a≠−∞; and a+b:=−∞ when a=−∞ and b≠+∞, or b=−∞ and a≠+∞ (The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined).

Proof

technique · direct
1.1F10F11algebra

For a natural number r, reals 0≤ui≤vi (i<r) and a real V≥1 with vi≤V for every i<r, one has ∏i<rvi−∏i<rui≤V r∑i<r(vi−ui): at r=0 both products are the empty product 1 and both sides are 0, and passing from r to r+1 uses ∏i<r+1vi−∏i<r+1ui=vr(∏i<rvi−∏i<rui)+(vr−ur)∏i<rui together with ∏i<rui≤V r and vr≤V, so the estimate follows by induction on r.

1.2L1L2F1F12

For a box B(a,b) and s∈Rn one has B(a,b)+s=B(a+s,b+s), where a+s is the parameter i↦ai+si, and the two boxes have the same volume; consequently, for a real δ>0, B(a,b)+δ=B(a−δ1, b+δ1) when B(a,b)≠∅ and ∅+δ=∅, and A+δ=⋃j<qBj+δ for any presentation of A, so A+δ is elementary while its definition mentions no presentation.

1.3F2F3

For x,y∈Rn and i<n one has ∣yi−xi∣≤d∞(x,y)≤d2(x,y).

1.4L1L2L3F2F8F10

If μ0(A)<+∞ then every nonempty box of a disjoint presentation of A has all parameters real, since an infinite parameter would make its volume, and hence the sum, equal to +∞. Put M:=1+∑j<qBj≠∅∑i<n(∣aij∣+∣bij∣), and M:=1 when every box is empty. Then M is a real number and every endpoint of every nonempty box has modulus at most M. Every point of a nonempty box therefore has every coordinate bounded by M, hence has Euclidean norm at most nM; thus every box lies in the ball about the origin of radius 1+nM. Therefore A is bounded and so is every subset of A.

2.1step 1.2step 1.3F1F4

For claim 1, taking s=0 gives A⊆A+δ; and if x∈A and d2(x,y)<δ then s:=y−x satisfies ∣si∣≤d2(x,y)<δ for every i<n by step 1.3, so y=x+s∈A+s⊆A+δ, whence the ball B(x,δ) of (Rn,d2) lies in A+δ and x is an interior point of it.

2.2step 1.1step 1.2L1L3L4F10

For claim 2, if μ0(A)=+∞ the inequality holds with m=0; otherwise fix a disjoint presentation, let V≥1 be a real with ℓij+2≤V for every nonempty Bj and every i<n, and let 0<δ≤1: finite subadditivity and step 1.2 give μ0(A+δ)≤∑j<qvol⁡(Bj+δ), an empty Bj contributing 0 and a nonempty one contributing ∏i<n(ℓij+2δ), so step 1.1 applied with vi=ℓij+2δ and ui=ℓij bounds each term by vol⁡(Bj)+2nV nδ and hence μ0(A+δ)≤μ0(A)+2nqV nδ.

3.1step 1.1step 1.4L1L3L4F5F6F7F8F10

For claim 3, assume μ0(A)<+∞, fix a disjoint presentation with all parameters of the nonempty Bj real by step 1.4, and define ℓij=bij−aij for nonempty Bj and ℓij=0 for empty Bj. Let V be as in step 2.2, let 0<δ≤1, and put Bj−δ:=B(aj+δ1, bj−δ1) for nonempty Bj and Bj−δ:=∅ otherwise, A′:=⋃j<qBj−δ and K:=⋃{ [aj+δ1, bj−δ1]:j<q and Bj≠∅ and aij+δ≤bij−δ for every i<n }: then A′⊆K⊆A, each listed closed rectangle is compact and hence closed, a finite union of closed sets is closed by complementation, K is bounded because K⊆A, so K is compact; and vol⁡(Bj−δ)=∏i<nmax⁡{ℓij−2δ, 0} in both the empty and the nonempty case, so step 1.1 applied with vi=ℓij and ui=max⁡{ℓij−2δ,0}, whose difference is at most 2δ, gives μ0(A)≤μ0(A′)+2nqV nδ.

4.1step 2.1step 2.2step 3.1F9∎

Given a real ε>0, apply [F9] to the positive real ε/(2nqV n+1) to obtain k≥1 with 1/k<ε/(2nqV n+1), and put m:=k−1, so that δ:=1/(m+1)=1/k satisfies 0<δ≤1 and 2nqV nδ≤ε; steps 2.2 and 3.1 then give claims 2 and 3, and step 2.1 gives claim 1.

Depends on

Dependency tree · 2 levels

Sources