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.
and subsets of a topological space, agreeing with the real-line notion
Definition
Let be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let .
- is a set of when there is a sequence of open subsets of with
- is an set of when there is a sequence of closed subsets of with
As everywhere in this library contains , so both indexings start at . An at most countable family may always be presented as a sequence (Finite, countably infinite, countable, uncountable): a finite list is extended by for , which changes neither the intersection nor the union, so nothing is lost by indexing over .
The two classes are exchanged by complementation. is in if and only if is in . If with each closed then by De Morgan and each is open (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison); the converse is the same computation read backwards.
Every open set is and every closed set is , by the constant sequence , respectively . Neither converse holds, and with its usual topology already refutes both. The singleton is a that is not open: it is , since lies in every one of those intervals while a real is excluded at some index, the Archimedean property giving a natural with and being a successor (For every in a complete ordered field there is a natural with , Every nonzero natural number is a successor, The canonical natural of a field); and is not open because every bounded open interval with contains the point (Intervals of : the nine order-convex forms, nondegeneracy, and length, The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded, claim 3). Complementing, is an that is not closed, its complement not being open.
The condition that is a real restriction is the other pairing, namely that every closed set be a , equivalently that every open set be an . That is not automatic in an arbitrary space, and it is exactly the second conjunct of perfect normality later on this page. It must not be confused with the two automatic inclusions above: they hold everywhere and say nothing about a space.
Agreement with the real-line notion, stated because a second notion of the same name would be a defect. and subsets of defines and subsets of by the same two displayed conditions, with "open" and "closed" read in the sense of Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen. Those two words name the same two collections of subsets of as the usual topology of does, and the verification is one line of unfolding. Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen calls open when every admits with , where (The -neighbourhood and the punctured -neighbourhood of a point of ); The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement calls open in when every admits with , and by claim 2 of The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded. The two conditions are therefore the same condition word for word, so the two collections of open subsets of are one collection, and hence so are the two collections of closed subsets, each being the complements of the other collection. The usual topology of is the metric topology of (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not). Since the two definitions quantify over one collection of open sets and one collection of closed sets, a subset of is in the sense above, for with its usual topology, if and only if it is in the sense of and subsets of ; and likewise for . There is one notion here, not two, and every statement proved about or subsets of elsewhere in this library may be quoted verbatim as a statement about the topological space .
Remarks
-
The letters. for ferme with for somme, for Gebiet with for Durchschnitt, as and subsets of records.
-
Neither class is closed under complementation, which is why both names are needed; and neither is a topology, an arbitrary union of sets being no longer in general. What is true, and all that is used on this page, is the complementation duality above together with the fact that a finite intersection of sets and a finite union of sets stay in their class, by rearranging a finite array of sequences.
-
In a metric space every closed set is . That is proved later on this page from the distance function, and it is the reason every metrizable space is perfectly normal. In a general space it can fail, so it is a genuine hypothesis and not a convenience.
Depends on
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
Finite, countably infinite, countable, uncountable
and subsets of
Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
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
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded
Intervals of : the nine order-convex forms, nondegeneracy, and length
The canonical natural of a field
For every in a complete ordered field there is a natural with
Every nonzero natural number is a successor