Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01
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.

Subsets and countable unions of null subsets of Rm are null

Statement

Every subset of a null subset of Rm is null. Assuming countable choice, every countable union of null subsets of Rm is null.

Facts & Assumptions

Given: Null sets Ej, j∈N.

[L2]

Countable choice selects one cover for each Ej (The Axiom of Countable Choice (ACω)), and N2 is countable (N×N≈N).

Proof

technique · constructive
1.1

Subset closure follows because any cover of a set covers every subset.

L1
1.2

Given ε>0, choose for each j a cube cover of Ej with total volume at most ε2−j−1. This simultaneous selection uses [L2].

L1L2L3construct
2.1

Enumerate the doubly indexed cubes through a bijection N→N2. Every finite partial sum is contained in a finite rectangle of indices and is at most ∑jε2−j−1≤ε.

step 1.2L2L3given
3.1

By [L4], the enumerated nonnegative volume series converges with sum at most ε. The cubes cover ⋃jEj, proving nullity.

step 2.1L1L4discharge-construct∎

Depends on

Used by

Dependency tree · two levels

72 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