First Baire theorem

In this file we prove that a completely metrizable topological space is a Baire space. Since Mathlib does not have the notion of a completely metrizable topological space yet, we state it for a complete uniform space with countably generated uniformity filter.

instance BaireSpace.of_pseudoEMetricSpace_completeSpace {X : Type u_1} [UniformSpace X] [CompleteSpace X] [Filter.IsCountablyGenerated (uniformity X)] : BaireSpace X

First Baire theorem: a completely metrizable topological space has Baire property.

Since Mathlib does not have the notion of a completely metrizable topological space yet, we state it for a complete uniform space with countably generated uniformity filter.

Equations

• ⋯ = ⋯