Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Regular open algebra in ZF

Statement

In ZF, for every topological space X, the operations in the regular-open definition make RO⁡(X) a complete Boolean algebra. Its order is inclusion, finite meets are intersections, and its bounds are ∅,X. The displayed formulas apply to empty as well as nonempty families, and X may be empty.

Facts & Assumptions

[F1]

Completeness, regular opens, and order continuity defines regular opens, their proposed operations, completeness, interior and closure.

[F2]

Quotient operations are well defined makes the quotient of a Boolean algebra by an ideal a Boolean algebra, identifying two elements exactly when their symmetric difference is in the ideal.

Proof

Given: A topological space X; all arguments take place in ZF.

1.1F1algebra

Put r(E)=int⁡E‾. This is regular open for any E⊆X: r(E) is open and contained in the closed set E‾, so r(E)⊆r(r(E))⊆int⁡E‾=r(E). Call N nowhere dense if int⁡N‾=∅. These sets form an ideal N of subsets: the empty set qualifies; subsets qualify by monotonicity; and if N,M qualify, any nonempty open W has a nonempty open part W∖N‾, which in turn has a nonempty open part outside M‾. Thus no nonempty open set lies in N‾∪M‾=N∪M‾, proving the finite-union condition. A nowhere-dense set contains no nonempty open set.

2.1step 1.1algebra

For E⊆X put ∂E=E‾∖int⁡E, and let A={E⊆X:∂E∈N}. The identities ∂(X∖E)=∂E and ∂(E∪F)⊆∂E∪∂F follow respectively from X∖E‾=X∖int⁡E and the closure/interior union inclusions. They and ∂∅=∅ show that A is closed under complements and finite unions, hence all finite set Boolean operations. It is therefore a Boolean algebra with those operations. If N∈N, then int⁡N=∅ and ∂N=N‾ is nowhere dense, so N⊆A and is an ideal of it. Every open U belongs to A: its closed boundary U‾∖U contains no nonempty open W, since W⊆U‾ would force W∩U≠∅.

3.1step 1.1step 2.1algebra

For E∈A, int⁡E⊆r(E)⊆E‾ gives E△r(E)⊆∂E∈N. Also r(E)∈A by openness. If regular opens U,V differ by a nowhere-dense set, the open set U∖V‾ is a subset of that difference, so it is empty by step 1.1. Hence U⊆V‾, and openness gives U⊆int⁡V‾=V. Interchanging U,V gives equality. More generally if both U and V differ from E by nowhere-dense sets, then U△V⊆(U△E)∪(E△V) is nowhere dense, so this uniqueness applies. Thus every class of A/N has exactly one regular-open representative, namely r(E).

4.1F1F2step 2.1step 3.1algebra

F2 and step 3.1 transport a Boolean algebra structure to RO⁡(X). To identify its operations, first U∩V is regular: monotonicity gives r(U∩V)⊆r(U)∩r(V)=U∩V, and the reverse inclusion follows from openness. Thus the transported meet is U∩V. The transported join is r(U∪V), the representative of its set-theoretic union class. For the complement put W=int⁡(X∖U)=X∖U‾. Since W⊆X∖U and that latter set is closed, r(W)⊆int⁡(X∖U)=W; openness gives equality. Also (X∖U)△W=U‾∖U is nowhere dense by step 2.1, so W is the required complement representative. Bounds transport to ∅,X, which are regular. The transported order satisfies U≤V iff U∩V=U iff U⊆V. In particular all distributive and complement laws hold by F2, rather than by a claim that regular opens are closed under ordinary unions.

5.1F1step 1.1step 4.1algebra

For any U⊆RO⁡(X), J=r(⋃U) is regular by step 1.1 and contains each U∈U, since those sets are open subsets of ⋃U‾. If a regular open V contains each U, monotonicity gives J⊆r(V)=V, proving it is the least upper bound. Put M=int⁡⋂U. For every U∈U, r(M)⊆r(U)=U. Since r(M) is open, it follows that r(M)⊆int⁡⋂U=M; the reverse holds because M is open. Thus M is regular. Any regular-open lower bound is an open subset of ⋂U, hence lies in M, so M is the greatest lower bound. If U is empty, these formulas give J=r(∅)=∅ and M=int⁡X=X, directly verifying both bounds. If X=∅ there is just the one regular open ∅=X, and the same proof gives the trivial complete Boolean algebra. No countable union of nowhere-dense sets or choice principle has been used. QED.

Depends on

Dependency tree · 2 levels

Sources