First Baire theorem #
In this file we prove that a completely pseudometrizable topological space is a Baire space.
@[instance 100]
instance
BaireSpace.of_completelyPseudoMetrizable
{X : Type u_1}
[TopologicalSpace X]
[TopologicalSpace.IsCompletelyPseudoMetrizableSpace X]
:
First Baire theorem: a completely pseudometrizable topological space has Baire property.