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 family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis
Statement
Let be a set, and for write
-
is a basis for some topology on (Basis and subbasis for a topology, and the topology generated by a family of sets) if and only if
- (B1) , and
- (B2) for all and every there is with .
When (B1) and (B2) hold, that topology is unique: it is , which is also exactly the family of all unions of subfamilies of .
-
Let be an arbitrary family and let be the family of intersections of finitely many members of . Then satisfies (B1) and (B2), and , the topology generated by . So the finite intersections of any subbasis form a basis for the topology it generates.
The nullary intersection: this library takes the empty intersection to be . In claim 2 the phrase "finitely many" includes none, and the intersection of the empty subfamily of is , because the defining condition "lies in every member of the empty family" holds of every point of . Hence for every , including , and no covering hypothesis is imposed on a subbasis. The competing convention takes only nonempty finite intersections and compensates by requiring ; under it claim 2 holds verbatim once that hypothesis is added, and the two conventions differ only in which of the two devices supplies (B1). The choice made here is recorded again among this page's conventions, and it is the reason comes out as the indiscrete topology rather than being undefined.
Facts & Assumptions
Given: A set ; a family and the family displayed above; a family and the family , where the value at is the empty intersection .
Topology axioms (T1) , (T2) closure under arbitrary unions, (T3) closure under binary intersections, and the fact that (T3) iterated gives every intersection of open sets (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).
is a basis for when and every is a union of members of ; equivalently, when for every and there is with (Basis and subbasis for a topology, and the topology generated by a family of sets).
is a topology on , contains , and is contained in every topology on that contains (Basis and subbasis for a topology, and the topology generated by a family of sets).
Proof
Assume (B1) and (B2).
Assume instead that is a basis for some topology on .
, being the value of the empty intersection, and , each being the intersection of the one-term list .
is closed under binary intersections: the intersection of with is the intersection of the concatenated list, again a list of finitely many members of .
always, since for and the set itself witnesses the defining condition; and every equals , since each such lies in and each lies in one of them.
Under the assumption of step 1.1: , the defining condition being vacuous, and , since by (B1) every lies in some and every subset of satisfies ; so (T1) holds for .
Under the assumption of step 1.1: if and , then for some , and membership of supplies with ; so and (T2) holds.
Under the assumption of step 1.1: if and , fix with and ; then , and (B2) supplies with , so and (T3) holds.
Under the assumption of step 1.2: by (T1), so [L2] gives for each a member with , whence , which is (B1); and for the set is open by (T3), so [L2] gives for each a member with , which is (B2).
Under the assumption of step 1.2: . Indeed implies by the second form of [L2]; and conversely makes a union of members of by step 1.5, hence open by (T2).
By steps 1.3 and 1.4, satisfies (B1), since forces , and (B2), since may be taken as .
Steps 2.1, 2.2 and 2.3 make a topology on whenever (B1) and (B2) hold, and step 1.5 then makes a basis for it and identifies with the family of unions of subfamilies of ; so (B1) and (B2) are sufficient.
Step 2.4 shows (B1) and (B2) are necessary, and step 2.5 shows that any topology having as a basis equals , which is the asserted uniqueness; with step 3.1 this proves claim 1.
By step 2.6 and step 3.1 applied to , the family is a topology on with basis , and it contains by step 1.3 and step 1.5.
Let be any topology on with ; then , because by (T1) covers the empty intersection and (T3) iterated covers the intersections of members of , and hence by (T2), every member of the former being a union of members of .
By steps 4.2 and 5.1 the topology contains and is contained in every topology containing , so it is the coarsest such topology, that is ; with step 2.6 this proves claim 2.
Remarks
-
What (B1) and (B2) are not. (B2) does not say that is closed under intersections; it says only that the intersection of two members is a union of members. The basis of open intervals of satisfies (B2) outright, since an intersection of two open intervals is an open interval or empty, whereas the basis of half-open intervals of the Sorgenfrey line uses the same closure property; a basis of open balls in a metric space uses the weaker form in an essential way.
-
The subbasis clause is what makes generation computable. The definition of as an intersection of topologies says nothing about what its members look like; claim 2 says they are exactly the unions of finite intersections of members of , which is how every generated topology in this library is actually described.
-
A family may be a basis for at most one topology, but it is a subbasis for at most one as well, and the two roles differ: is a subbasis for and a basis for it exactly when already satisfies (B1) and (B2).