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$ ,

$m_{X} (A) = σ_{X} (A) .$

Facts & Assumptions

Given: An algebra $A$ on $X$ and $M : = m_{X} (A)$ .

[L1]

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

[L2]

The family $M$ is closed under complements (The monotone class generated by an algebra is closed under complements) and binary intersections (The monotone class generated by an algebra is closed under finite intersections).

[L3]

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

[L4]

The family $σ_{X} (A)$ is the smallest sigma-algebra containing $A$ (Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal).

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 \subseteq σ_{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) \subseteq M$ .

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources