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.
Completeness, regular opens, and order continuity
Definition
A Boolean algebra is complete, or Dedekind complete, if every subset has a least upper bound . Complements then give greatest lower bounds by . The empty bounds are and . The one-element Boolean algebra is allowed.
For a topological space , is the union of the open subsets of , and is the intersection of the closed subsets containing . An open set is regular open if . Write for the set of regular open subsets, ordered by inclusion. Its proposed operations, justified by Regular open algebra in ZF ↗, are
Here the empty union is and the empty intersection is ; finite meets will be ordinary finite intersections, and the bounds will be . No separation axiom on is assumed.
A Boolean homomorphism is order-continuous if it preserves every supremum and infimum that exists in : whenever exists, , and likewise for infima. This includes empty families. An order-dense Boolean embedding is an injective Boolean homomorphism such that each has some with . A Boolean completion is such an embedding into a complete Boolean algebra. This definition asserts neither existence of a completion nor extension of a homomorphism.
Depends on
Used by
- Boolean-valued semantics for names Definition
- Shelah sweetness models for forcing Definition
- The Good-Tree-Watson symmetric Stone model Definition
- The Suslin Hypothesis and Suslin algebras Definition
- Dense-equivalent forcing presentations Example
- Generic Boolean filters select ground-model joins Lemma
- Probability algebras, arbitrary joins and the countable chain condition Lemma
- Sweet density transfers along complete suborders Lemma
- Orientation for intermediate models and complete subalgebras Remark
- Completeness, extremal disconnectedness, and regular-open clopens Theorem
- Order-continuous Boolean homomorphisms extend uniquely to completions Theorem
- Regular open algebra in ZF Theorem
- Sweet amalgamation extends partial Boolean isomorphisms Theorem
Dependency tree · two levels
6 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
- Fremlin, Measure Theory, 313H–313L and 314O–314P, Chapter 31, pp. 25–27 and 37–38 (standard reference, not scraped)