feat(topology/separation, topology/metric_space/basic): add lemmas on…

… discrete subsets of a topological space (#5523)

These lemmas form part of a simplification of the proofs of #5361.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/topology/metric_space/basic.lean

@@ -674,6 +674,18 @@ lemma is_open_singleton_iff {X : Type*} [metric_space X] {x : X} :
   is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
 by simp [is_open_iff, subset_singleton_iff, mem_ball]
 
+/-- Given a point `x` in a discrete subset `s` of a metric space, there is an open ball
+centered at `x` and intersecting `s` only at `x`. -/
+lemma exists_ball_inter_eq_singleton_of_mem_discrete [discrete_topology s] {x : α} (hx : x ∈ s) :
+  ∃ ε > 0, metric.ball x ε ∩ s = {x} :=
+nhds_basis_ball.exists_inter_eq_singleton_of_mem_discrete hx
+
+/-- Given a point `x` in a discrete subset `s` of a metric space, there is a closed ball
+of positive radius centered at `x` and intersecting `s` only at `x`. -/
+lemma exists_closed_ball_inter_eq_singleton_of_discrete [discrete_topology s] {x : α} (hx : x ∈ s) :
+  ∃ ε > 0, metric.closed_ball x ε ∩ s = {x} :=
+nhds_basis_closed_ball.exists_inter_eq_singleton_of_mem_discrete hx
+
 end metric
 
 open metric

src/topology/separation.lean

@@ -139,6 +139,45 @@ begin
   exact is_closed_bUnion (finite.of_fintype _) (λ y _, is_closed_singleton)
 end
 
+lemma singleton_mem_nhds_within_of_mem_discrete {s : set α} [discrete_topology s]
+  {x : α} (hx : x ∈ s) :
+  {x} ∈ 𝓝[s] x :=
+begin
+  have : ({⟨x, hx⟩} : set s) ∈ 𝓝 (⟨x, hx⟩ : s), by simp [nhds_discrete],
+  simpa only [nhds_within_eq_map_subtype_coe hx, image_singleton]
+    using @image_mem_map _ _ _ (coe : s → α) _ this
+end
+
+lemma nhds_within_of_mem_discrete {s : set α} [discrete_topology s] {x : α} (hx : x ∈ s) :
+  𝓝[s] x = pure x :=
+le_antisymm (le_pure_iff.2 $ singleton_mem_nhds_within_of_mem_discrete hx) (pure_le_nhds_within hx)
+
+lemma filter.has_basis.exists_inter_eq_singleton_of_mem_discrete
+  {ι : Type*} {p : ι → Prop} {t : ι → set α} {s : set α} [discrete_topology s] {x : α}
+  (hb : (𝓝 x).has_basis p t) (hx : x ∈ s) :
+  ∃ i (hi : p i), t i ∩ s = {x} :=
+begin
+  rcases (nhds_within_has_basis hb s).mem_iff.1 (singleton_mem_nhds_within_of_mem_discrete hx)
+    with ⟨i, hi, hix⟩,
+  exact ⟨i, hi, subset.antisymm hix $ singleton_subset_iff.2 ⟨mem_of_nhds $ hb.mem_of_mem hi, hx⟩⟩
+end
+
+/-- A point `x` in a discrete subset `s` of a topological space admits a neighbourhood
+that only meets `s` at `x`.  -/
+lemma nhds_inter_eq_singleton_of_mem_discrete {s : set α} [discrete_topology s] {x : α} (hx : x ∈ s) :
+  ∃ U ∈ 𝓝 x, U ∩ s = {x} :=
+by simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hx
+
+/-- For point `x` in a discrete subset `s` of a topological space, there is a set `U`
+such that
+1. `U` is a punctured neighborhood of `x` (ie. `U ∪ {x}` is a neighbourhood of `x`),
+2. `U` is disjoint from `s`.
+-/
+lemma disjoint_nhds_within_of_mem_discrete {s : set α} [discrete_topology s] {x : α} (hx : x ∈ s) :
+  ∃ U ∈ 𝓝[{x}ᶜ] x, disjoint U s :=
+let ⟨V, h, h'⟩ := nhds_inter_eq_singleton_of_mem_discrete hx in ⟨{x}ᶜ ∩ V, inter_mem_nhds_within _ h,
+  (disjoint_iff_inter_eq_empty.mpr (by { rw [inter_assoc, h', compl_inter_self] }))⟩
+
 /-- A T₂ space, also known as a Hausdorff space, is one in which for every
   `x ≠ y` there exists disjoint open sets around `x` and `y`. This is
   the most widely used of the separation axioms. -/