Baire theorem
In a complete metric space, a countable intersection of dense open subsets is dense.
The good concept underlying the theorem is that of a Gδ set, i.e., a countable intersection of open sets. Then Baire theorem can also be formulated as the fact that a countable intersection of dense Gδ sets is a dense Gδ set. We prove Baire theorem, giving several different formulations that can be handy. We also prove the important consequence that, if the space is covered by a countable union of closed sets, then the union of their interiors is dense.
The names of the theorems do not contain the string "Baire", but are instead built from the form of the statement. "Baire" is however in the docstring of all the theorems, to facilitate grep searches.
We also define the filter residual α generated by dense Gδ sets and prove that this filter
has the countable intersection property.
An open set is a Gδ set.
The union of two Gδ sets is a Gδ set.
A set s is called residual if it includes a dense Gδ set. If α is a Baire space
(e.g., a complete metric space), then residual sets form a filter, see mem_residual.
For technical reasons we define the filter residual in any topological space
but in a non-Baire space it is not useful because it may contain some non-residual
sets.
Baire theorem: a countable intersection of dense open sets is dense. Formulated here when
the source space is ℕ (and subsumed below by dense_Inter_of_open working with any
encodable source space).
Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀.
Baire theorem: a countable intersection of dense open sets is dense. Formulated here with an index set which is a countable set in any type.
Baire theorem: a countable intersection of dense open sets is dense. Formulated here with an index set which is an encodable type.
Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with ⋂₀.
Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with an index set which is an encodable type.
Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with an index set which is a countable set in any type.
A property holds on a residual (comeagre) set if and only if it holds on some dense Gδ set.
A set is residual (comeagre) if and only if it includes a dense Gδ set.
Equations
Baire theorem: if countably many closed sets cover the whole space, then their interiors are dense. Formulated here with an index set which is a countable set in any type.
Baire theorem: if countably many closed sets cover the whole space, then their interiors
are dense. Formulated here with ⋃₀.
Baire theorem: if countably many closed sets cover the whole space, then their interiors are dense. Formulated here with an index set which is an encodable type.
One of the most useful consequences of Baire theorem: if a countable union of closed sets covers the space, then one of the sets has nonempty interior.