feat(topology/G_delta): a finite set is a Gδ-set (#9644)

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

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)]