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.
Equivalent forms of the Baire property
Statement
For a topological space , the following are equivalent: every countable intersection of dense open sets is dense; every countable union of closed sets with empty interior has empty interior; no nonempty open subset is meagre in ; and every residual subset meets every nonempty open set. The equivalence includes the empty space.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a topological space and let . The set is nowhere dense when (def-interior-closure-boundary-top). It is meagre when there is a sequence of nowhere dense subsets of with . It is residual, or comeagre, when is meagre. The empty union shows that is meagre, including when . (Nowhere dense, meagre, residual, and comeagre subsets of a topological space).
A topological space (def-topological-space) is a Baire space when for every sequence of subsets of that are open and dense in (def-dense-top, def-sequence-convergence-top, def-natural-numbers), the intersection is dense in . (Baire space: a topological space in which every countable intersection of dense open subsets is dense).
For all sets , and , Let be a set with . Then is a nonempty set and ( and ; and for a nonempty set , and ).
Proof
Apply complements and De Morgan's laws to pass between dense intersections of open sets and unions of closed nowhere dense sets.
Then localise to a nonempty open set to prove equivalence with no nonempty open subset being meagre; keep the empty-space convention visible.
The preceding construction and implications establish the assertion.
Depends on
- Nowhere dense, meagre, residual, and comeagre subsets of a topological space
- Baire space: a topological space in which every countable intersection of dense open subsets is dense
- $X \setminus (a \cup b) = (X \setminus a) \cap (X \setminus b)$ and $X \setminus (a \cap b) = (X \setminus a) \cup (X \setminus b)$; and for a nonempty set $F$, $X \setminus \bigcup F = \bigcap \{\, X \setminus a : a \in F \,\}$ and $X \setminus \bigcap F = \bigcup \{\, X \setminus a : a \in F \,\}$
Used by
- FALSE: the rational numbers form a Baire space False statement
- Open subspaces and residual subspaces of Baire spaces are Baire Proposition
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 41 results over 13 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
- David Marker, Descriptive Set Theory, §§1–2 (standard reference, not scraped)
- Michael Kunzinger, General Topology, §§11.3–11.4 (standard reference, not scraped)
- MFF General Topology course summary, §4.3 (standard reference, not scraped)
- Jesse Peterson, Real Analysis, §§3.6–3.7 (standard reference, not scraped)