Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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 sigma-algebra with a listed infinite subfamily contains a disjoint sequence of nonempty members

Statement

Let A be a sigma-algebra on X. If there is an injective sequence e:N→A, then there is a sequence (Dn)n∈N of pairwise disjoint nonempty members of A.

Facts & Assumptions

Given: A sigma-algebra A on X and an injective sequence e:N→A.

[L1]

A sigma-algebra is closed under complements and countable unions, hence under finite Boolean operations (Sigma-algebras).

[L2]

A countably infinite set admits a bijective listing by N (Finite, countably infinite, countable, uncountable).

[L3]

A seed and a function determine a sequence by recursion on N (The recursion theorem).

Proof

technique · constructive
1.1givenL1L2construct

Let B be the Boolean algebra generated by the sets e(n). Finite Boolean expressions can be coded by natural numbers, so deleting repeated values in least-code order gives a listing of B. It is infinite because it contains the distinct sets e(n).

2.1step 1.1L1L3construct

Call a nonempty B∈B an atom when it has no nonempty proper member in B. If B has infinitely many atoms, list them in least-code order. Otherwise let R0 be the complement of the union of its finitely many atoms. This complement is nonempty: if the atoms covered X, then intersecting any member of B with each atom would show that every member is a union of those finitely many atoms, contradicting that B is infinite. The set R0 contains no atom. Given nonempty atomless Rn∈B, take the least listed B that splits it, put Dn:=Rn∩B and Rn+1:=Rn∖B, and use [L3] to continue. Both new sets are nonempty by the choice of B.

3.1step 2.1discharge-construct∎

In the first case the listed atoms are pairwise disjoint nonempty members of A. In the second, each Dn⊆Rn is nonempty, Rn+1 is disjoint from Dn, and all later Dm lie in Rn+1; hence the Dn are pairwise disjoint members of A. This constructs the required sequence without a choice principle.

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