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.
Baire space: a topological space in which every countable intersection of dense open subsets is dense
Definition
A topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) is a Baire space when
for every sequence of subsets of that are open and dense in (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure, The natural numbers (von Neumann)), the intersection is dense in .
As everywhere in this library contains , so the sequence starts at and an index range copied from a text that starts at must be shifted before it is used here.
The condition unwound. Denseness of says (Interior, closure, boundary, exterior, derived set and isolated point in a topological space), equivalently that meets every nonempty open subset of (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets). So the Baire condition reads:
for every sequence of dense open sets and every nonempty open there is a point of lying in every .
That is the form every proof below uses, and it is the form in which the condition is checked: one produces a single point, in a given nonempty open set, belonging to all of the at once.
The intersection itself need not be open. Nothing in the definition asserts that is open, and in general it is not; what is asserted is only that it is dense. A finite intersection of dense open sets is dense and open, and that much holds in every space; the content of the definition is entirely in the passage to a countable family.
Why the meager formulation is not given here. The usual equivalent phrasing says that a countable union of nowhere dense sets has empty interior, or that a nonempty open set is not meager. This page does not state it, because the notions of nowhere dense and meager available to it are Nowhere dense, meager (first category), residual, and second category subsets of , which is stated for subsets of and not for subsets of an arbitrary topological space; restating them here in general would create a second notion under the same name. The definition above is stated in terms of denseness alone, which Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets does define for an arbitrary space, and it is equivalent to the meager formulation wherever both are available.
Remarks
What the definition is for. It isolates exactly the hypothesis under which a countable family of "large" open sets still has a large intersection, and that is the hypothesis a great many existence arguments run on: to produce an object with countably many properties, one shows that each property is enjoyed by a dense open set and then takes a point of the intersection. Nothing about the ambient space is assumed here beyond the definition, so the notion applies to spaces with no metric and no countability property.
Which spaces satisfy it, and at what cost. Every locally compact Hausdorff space is a Baire space, assuming dependent choice (Assuming dependent choice, every locally compact Hausdorff space is a Baire space); the corresponding statement for complete metric spaces, and the exact choice principles the several versions of the Baire category theorem are equivalent to over ZF, are recorded in The Baire category theorem is four inequivalent statements over ZF ‡, which this library states and does not prove.
Depends on
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets
- Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure
- Interior, closure, boundary, exterior, derived set and isolated point in a topological space
- The natural numbers $\mathbb{N}$ (von Neumann)
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 56 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Baire space (Wikipedia) (standard reference, not scraped)
- Baire category theorem (Wikipedia) (standard reference, not scraped)