From 3166f4ef1dcd91ffa6ddf4de4f2b4c7262625286 Mon Sep 17 00:00:00 2001 From: damiano Date: Sat, 9 Jan 2021 12:23:42 +0000 Subject: [PATCH] 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 --- src/topology/metric_space/basic.lean | 12 +++++++++ src/topology/separation.lean | 39 ++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index ab3413a6075ae..0b16764981680 100644 --- a/src/topology/metric_space/basic.lean +++ b/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 diff --git a/src/topology/separation.lean b/src/topology/separation.lean index 4401105a288c6..fe1449f5cb56b 100644 --- a/src/topology/separation.lean +++ b/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. -/