Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)verified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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 (X,T)(X, \mathcal{T}) (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 (Un)nN(U_n)_{n \in \mathbb{N}} of subsets of XX that are open and dense in XX (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 N\mathbb{N} (von Neumann)), the intersection nNUn\bigcap_{n \in \mathbb{N}} U_n is dense in XX.

As everywhere in this library N\mathbb{N} contains 00, so the sequence starts at U0U_0 and an index range copied from a text that starts at 11 must be shifted before it is used here.

The condition unwound. Denseness of AXA \subseteq X says A=X\overline{A} = X (Interior, closure, boundary, exterior, derived set and isolated point in a topological space), equivalently that AA meets every nonempty open subset of XX (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 (Un)(U_n) of dense open sets and every nonempty open WXW \subseteq X there is a point of WW lying in every UnU_n.

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 UnU_n at once.

The intersection itself need not be open. Nothing in the definition asserts that nUn\bigcap_n U_n 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 R\mathbb{R}, which is stated for subsets of R\mathbb{R} 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

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