Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicable
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) (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)n∈N of subsets of X that are open and dense in X (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 (von Neumann)), the intersection ⋂n∈NUn is dense in X.

As everywhere in this library N contains 0, so the sequence starts at U0 and an index range copied from a text that starts at 1 must be shifted before it is used here.

The condition unwound. Denseness of A⊆X says A‾=X (Interior, closure, boundary, exterior, derived set and isolated point in a topological space), equivalently that A meets every nonempty open subset of X (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) of dense open sets and every nonempty open W⊆X there is a point of W lying in every Un.

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

The intersection itself need not be open. Nothing in the definition asserts that ⋂nUn 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, which is stated for subsets of 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 under dependent choice (Assuming dependent choice, every locally compact Hausdorff space is a Baire space). The later Separable complete metric spaces are Baire in ZF ↗ proves the separable complete-metric case without choice, by selecting least indices from one fixed dense sequence; Dependent Choice is equivalent to the complete-metric Baire principle over ZF ↗ proves the equivalence of the unrestricted complete-metric principle with DC over ZF.

Depends on

Dependency tree · 2 levels

Sources