feat(topology/basic): interior of a singleton (#8784)

* add generic lemmas `interior_singleton`, `closure_compl_singleton`;
* add more lemmas and instances about `ne_bot (𝓝[{x}ᶜ] x)`;
* rename `dense_compl_singleton` to `dense_compl_singleton_iff_not_open`,
  add new `dense_compl_singleton` that assumes `[ne_bot (𝓝[{x}ᶜ] x)]`.

src/analysis/normed_space/basic.lean

@@ -1349,6 +1349,14 @@ nnreal.eq $ norm_of_nonneg hx
 lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (∥x∥₊ : ℝ≥0∞) = ennreal.of_real x :=
 by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hx] }
 
+/-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
+This is a particular case of `module.punctured_nhds_ne_bot`. -/
+instance punctured_nhds_module_ne_bot
+  {E : Type*} [add_comm_group E] [topological_space E] [has_continuous_add E] [nontrivial E]
+  [module ℝ E] [has_continuous_smul ℝ E] (x : E) :
+  ne_bot (𝓝[{x}ᶜ] x) :=
+module.punctured_nhds_ne_bot ℝ E x
+
 end real
 
 namespace nnreal
@@ -1654,20 +1662,7 @@ theorem interior_closed_ball' [normed_space ℝ E] [nontrivial E] (x : E) (r : 
 begin
   rcases lt_trichotomy r 0 with hr|rfl|hr,
   { simp [closed_ball_eq_empty.2 hr, ball_eq_empty.2 hr.le] },
-  { suffices : x ∉ interior {x},
-    { rw [ball_zero, closed_ball_zero, ← set.subset_empty_iff],
-      intros y hy,
-      obtain rfl : y = x := set.mem_singleton_iff.1 (interior_subset hy),
-      exact this hy },
-    rw [← set.mem_compl_iff, ← closure_compl],
-    rcases exists_ne (0 : E) with ⟨z, hz⟩,
-    suffices : (λ c : ℝ, x + c • z) 0 ∈ closure ({x}ᶜ : set E),
-      by simpa only [zero_smul, add_zero] using this,
-    have : (0:ℝ) ∈ closure (set.Ioi (0:ℝ)), by simp [closure_Ioi],
-    refine (continuous_const.add (continuous_id.smul
-      continuous_const)).continuous_within_at.mem_closure this _,
-    intros c hc,
-    simp [smul_eq_zero, hz, ne_of_gt hc] },
+  { rw [closed_ball_zero, ball_zero, interior_singleton] },
   { exact interior_closed_ball x hr }
 end
 

src/topology/algebra/module.lean

@@ -32,13 +32,13 @@ section
 
 variables {R : Type*} {M : Type*}
 [ring R] [topological_space R]
-[topological_space M] [add_comm_group M]
+[topological_space M] [add_comm_group M] [has_continuous_add M]
 [module R M] [has_continuous_smul R M]
 
 /-- If `M` is a topological module over `R` and `0` is a limit of invertible elements of `R`, then
 `⊤` is the only submodule of `M` with a nonempty interior.
 This is the case, e.g., if `R` is a nondiscrete normed field. -/
-lemma submodule.eq_top_of_nonempty_interior' [has_continuous_add M]
+lemma submodule.eq_top_of_nonempty_interior'
   [ne_bot (𝓝[{x : R | is_unit x}] 0)]
   (s : submodule R M) (hs : (interior (s:set M)).nonempty) :
   s = ⊤ :=
@@ -56,6 +56,30 @@ begin
   exact (s.smul_mem_iff' _).1 ((s.add_mem_iff_right hy').1 hu)
 end
 
+variables (R M)
+
+/-- Let `R` be a topological ring such that zero is not an isolated point (e.g., a nondiscrete
+normed field, see `normed_field.punctured_nhds_ne_bot`). Let `M` be a nontrivial module over `R`
+such that `c • x = 0` implies `c = 0 ∨ x = 0`. Then `M` has no isolated points. We formulate this
+using `ne_bot (𝓝[{x}ᶜ] x)`.
+
+This lemma is not an instance because Lean would need to find `[has_continuous_smul ?m_1 M]` with
+unknown `?m_1`. We register this as an instance for `R = ℝ` in `real.punctured_nhds_module_ne_bot`.
+One can also use `haveI := module.punctured_nhds_ne_bot R M` in a proof.
+-/
+lemma module.punctured_nhds_ne_bot [nontrivial M] [ne_bot (𝓝[{0}ᶜ] (0 : R))]
+  [no_zero_smul_divisors R M] (x : M) :
+  ne_bot (𝓝[{x}ᶜ] x) :=
+begin
+  rcases exists_ne (0 : M) with ⟨y, hy⟩,
+  suffices : tendsto (λ c : R, x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x), from this.ne_bot,
+  refine tendsto.inf _ (tendsto_principal_principal.2 $ _),
+  { convert tendsto_const_nhds.add ((@tendsto_id R _).smul_const y),
+    rw [zero_smul, add_zero] },
+  { intros c hc,
+    simpa [hy] using hc }
+end
+
 end
 
 section closure

src/topology/basic.lean

@@ -394,6 +394,12 @@ eq_univ_iff_forall.symm
 lemma dense.closure_eq {s : set α} (h : dense s) : closure s = univ :=
 dense_iff_closure_eq.mp h
 
+lemma interior_eq_empty_iff_dense_compl {s : set α} : interior s = ∅ ↔ dense sᶜ :=
+by rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]
+
+lemma dense.interior_compl {s : set α} (h : dense s) : interior sᶜ = ∅ :=
+interior_eq_empty_iff_dense_compl.2 $ by rwa compl_compl
+
 /-- The closure of a set `s` is dense if and only if `s` is dense. -/
 @[simp] lemma dense_closure {s : set α} : dense (closure s) ↔ dense s :=
 by rw [dense, dense, closure_closure]
@@ -430,7 +436,7 @@ lemma dense.mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) (hd : dense s₁) : de
 λ x, closure_mono h (hd x)
 
 /-- Complement to a singleton is dense if and only if the singleton is not an open set. -/
-lemma dense_compl_singleton {x : α} : dense ({x}ᶜ : set α) ↔ ¬is_open ({x} : set α) :=
+lemma dense_compl_singleton_iff_not_open {x : α} : dense ({x}ᶜ : set α) ↔ ¬is_open ({x} : set α) :=
 begin
   fsplit,
   { intros hd ho,
@@ -862,6 +868,31 @@ mem_closure_iff_frequently.trans cluster_pt_principal_iff_frequently.symm
 lemma mem_closure_iff_nhds_ne_bot {s : set α} : a ∈ closure s ↔ 𝓝 a ⊓ 𝓟 s ≠ ⊥ :=
 mem_closure_iff_cluster_pt.trans ne_bot_iff
 
+lemma mem_closure_iff_nhds_within_ne_bot {s : set α} {x : α} :
+  x ∈ closure s ↔ ne_bot (𝓝[s] x) :=
+mem_closure_iff_cluster_pt
+
+/-- If `x` is not an isolated point of a topological space, then `{x}ᶜ` is dense in the whole
+space. -/
+lemma dense_compl_singleton (x : α) [ne_bot (𝓝[{x}ᶜ] x)] : dense ({x}ᶜ : set α) :=
+begin
+  intro y,
+  unfreezingI { rcases eq_or_ne y x with rfl|hne },
+  { rwa mem_closure_iff_nhds_within_ne_bot },
+  { exact subset_closure hne }
+end
+
+/-- If `x` is not an isolated point of a topological space, then the closure of `{x}ᶜ` is the whole
+space. -/
+@[simp] lemma closure_compl_singleton (x : α) [ne_bot (𝓝[{x}ᶜ] x)] :
+  closure {x}ᶜ = (univ : set α) :=
+(dense_compl_singleton x).closure_eq
+
+/-- If `x` is not an isolated point of a topological space, then the interior of `{x}ᶜ` is empty. -/
+@[simp] lemma interior_singleton (x : α) [ne_bot (𝓝[{x}ᶜ] x)] :
+  interior {x} = (∅ : set α) :=
+interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)
+
 lemma closure_eq_cluster_pts {s : set α} : closure s = {a | cluster_pt a (𝓟 s)} :=
 set.ext $ λ x, mem_closure_iff_cluster_pt
 

src/topology/continuous_on.lean

@@ -317,10 +317,6 @@ theorem principal_subtype {α : Type*} (s : set α) (t : set {x // x ∈ s}) :
   𝓟 t = comap coe (𝓟 ((coe : s → α) '' t)) :=
 by rw [comap_principal, set.preimage_image_eq _ subtype.coe_injective]
 
-lemma mem_closure_iff_nhds_within_ne_bot {s : set α} {x : α} :
-  x ∈ closure s ↔ ne_bot (𝓝[s] x) :=
-mem_closure_iff_cluster_pt
-
 lemma nhds_within_ne_bot_of_mem {s : set α} {x : α} (hx : x ∈ s) :
   ne_bot (𝓝[s] x) :=
 mem_closure_iff_nhds_within_ne_bot.1 $ subset_closure hx