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.
theorem
IsGδ.baireSpace_of_t2Space_locallyCompactSpace
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
[R1Space X]
[LocallyCompactSpace X]
(hG : IsGδ s)
:
BaireSpace ↑s
A Gδ subset of a locally compact R₁ space is Baire.
@[deprecated IsGδ.baireSpace_of_t2Space_locallyCompactSpace (since := "2026-06-04")]
theorem
IsGδ.of_t2Space_locallyCompactSpace
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
[R1Space X]
[LocallyCompactSpace X]
(hG : IsGδ s)
:
BaireSpace ↑s
Alias of IsGδ.baireSpace_of_t2Space_locallyCompactSpace.
A Gδ subset of a locally compact R₁ space is Baire.