chore(topology/*): more lemmas about dense/dense_range (#9492)

src/topology/bases.lean

@@ -347,6 +347,13 @@ protected lemma dense_range.separable_space {α β : Type*} [topological_space 
 let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α in
 ⟨⟨f '' s, countable.image s_cnt f, h.dense_image h' s_dense⟩⟩
 
+lemma dense.exists_countable_dense_subset {α : Type*} [topological_space α]
+  {s : set α} [separable_space s] (hs : dense s) :
+  ∃ t ⊆ s, countable t ∧ dense t :=
+let ⟨t, htc, htd⟩ := exists_countable_dense s
+in ⟨coe '' t, image_subset_iff.2 $ λ x _, mem_preimage.2 $ subtype.coe_prop _, htc.image coe,
+  hs.dense_range_coe.dense_image continuous_subtype_val htd⟩
+
 namespace topological_space
 universe u
 variables (α : Type u) [t : topological_space α]

src/topology/basic.lean

@@ -423,6 +423,11 @@ end
 
 alias dense_iff_inter_open ↔ dense.inter_open_nonempty _
 
+lemma dense.exists_mem_open {s : set α} (hs : dense s) {U : set α} (ho : is_open U)
+  (hne : U.nonempty) :
+  ∃ x ∈ s, x ∈ U :=
+let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne in ⟨x, hx.2, hx.1⟩
+
 lemma dense.nonempty_iff {s : set α} (hs : dense s) :
   s.nonempty ↔ nonempty α :=
 ⟨λ ⟨x, hx⟩, ⟨x⟩, λ ⟨x⟩,
@@ -1351,6 +1356,9 @@ dense_iff_closure_eq
 lemma dense_range.closure_range (h : dense_range f) : closure (range f) = univ :=
 h.closure_eq
 
+lemma dense.dense_range_coe {s : set α} (h : dense s) : dense_range (coe : s → α) :=
+by simpa only [dense_range, subtype.range_coe_subtype]
+
 lemma continuous.range_subset_closure_image_dense {f : α → β} (hf : continuous f)
   {s : set α} (hs : dense s) :
   range f ⊆ closure (f '' s) :=
@@ -1392,6 +1400,11 @@ hf.nonempty_iff.mpr h
 def dense_range.some (hf : dense_range f) (b : β) : κ :=
 classical.choice $ hf.nonempty_iff.mpr ⟨b⟩
 
+lemma dense_range.exists_mem_open (hf : dense_range f) {s : set β} (ho : is_open s)
+  (hs : s.nonempty) :
+  ∃ a, f a ∈ s :=
+exists_range_iff.1 $ hf.exists_mem_open ho hs
+
 end dense_range
 
 end continuous

src/topology/dense_embedding.lean

@@ -31,7 +31,7 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 
 /-- `i : α → β` is "dense inducing" if it has dense range and the topology on `α`
   is the one induced by `i` from the topology on `β`. -/
-structure dense_inducing [topological_space α] [topological_space β] (i : α → β)
+@[protect_proj] structure dense_inducing [topological_space α] [topological_space β] (i : α → β)
   extends inducing i : Prop :=
 (dense : dense_range i)
 
@@ -62,6 +62,13 @@ begin
      ... ⊆ closure (i '' s)         : closure_mono (image_subset i sub)
 end
 
+lemma dense_image (di : dense_inducing i) {s : set α} : dense (i '' s) ↔ dense s :=
+begin
+  refine ⟨λ H x, _, di.dense.dense_image di.continuous⟩,
+  rw [di.to_inducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ],
+  trivial
+end
+
 /-- The product of two dense inducings is a dense inducing -/
 protected lemma prod [topological_space γ] [topological_space δ]
   {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_inducing e₁) (de₂ : dense_inducing e₂) :
@@ -223,27 +230,31 @@ protected lemma prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_embedd
   ..dense_inducing.prod de₁.to_dense_inducing de₂.to_dense_inducing }
 
 /-- The dense embedding of a subtype inside its closure. -/
-def subtype_emb {α : Type*} (p : α → Prop) (e : α → β) (x : {x // p x}) :
+@[simps] def subtype_emb {α : Type*} (p : α → Prop) (e : α → β) (x : {x // p x}) :
   {x // x ∈ closure (e '' {x | p x})} :=
 ⟨e x, subset_closure $ mem_image_of_mem e x.prop⟩
 
 protected lemma subtype (p : α → Prop) : dense_embedding (subtype_emb p e) :=
-{ dense_embedding .
-  dense   := assume ⟨x, hx⟩, closure_subtype.mpr $
-    have (λ (x : {x // p x}), e x) = e ∘ coe, from rfl,
+{ dense := dense_iff_closure_eq.2 $
     begin
-      rw ← image_univ,
-      simp [(image_comp _ _ _).symm, (∘), subtype_emb, -image_univ],
-      rw [this, image_comp, subtype.coe_image],
-      simp,
-      assumption
+      ext ⟨x, hx⟩,
+      rw image_eq_range at hx,
+      simpa [closure_subtype, ← range_comp, (∘)],
     end,
-  inj     := assume ⟨x, hx⟩ ⟨y, hy⟩ h, subtype.eq $ de.inj $ @@congr_arg subtype.val h,
+  inj := (de.inj.comp subtype.coe_injective).cod_restrict _,
   induced := (induced_iff_nhds_eq _).2 (assume ⟨x, hx⟩,
     by simp [subtype_emb, nhds_subtype_eq_comap, de.to_inducing.nhds_eq_comap, comap_comap, (∘)]) }
 
+lemma dense_image {s : set α} : dense (e '' s) ↔ dense s :=
+de.to_dense_inducing.dense_image
+
 end dense_embedding
 
+lemma dense.dense_embedding_coe [topological_space α] {s : set α} (hs : dense s) :
+  dense_embedding (coe : s → α) :=
+{ dense := hs.dense_range_coe,
+  .. embedding_subtype_coe }
+
 lemma is_closed_property [topological_space β] {e : α → β} {p : β → Prop}
   (he : dense_range e) (hp : is_closed {x | p x}) (h : ∀a, p (e a)) :
   ∀b, p b :=