Documentation

Mathlib.Topology.Baire.CompleteMetrizable

First Baire theorem #

In this file we prove that a completely pseudometrizable topological space is a Baire space.

source
@[instance 100]
instance BaireSpace.of_completelyPseudoMetrizable {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] :
BaireSpace X

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