A Gδ set is a countable intersection of open sets.

An open set is a Gδ set.

A countable intersection of Gδ sets is a Gδ set.

The union of two Gδ sets is a Gδ set.

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 a countable set in any type.

Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with an index set which is an encodable type.

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.