# Baire spaces #

A topological space is called a *Baire space*
if a countable intersection of dense open subsets is dense.
Baire theorems say that all completely metrizable spaces
and all locally compact regular spaces are Baire spaces.
We prove the theorems in `Mathlib/Topology/Baire/CompleteMetrizable`

and `Mathlib/Topology/Baire/LocallyCompactRegular`

.

In this file we prove various corollaries of Baire theorems.

The good concept underlying the theorems 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 deduce this version from Baire property. 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.

We also prove that in Baire spaces, the `residual`

sets are exactly those containing a dense Gδ set.

Definition of a Baire 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 a countable type.

A set is residual (comeagre) if and only if it includes a dense `Gδ`

set.

A property holds on a residual (comeagre) set if and only if it holds on some dense `Gδ`

set.

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 a countable 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.

Baire theorem: the intersection of two dense Gδ sets is dense.

If a countable family of closed sets cover a dense `Gδ`

set, then the union of their interiors
is dense. Formulated here with `⋃`

.

If a countable family of closed sets cover a dense `Gδ`

set, then the union of their interiors
is dense. Formulated here with a union over a countable set in any type.

If a countable family of closed sets cover a dense `Gδ`

set, then the union of their interiors
is 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 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 a countable 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.