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.