LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 countable algebra cover disjointifies inside the covered algebra set

Statement

Let $A_{0}$ be an algebra on $X$ , let $A \in A_{0}$ , and let $(A_{k})_{k \in N}$ be a sequence in $A_{0}$ with $A \subseteq ⋃_{k} A_{k}$ . Then there are pairwise disjoint $B_{k} \in A_{0}$ such that $A = ⋃_{k} B_{k}$ and $B_{k} \subseteq A_{k}$ for every $k$ . Equivalently: every countable algebra cover of an algebra set disjointifies inside that set into algebra members subordinate to the original cover.

Facts & Assumptions

Given: The algebra $A_{0}$ , the covered set $A$ , and the cover $(A_{k})$ from the Statement.

[F1]

An algebra of subsets of $X$ contains $\emptyset$ and is closed under complements and binary unions; consequently it is closed under finite unions, finite intersections, and differences. (Algebras of subsets)

Proof

technique · constructive

1.1F1construct

Define $B_{k} : = A \cap (A_{k} ∖ ⋃_{j < k} A_{j})$ , using the empty preceding union when $k = 0$ ; finite unions, differences, and intersections keep every $B_{k}$ in $A_{0}$ , and $B_{k} \subseteq A_{k}$ .

2.1step 1.1algebradischarge-construct∎

Distinct pieces are disjoint because a point in $B_{k}$ belongs to no earlier $A_{j}$ ; every $x \in A$ lies in some $A_{k}$ , and at its least such index it belongs to $B_{k}$ , so $A = ⋃_{k} B_{k}$ .

Depends on

Algebras of subsets

Used by

Dependency tree · one level

1 result within one dependency step 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

G. Folland, Real Analysis, 2nd ed., proof of Proposition 1.13(a) (standard reference, not scraped)