Alphabeta Math
TheoremStatement: 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.

A linear map T of Rn sends Lebesgue measurable sets to Lebesgue measurable sets, with λn(T[E])=∣det⁡T∣ λn(E) when T is invertible and T[E] Lebesgue null when it is not

Statement

Let n≥1, assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)) and let T:Rn→Rn be linear with matrix A (Linear map between vector spaces over the same field, Every Euclidean linear map has a unique matrix and satisfies ∥Lh∥2≤K∥h∥2 for some K≥0).

  1. Invertible case. If det⁡A≠0, then T[E] is Lebesgue measurable for every Lebesgue measurable E and λn(T[E])  =  ∣det⁡A∣  λn(E), both sides possibly +∞; the product is defined in R‾ because ∣det⁡A∣>0.
  2. Singular case. If det⁡A=0, then T[E] is Lebesgue measurable with λn(T[E])=0 for every E⊆Rn.

The singular clause is stated as nullity and not as a product. When det⁡A=0 and λn(E)=+∞ the expression ∣det⁡A∣ λn(E) is 0⋅(+∞), which The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined leaves undefined; writing the conclusion as λn(T[E])=0 says the same thing wherever the product is defined and remains a statement where it is not.

Facts & Assumptions

Given: A natural number n≥1, the Axiom of Countable Choice, a linear map T of Rn with matrix A, and a set E⊆Rn.

[L1]

An invertible linear map carries Borel sets to Borel sets, and there is a strictly positive real c(T)=λn(T[(0,1]n]) with λn(T[E])=c(T)λn(E) for every Borel E, with c(S∘T)=c(S)c(T) and c(id)=1 (An invertible linear map of Rn scales the Lebesgue measure of every Borel set by a positive constant depending only on the map).

[L2]

λn(Dp(c)[(0,1]n])=∣c∣=∣det⁡Dp(c)∣ and λn(Epq[(0,1]n])=1=∣det⁡Epq∣ (A coordinate scaling and a coordinate transposition send the unit cube to a set of measure equal to the absolute value of the determinant).

[L3]

For n≥2 a shear satisfies λn(Tij(t)[(0,1]n])=1=∣det⁡Tij(t)∣ (A shear sends the unit cube to a set of Lebesgue measure one).

[L4]

Every proper linear subspace W⊊Rn is Lebesgue measurable with λn(W)=0 (Every affine hyperplane of Rn, and hence every proper linear subspace, is Lebesgue null).

[L5]

A Lipschitz self-map of Rn carries a set of Lebesgue outer measure zero to a Lebesgue measurable set of measure zero (A Lipschitz self-map of Rn carries Lebesgue null sets to Lebesgue null sets, Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction).

[L6]

E is Lebesgue measurable if and only if E=H∪W for an Fσ set H and a set W with λn∗(W)=0 (Assuming countable choice, four equivalent descriptions of a Lebesgue measurable subset of Rn, condition 4; Gδ and Fσ subsets of a topological space, agreeing with the real-line notion).

[F1]
[F3]

For every n≥1 and every real matrix A∈Mn(R), A is invertible if and only if det⁡(A)≠0 (A finite square real matrix is invertible if and only if its determinant is nonzero).

[F5]

For a linear map T:V→W, im⁡T:={T(v):v∈V} (Kernel and image of a linear map), and it is a linear subspace (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial).

[F6]

Every product with one factor 0 and the other ±∞ is left undefined in R‾ (The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined).

[F7]

Let S⊆N; if 0∈S and σ(n)∈S whenever n∈S, then S=N (The principle of mathematical induction).

Proof

technique · direct
1.1F2F3F4F5

Suppose det⁡A=0. Then im⁡T is a proper linear subspace of Rn: were T surjective, each standard vector ei would be T(vi) for some vi, finitely many instantiations, and the matrix B with bji:=(vi)j would satisfy (AB)ki=∑jakj(vi)j=(Tvi)k=(ei)k, so AB=In and det⁡A det⁡B=det⁡In=1, contradicting det⁡A=0.

1.2F4

T is Lipschitz, since ∥Tx−Ty∥2=∥T(x−y)∥2≤K∥x−y∥2 for a real K≥0.

1.3L1L2L3F1

Every elementary matrix M of Mn(R) satisfies c(M)=∣det⁡M∣: at n=1 the only elementary matrices are the scalings D0(c), and for n≥2 the three types are the scalings, the transpositions and the shears, whose unit-cube images have the measures ∣c∣, 1 and 1, matching ∣det⁡∣ in each case.

2.1step 1.1step 1.3L1F1F2F3F7

Suppose det⁡A≠0, so A is invertible and factors as a finite product M1⋯Mr of elementary matrices, each invertible. Multiplicativity of c and of the determinant then give c(T)=∏sc(Ms)=∏s∣det⁡Ms∣=∣det⁡A∣ by induction on r, the empty product giving c(id)=1=∣det⁡In∣.

2.2step 1.1L4L7F6

For det⁡A=0, step 1.1 makes im⁡T a proper linear subspace, hence Lebesgue null; every T[E] is a subset of it, so completeness makes T[E] Lebesgue measurable with λn(T[E])=0, which is claim 2; stating it as a product would require the undefined 0⋅(+∞) when λn(E)=+∞.

3.1step 1.2step 2.1step 2.2L1L5L6L7∎

For det⁡A≠0 and E Lebesgue measurable, write E=H∪W with H an Fσ set, hence Borel, and λn∗(W)=0; then T[E]=T[H]∪T[W], where T[H] is Borel and T[W] is Lebesgue measurable of measure 0 by step 1.2 and the Lipschitz lemma, so T[E] is measurable. Since H⊆E and E∖H⊆W, and T[H]⊆T[E] with T[E]∖T[H]⊆T[W], both pairs differ by null sets, so λn(E)=λn(H) and λn(T[E])=λn(T[H])=c(T)λn(H)=∣det⁡A∣ λn(E), which is claim 1; claim 2 is step 2.2.

Depends on

Used by

…and 16 more results.

Dependency tree · two levels

156 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