We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 67c8029 commit 482f01dCopy full SHA for 482f01d
1 file changed
Mathlib/Topology/Baire/LocallyCompactRegular.lean
@@ -59,8 +59,7 @@ instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace : BaireSpac
59
exact hK_nonempty.mono hK_subset
60
61
/-- A Gδ subset of a locally compact R₁ space is Baire. -/
62
-theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) :
63
- BaireSpace s := by
+theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) : BaireSpace s := by
64
have : BaireSpace (closure s) := by
65
convert BaireSpace.of_t2Space_locallyCompactSpace using 1
66
· infer_instance
0 commit comments