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

The monotone class generated by an algebra equals the sigma-algebra it generates

Statement

For every algebra A of subsets of X,

mX(A)=σX(A).

Facts & Assumptions

Given: An algebra A on X and M:=mX(A).

[L1]

The family M is the smallest monotone class containing A (The generated monotone class exists and is minimal).

[L3]

An algebra closed under increasing countable unions is a sigma-algebra (An algebra closed under increasing countable unions is a sigma-algebra).

[L4]

Proof

technique · direct
1.1L1L2algebra

By [L2], M contains X and is closed under complements and binary intersections, hence under finite unions; it is therefore an algebra.

1.2L1L4algebra

Every sigma-algebra is closed under increasing unions and, by De Morgan's law, decreasing intersections. Thus σX(A) is a monotone class containing A, and minimality in [L1] gives M⊆σX(A).

2.1step 1.1L1L3L4

Since M is a monotone class by [L1], it is closed under increasing countable unions. Step 1.1 and [L3] make it a sigma-algebra containing A, so [L4] gives σX(A)⊆M.

3.1step 2.1step 1.2∎

The inclusions of steps 2.1 and 1.2 prove the equality.

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