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 be a sigma-algebra on . If there is an injective sequence , then there is a sequence of pairwise disjoint nonempty members of .
Facts & Assumptions
Given: A sigma-algebra on and an injective sequence .
A sigma-algebra is closed under complements and countable unions, hence under finite Boolean operations (Sigma-algebras).
A countably infinite set admits a bijective listing by (Finite, countably infinite, countable, uncountable).
A seed and a function determine a sequence by recursion on (The recursion theorem).
Proof
Let be the Boolean algebra generated by the sets . Finite Boolean expressions can be coded by natural numbers, so deleting repeated values in least-code order gives a listing of . It is infinite because it contains the distinct sets .
Call a nonempty an atom when it has no nonempty proper member in . If has infinitely many atoms, list them in least-code order. Otherwise let be the complement of the union of its finitely many atoms. This complement is nonempty: if the atoms covered , then intersecting any member of with each atom would show that every member is a union of those finitely many atoms, contradicting that is infinite. The set contains no atom. Given nonempty atomless , take the least listed that splits it, put and , and use [L3] to continue. Both new sets are nonempty by the choice of .
In the first case the listed atoms are pairwise disjoint nonempty members of . In the second, each is nonempty, is disjoint from , and all later lie in ; hence the are pairwise disjoint members of . This constructs the required sequence without a choice principle.
Depends on
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 26 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- R. F. Bass, Real Analysis for Graduate Students, version 5.0, Exercises 2.6 and 2.8 (standard reference, not scraped)