From 11117ec5553acfa01a7f6f5478be46ba5c8d1c36 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 11 Oct 2021 04:03:51 +0000
Subject: [PATCH] =?UTF-8?q?feat(topology/G=5Fdelta):=20a=20finite=20set=20?=
 =?UTF-8?q?is=20a=20G=CE=B4-set=20(#9644)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/topology/G_delta.lean    | 21 +++++++++++++++++++++
 src/topology/separation.lean | 10 ++++++++++
 2 files changed, 31 insertions(+)

diff --git a/src/topology/G_delta.lean b/src/topology/G_delta.lean
index 47b5f993cefa1..f2d70eb79b48c 100644
--- a/src/topology/G_delta.lean
+++ b/src/topology/G_delta.lean
@@ -49,6 +49,8 @@ def is_Gδ (s : set α) : Prop :=
 lemma is_open.is_Gδ {s : set α} (h : is_open s) : is_Gδ s :=
 ⟨{s}, by simp [h], countable_singleton _, (set.sInter_singleton _).symm⟩
 
+lemma is_Gδ_empty : is_Gδ (∅ : set α) := is_open_empty.is_Gδ
+
 lemma is_Gδ_univ : is_Gδ (univ : set α) := is_open_univ.is_Gδ
 
 lemma is_Gδ_bInter_of_open {I : set ι} (hI : countable I) {f : ι → set α}
@@ -95,6 +97,25 @@ begin
   exact is_open.union (Sopen a hab.1) (Topen b hab.2)
 end
 
+section first_countable
+
+open topological_space
+
+variables [t1_space α] [first_countable_topology α]
+
+lemma is_Gδ_singleton (a : α) : is_Gδ ({a} : set α) :=
+begin
+  rcases (is_countably_generated_nhds a).exists_antitone_subbasis (nhds_basis_opens _)
+    with ⟨U, hU, h_basis⟩,
+  rw [← bInter_basis_nhds h_basis.to_has_basis],
+  exact is_Gδ_bInter (countable_encodable _) (λ n hn, (hU n).2.is_Gδ),
+end
+
+lemma set.finite.is_Gδ {s : set α} (hs : finite s) : is_Gδ s :=
+finite.induction_on hs is_Gδ_empty $ λ a s _ _ hs, (is_Gδ_singleton a).union hs
+
+end first_countable
+
 end is_Gδ
 
 section continuous_at
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index 754772f7cdeab..2458bdfb8a18d 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -311,6 +311,16 @@ begin
   exact is_closed_bUnion hs (λ i hi, is_closed_singleton)
 end
 
+lemma bInter_basis_nhds [t1_space α] {ι : Sort*} {p : ι → Prop} {s : ι → set α} {x : α}
+  (h : (𝓝 x).has_basis p s) : (⋂ i (h : p i), s i) = {x} :=
+begin
+  simp only [eq_singleton_iff_unique_mem, mem_Inter],
+  refine ⟨λ i hi, mem_of_mem_nhds $ h.mem_of_mem hi, λ y hy, _⟩,
+  contrapose! hy,
+  rcases h.mem_iff.1 (compl_singleton_mem_nhds hy.symm) with ⟨i, hi, hsub⟩,
+  exact ⟨i, hi, λ h, hsub h rfl⟩
+end
+
 /-- If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is
 infinite. -/
 lemma infinite_of_mem_nhds {α} [topological_space α] [t1_space α] (x : α) [hx : ne_bot (𝓝[{x}ᶜ] x)]