feat(topology/*): lemmas about dense/dense_range and `is_(pre)con…

…nected` (#8651)

* add `dense_compl_singleton`;
* extract new lemma `is_preconnected_range` from the proof of
  `is_connected_range`;
* add `dense_range.preconnected_space` and
  `dense_inducing.preconnected_space`;
* rename `self_sub_closure_image_preimage_of_open` to
  `self_subset_closure_image_preimage_of_open`.

Inspired by #8579

src/topology/basic.lean

@@ -429,6 +429,17 @@ hs.nonempty_iff.2 h
 lemma dense.mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) (hd : dense s₁) : dense s₂ :=
 λ 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 α) :=
+begin
+  fsplit,
+  { intros hd ho,
+    exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _) },
+  { refine λ ho, dense_iff_inter_open.2 (λ U hU hne, inter_compl_nonempty_iff.2 $ λ hUx, _),
+    obtain rfl : U = {x}, from eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩,
+    exact ho hU }
+end
+
 /-!
 ### Frontier of a set
 -/
@@ -902,6 +913,11 @@ end
 lemma closure_inter_open' {s t : set α} (h : is_open t) : closure s ∩ t ⊆ closure (s ∩ t) :=
 by simpa only [inter_comm] using closure_inter_open h
 
+lemma dense.open_subset_closure_inter {s t : set α} (hs : dense s) (ht : is_open t) :
+  t ⊆ closure (t ∩ s) :=
+calc t = t ∩ closure s   : by rw [hs.closure_eq, inter_univ]
+   ... ⊆ closure (t ∩ s) : closure_inter_open ht
+
 lemma mem_closure_of_mem_closure_union {s₁ s₂ : set α} {x : α} (h : x ∈ closure (s₁ ∪ s₂))
   (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ :=
 begin
@@ -1315,6 +1331,12 @@ lemma dense_range.dense_image {f : α → β} (hf' : dense_range f) (hf : contin
   dense (f '' s)  :=
 (hf'.mono $ hf.range_subset_closure_image_dense hs).of_closure
 
+/-- If `f` has dense range and `s` is an open set in the codomain of `f`, then the image of the
+preimage of `s` under `f` is dense in `s`. -/
+lemma dense_range.subset_closure_image_preimage_of_is_open (hf : dense_range f) {s : set β}
+  (hs : is_open s) : s ⊆ closure (f '' (f ⁻¹' s)) :=
+by { rw image_preimage_eq_inter_range, exact hf.open_subset_closure_inter hs }
+
 /-- If a continuous map with dense range maps a dense set to a subset of `t`, then `t` is a dense
 set. -/
 lemma dense_range.dense_of_maps_to {f : α → β} (hf' : dense_range f) (hf : continuous f)

src/topology/connected.lean

@@ -254,14 +254,18 @@ class connected_space (α : Type u) [topological_space α] extends preconnected_
 
 attribute [instance, priority 50] connected_space.to_nonempty -- see Note [lower instance priority]
 
+lemma is_preconnected_range [topological_space β] [preconnected_space α] {f : α → β}
+  (h : continuous f) : is_preconnected (range f) :=
+@image_univ _ _ f ▸ is_preconnected_univ.image _ h.continuous_on
+
 lemma is_connected_range [topological_space β] [connected_space α] {f : α → β} (h : continuous f) :
   is_connected (range f) :=
-begin
-  inhabit α,
-  rw ← image_univ,
-  exact ⟨⟨f (default α), mem_image_of_mem _ (mem_univ _)⟩,
-         is_preconnected.image is_preconnected_univ _ h.continuous_on⟩
-end
+⟨range_nonempty f, is_preconnected_range h⟩
+
+lemma dense_range.preconnected_space [topological_space β] [preconnected_space α] {f : α → β}
+  (hf : dense_range f) (hc : continuous f) :
+  preconnected_space β :=
+⟨hf.closure_eq ▸ (is_preconnected_range hc).closure⟩
 
 lemma connected_space_iff_connected_component :
   connected_space α ↔ ∃ x : α, connected_component x = univ :=

src/topology/dense_embedding.lean

@@ -49,30 +49,17 @@ di.to_inducing.continuous
 lemma closure_range : closure (range i) = univ :=
 di.dense.closure_range
 
-lemma self_sub_closure_image_preimage_of_open {s : set β} (di : dense_inducing i) :
-  is_open s → s ⊆ closure (i '' (i ⁻¹' s)) :=
-begin
-  intros s_op b b_in_s,
-  rw [image_preimage_eq_inter_range, mem_closure_iff],
-  intros U U_op b_in,
-  rw ←inter_assoc,
-  exact (dense_iff_inter_open.1 di.dense) _ (is_open.inter U_op s_op) ⟨b, b_in, b_in_s⟩
-end
+lemma preconnected_space [preconnected_space α] (di : dense_inducing i) : preconnected_space β :=
+di.dense.preconnected_space di.continuous
 
-lemma closure_image_nhds_of_nhds {s : set α} {a : α} (di : dense_inducing i) :
-  s ∈ 𝓝 a → closure (i '' s) ∈ 𝓝 (i a) :=
+lemma closure_image_mem_nhds {s : set α} {a : α} (di : dense_inducing i) (hs : s ∈ 𝓝 a) :
+  closure (i '' s) ∈ 𝓝 (i a) :=
 begin
-  rw [di.nhds_eq_comap a, mem_comap_sets],
-  intro h,
-  rcases h with ⟨t, t_nhd, sub⟩,
-  rw mem_nhds_iff at t_nhd,
-  rcases t_nhd with ⟨U, U_sub, ⟨U_op, e_a_in_U⟩⟩,
-  have := calc i ⁻¹' U ⊆ i⁻¹' t : preimage_mono U_sub
-                   ... ⊆ s      : sub,
-  have := calc U ⊆ closure (i '' (i ⁻¹' U)) : self_sub_closure_image_preimage_of_open di U_op
-             ... ⊆ closure (i '' s)         : closure_mono (image_subset i this),
-  have U_nhd : U ∈ 𝓝 (i a) := is_open.mem_nhds U_op e_a_in_U,
-  exact (𝓝 (i a)).sets_of_superset U_nhd this
+  rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs,
+  rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩,
+  refine mem_sets_of_superset (hUo.mem_nhds haU) _,
+  calc U ⊆ closure (i '' (i ⁻¹' U)) : di.dense.subset_closure_image_preimage_of_is_open hUo
+     ... ⊆ closure (i '' s)         : closure_mono (image_subset i sub)
 end
 
 /-- The product of two dense inducings is a dense inducing -/