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.
Arbitrary unions and finite intersections of open subsets of are open, and dually for closed sets
Statement
Let open and closed subsets of be as in Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen.
- Arbitrary unions of open sets are open. If is any family of open subsets of , then is open.
- Finite intersections of open sets are open. If and are open, then is open.
- Arbitrary intersections of closed sets are closed. If is a nonempty family of closed subsets of , then is closed.
- Finite unions of closed sets are closed. If and are closed, then is closed.
The word finite in claims 2 and 4 is not decoration: an arbitrary intersection of open sets need not be open, and dually an arbitrary union of closed sets need not be closed; the remarks below say where that is settled. Claim 3 asks to be nonempty only so that is a subset of without appeal to a convention about the empty intersection.
Facts & Assumptions
Given: A family of open subsets of , with ; a natural number and open sets ; a nonempty family of closed subsets of , with ; and closed sets .
De Morgan's laws in the ambient set theory: for a nonempty family of subsets of , , and . Also .
is open when every admits a real with ; is closed when is open (Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen).
Every nonempty finite set of reals has a minimum, so is defined and equals one of the two entries, and is both (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).
Proof
Let . Then for some , and is open, so there is with ; as was arbitrary, is open, which is claim 1.
Now let and be open and let ; fix with and with .
Put , which is one of and hence , and satisfies and ; then and , so , and as was arbitrary is open.
The family consists of open sets by [L1], so its union is open by step 1.1; that union is by [A1], so is closed, which is claim 3.
Claim 2 now follows by induction on : for the intersection is , which is open by hypothesis; and if is open then is an intersection of two open sets, hence open by step 2.1.
Each is open by [L1], so is open by step 3.1; that set is by [A1], so is closed, which is claim 4.
Claims 1, 2, 3 and 4 are steps 1.1, 3.1, 2.2 and 4.1 respectively, so arbitrary unions and finite intersections of open sets are open, and arbitrary intersections and finite unions of closed sets are closed.
Remarks
-
Completeness plays no part. Nothing above uses the least-upper-bound property, or even the Archimedean property: the only facts about the proof touches are the definition of a neighbourhood, its monotonicity in the radius, and the comparison of two positive radii. What needs completeness is not the algebra of open sets but the theorems about compactness that come later.
-
Why finiteness cannot be dropped in claim 2. The minimum taken in step 2.1 is a minimum of finitely many positive radii, and it is positive precisely because it is one of them (Every nonempty finite set of reals has a maximum and a minimum). An infinite family of positive radii has an infimum that may be , and then no positive survives. That is exactly what happens for the shrinking intervals of FALSE: an arbitrary intersection of open subsets of is open, whose named witness is is not open ↗.
-
The four claims are a rewriting of two. Claims 3 and 4 are claims 1 and 2 read through complementation, and closedness is defined by complementation (Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen), so no separate argument about closed sets is possible or needed.
Depends on
Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen
The -neighbourhood and the punctured -neighbourhood of a point of
Every nonempty finite set of reals has a maximum and a minimum
Maximum and minimum of a set
Intervals of : the nine order-convex forms, nondegeneracy, and length
Complete ordered field (least-upper-bound property)
Ordered field