Second Baire theorem #
In this file we prove that a locally compact regular topological space has Baire property.
@[instance 100]
instance
BaireSpace.of_t2Space_locallyCompactSpace
{X : Type u_1}
[TopologicalSpace X]
[R1Space X]
[LocallyCompactSpace X]
:
Second Baire theorem: locally compact R₁ spaces are Baire.
Equations
- ⋯ = ⋯