refactor(*): migrate to dense API (#4447)

@PatrickMassot introduced `dense` in #4399. In this PR I review the API and migrate many definitions and lemmas
to use `dense s` instead of `closure s = univ`. I also generalize `second_countable_of_separable` to a `uniform_space`
with a countably generated uniformity filter.

## API changes

### Use `dense` or `dense_range` instead of `closure _ = univ`

#### Lemmas

- `has_fderiv_within_at.unique_diff_within_at`;
- `exists_dense_seq`;
- `dense_Inter_of_open_nat`;
- `dense_sInter_of_open`;
- `dense_bInter_of_open`;
- `dense_Inter_of_open`;
- `dense_sInter_of_Gδ`;
- `dense_bInter_of_Gδ`;
- `eventually_residual`;
- `mem_residual`;
- `dense_bUnion_interior_of_closed`;
- `dense_sUnion_interior_of_closed`;
- `dense_Union_interior_of_closed`;
- `Kuratowski_embeddinng.embedding_of_subset_isometry`;
- `continuous_extend_from`;

#### Definitions

- `unique_diff_within_at`;
- `residual`;

### Rename

- `submodule.linear_eq_on` → `linear_map.eq_on_span`, `linear_map.eq_on_span'`;
- `submodule.linear_map.ext_on` → `linear_map.ext_on_range`;
- `filter.is_countably_generated.has_antimono_basis` →
  `filter.is_countably_generated.exists_antimono_basis`;
- `exists_countable_closure_eq_univ` → `exists_countable_dense`, use `dense`;
- `dense_seq_dense` → `dense_range_dense_seq`, use `dense`;
- `dense_range.separable_space` is now `protected`;
- `dense_of_subset_dense` → `dense.mono`;
- `dense_inter_of_open_left` → `dense.inter_of_open_left`;
- `dense_inter_of_open_right` → `dense.inter_of_open_right`;
- `continuous.dense_image_of_dense_range` → `dense_range.dense_image`;
- `dense_range.inhabited`, `dense_range.nonempty`: changed API, TODO;
- `quotient_dense_of_dense` → `dense.quotient`, use `dense`;
- `dense_inducing.separable` → `dense_inducing.separable_space`, add `protected`;
- `dense_embedding.separable` → `dense_embedding.separable_space`, add `protected`;
- `dense_inter_of_Gδ` → `dense.inter_of_Gδ`;
- `stone_cech_unit_dense` → `dense_range_stone_cech_unit`;
- `abstract_completion.dense'` → `abstract_completion.closure_range`;
- `Cauchy.pure_cauchy_dense` → `Cauchy.dense_range_pure_cauchy`;
- `completion.dense` → `completion.dense_range_coe`;
- `completion.dense₂` → `completion.dense_range_coe₂`;
- `completion.dense₃` → `completion.dense_range_coe₃`;

### New

- `has_fderiv_within_at.unique_on` : if `f'` and `f₁'` are two derivatives of `f`
  within `s` at `x`, then they are equal on the tangent cone to `s` at `x`;
- `local_homeomorph.mdifferentiable.mfderiv_bijective`,
  `local_homeomorph.mdifferentiable.mfderiv_surjective`
- `continuous_linear_map.eq_on_closure_span`: if two continuous linear maps are equal on `s`,
  then they are equal on `closure (submodule.span s)`;
- `continuous_linear_map.ext_on`: if two continuous linear maps are equal on a set `s` such that
  `submodule.span s` is dense, then they are equal;
- `dense_closure`: `closure s` is dense iff `s` is dense;
- `dense.of_closure`, `dense.closure`: aliases for `dense_closure.mp` and `dense_closure.mpr`;
- `dense_univ`: `univ` is dense;
- `dense.inter_open_nonempty`: alias for `dense_iff_inter_open.mp`;
- `dense.nonempty_iff`: if `s : set α` is a dense set, then `s` is nonempty iff `α` is nonempty;
- `dense.nonempty`: a dense set in a nonempty type is nonempty;
- `dense_range.some`: given a function with `dense_range` and a point in the codomain, returns a point in the domain;
- `function.surjective.dense_range`: a surjective function has dense range;
- `continuous.range_subset_closure_image_dense`: closure of the image of a dense set under
  a continuous function includes the range of this function;
- `dense_range.dense_of_maps_to`: if a function with dense range maps a dense set `s` to `t`, then
  `t` is dense in the codomain;
- `dense_range.quotient`;
- `dense.prod`: product of two dense sets is dense in the product;
- `set.eq_on.closure`;
- `continuous.ext_on`;
- `linear_map.ext_on`



Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: 3 people

src/analysis/calculus/fderiv.lean

@@ -240,36 +240,22 @@ begin
   rwa [this, zero_add] at L3
 end
 
+/-- If `f'` and `f₁'` are two derivatives of `f` within `s` at `x`, then they are equal on the
+tangent cone to `s` at `x` -/
+theorem has_fderiv_within_at.unique_on (hf : has_fderiv_within_at f f' s x)
+  (hg : has_fderiv_within_at f f₁' s x) :
+  eq_on f' f₁' (tangent_cone_at 𝕜 s x) :=
+λ y ⟨c, d, dtop, clim, cdlim⟩,
+  tendsto_nhds_unique (hf.lim at_top dtop clim cdlim) (hg.lim at_top dtop clim cdlim)
+
 /-- `unique_diff_within_at` achieves its goal: it implies the uniqueness of the derivative. -/
 theorem unique_diff_within_at.eq (H : unique_diff_within_at 𝕜 s x)
-  (h : has_fderiv_within_at f f' s x) (h₁ : has_fderiv_within_at f f₁' s x) : f' = f₁' :=
-begin
-  have A : ∀y ∈ tangent_cone_at 𝕜 s x, f' y = f₁' y,
-  { rintros y ⟨c, d, dtop, clim, cdlim⟩,
-    exact tendsto_nhds_unique (h.lim at_top dtop clim cdlim) (h₁.lim at_top dtop clim cdlim) },
-  have B : ∀y ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 s x), f' y = f₁' y,
-  { assume y hy,
-    apply submodule.span_induction hy,
-    { exact λy hy, A y hy },
-    { simp only [continuous_linear_map.map_zero] },
-    { simp {contextual := tt} },
-    { simp {contextual := tt} } },
-  have C : ∀y ∈ closure ((submodule.span 𝕜 (tangent_cone_at 𝕜 s x)) : set E), f' y = f₁' y,
-  { assume y hy,
-    let K := {y | f' y = f₁' y},
-    have : (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E) ⊆ K := B,
-    have : closure (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E) ⊆ closure K :=
-      closure_mono this,
-    have : y ∈ closure K := this hy,
-    rwa (is_closed_eq f'.continuous f₁'.continuous).closure_eq at this },
-  rw H.1 at C,
-  ext y,
-  exact C y (mem_univ _)
-end
+  (hf : has_fderiv_within_at f f' s x) (hg : has_fderiv_within_at f f₁' s x) : f' = f₁' :=
+continuous_linear_map.ext_on H.1 (hf.unique_on hg)
 
 theorem unique_diff_on.eq (H : unique_diff_on 𝕜 s) (hx : x ∈ s)
   (h : has_fderiv_within_at f f' s x) (h₁ : has_fderiv_within_at f f₁' s x) : f' = f₁' :=
-unique_diff_within_at.eq (H x hx) h h₁
+(H x hx).eq h h₁
 
 end derivative_uniqueness
 
@@ -2458,44 +2444,22 @@ end
 under a map with onto derivative has also the unique differentiability property at the image point.
 -/
 lemma has_fderiv_within_at.unique_diff_within_at {x : E} (h : has_fderiv_within_at f f' s x)
-  (hs : unique_diff_within_at 𝕜 s x) (h' : closure (range f') = univ) :
+  (hs : unique_diff_within_at 𝕜 s x) (h' : dense_range f') :
   unique_diff_within_at 𝕜 (f '' s) (f x) :=
 begin
-  have B : ∀v ∈ (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E),
-    f' v ∈ (submodule.span 𝕜 (tangent_cone_at 𝕜 (f '' s) (f x)) : set F),
-  { assume v hv,
-    apply submodule.span_induction hv,
-    { exact λ w hw, submodule.subset_span (h.maps_to_tangent_cone hw) },
-    { simp },
-    { assume w₁ w₂ hw₁ hw₂,
-      rw continuous_linear_map.map_add,
-      exact submodule.add_mem (submodule.span 𝕜 (tangent_cone_at 𝕜 (f '' s) (f x))) hw₁ hw₂ },
-    { assume a w hw,
-      rw continuous_linear_map.map_smul,
-      exact submodule.smul_mem (submodule.span 𝕜 (tangent_cone_at 𝕜 (f '' s) (f x))) _ hw } },
-  rw [unique_diff_within_at, ← univ_subset_iff],
-  split,
-  show f x ∈ closure (f '' s), from h.continuous_within_at.mem_closure_image hs.2,
-  show univ ⊆ closure ↑(submodule.span 𝕜 (tangent_cone_at 𝕜 (f '' s) (f x))), from calc
-    univ ⊆ closure (range f') : univ_subset_iff.2 h'
-    ... = closure (f' '' univ) : by rw image_univ
-    ... = closure (f' '' (closure (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E))) : by rw hs.1
-    ... ⊆ closure (closure (f' '' (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E))) :
-      closure_mono (image_closure_subset_closure_image f'.cont)
-    ... = closure (f' '' (submodule.span 𝕜 (tangent_cone_at 𝕜 s x) : set E)) : closure_closure
-    ... ⊆ closure (submodule.span 𝕜 (tangent_cone_at 𝕜 (f '' s) (f x)) : set F) :
-      closure_mono (image_subset_iff.mpr B)
+  refine ⟨h'.dense_of_maps_to f'.continuous hs.1 _,
+    h.continuous_within_at.mem_closure_image hs.2⟩,
+  show submodule.span 𝕜 (tangent_cone_at 𝕜 s x) ≤
+    (submodule.span 𝕜 (tangent_cone_at 𝕜 (f '' s) (f x))).comap f',
+  rw [submodule.span_le],
+  exact h.maps_to_tangent_cone.mono (subset.refl _) submodule.subset_span
 end
 
 lemma has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv
   {x : E} (e' : E ≃L[𝕜] F) (h : has_fderiv_within_at f (e' : E →L[𝕜] F) s x)
   (hs : unique_diff_within_at 𝕜 s x) :
   unique_diff_within_at 𝕜 (f '' s) (f x) :=
-begin
-  apply h.unique_diff_within_at hs,
-  have : set.range (e' : E →L[𝕜] F) = univ := e'.to_linear_equiv.to_equiv.range_eq_univ,
-  rw [this, closure_univ]
-end
+h.unique_diff_within_at hs e'.surjective.dense_range
 
 lemma continuous_linear_equiv.unique_diff_on_preimage_iff (e : F ≃L[𝕜] E) :
   unique_diff_on 𝕜 (e ⁻¹' s) ↔ unique_diff_on 𝕜 s :=

src/analysis/calculus/tangent_cone.lean

@@ -50,7 +50,7 @@ To avoid pathologies in dimension 0, we also require that `x` belongs to the clo
 is automatic when `E` is not `0`-dimensional).
  -/
 def unique_diff_within_at (s : set E) (x : E) : Prop :=
-closure ((submodule.span 𝕜 (tangent_cone_at 𝕜 s x)) : set E) = univ ∧ x ∈ closure s
+dense ((submodule.span 𝕜 (tangent_cone_at 𝕜 s x)) : set E) ∧ x ∈ closure s
 
 /-- A property ensuring that the tangent cone to `s` at any of its points spans a dense subset of
 the whole space.  The main role of this property is to ensure that the differential along `s` is
@@ -268,10 +268,9 @@ lemma unique_diff_within_at.mono_nhds (h : unique_diff_within_at 𝕜 s x)
   unique_diff_within_at 𝕜 t x :=
 begin
   unfold unique_diff_within_at at *,
-  rw [← univ_subset_iff, ← h.1],
   rw [mem_closure_iff_nhds_within_ne_bot] at h ⊢,
-  exact ⟨closure_mono (submodule.span_mono (tangent_cone_mono_nhds st)),
-    ne_bot_of_le_ne_bot h.2 st⟩
+  exact ⟨h.1.mono $ submodule.span_mono $ tangent_cone_mono_nhds st,
+    h.2.mono st⟩
 end
 
 lemma unique_diff_within_at.mono (h : unique_diff_within_at 𝕜 s x) (st : s ⊆ t) :
@@ -317,13 +316,13 @@ lemma unique_diff_within_at.prod {t : set F} {y : F}
   unique_diff_within_at 𝕜 (set.prod s t) (x, y) :=
 begin
   rw [unique_diff_within_at] at ⊢ hs ht,
-  rw [← univ_subset_iff, closure_prod_eq],
+  rw [closure_prod_eq],
   refine ⟨_, hs.2, ht.2⟩,
-  have : _ ⊆ tangent_cone_at 𝕜 (s.prod t) (x, y) :=
-    union_subset (subset_tangent_cone_prod_left ht.2) (subset_tangent_cone_prod_right hs.2),
-  refine subset.trans _ (closure_mono $ submodule.span_mono this),
-  erw [linear_map.span_inl_union_inr, submodule.prod_coe, closure_prod_eq,
-    hs.1, ht.1, univ_prod_univ]
+  have : _ ≤ submodule.span 𝕜 (tangent_cone_at 𝕜 (s.prod t) (x, y)) :=
+    submodule.span_mono (union_subset (subset_tangent_cone_prod_left ht.2)
+      (subset_tangent_cone_prod_right hs.2)),
+  rw [linear_map.span_inl_union_inr, submodule.le_def, submodule.prod_coe] at this,
+  exact (hs.1.prod ht.1).mono this
 end
 
 /-- The product of two sets of unique differentiability is a set of unique differentiability. -/
@@ -339,9 +338,9 @@ begin
   assume x xs,
   rcases hs with ⟨y, hy⟩,
   suffices : y - x ∈ interior (tangent_cone_at ℝ s x),
-  { refine ⟨_, subset_closure xs⟩,
-    rw [submodule.eq_top_of_nonempty_interior' _ ⟨y - x, interior_mono submodule.subset_span this⟩,
-      submodule.top_coe, closure_univ]; apply_instance },
+  { refine ⟨dense.of_closure _, subset_closure xs⟩,
+    simp [(submodule.span ℝ (tangent_cone_at ℝ s x)).eq_top_of_nonempty_interior'
+      ⟨y - x, interior_mono submodule.subset_span this⟩] },
   rw [mem_interior_iff_mem_nhds] at hy ⊢,
   apply mem_sets_of_superset ((is_open_map_add_right (-x)).image_mem_nhds hy),
   rintros _ ⟨z, zs, rfl⟩,

src/analysis/normed_space/finite_dimension.lean

@@ -258,7 +258,7 @@ begin
   from metric.second_countable_of_countable_discretization
     (λ ε ε_pos, ⟨fin d → ℕ, by apply_instance, this ε ε_pos⟩),
   intros ε ε_pos,
-  obtain ⟨u : ℕ → F, hu : closure (range u) = univ⟩ := exists_dense_seq F,
+  obtain ⟨u : ℕ → F, hu : dense_range u⟩ := exists_dense_seq F,
   obtain ⟨v : fin d → E, hv : is_basis 𝕜 v⟩ := finite_dimensional.fin_basis 𝕜 E,
   obtain ⟨C : ℝ, C_pos : 0 < C,
           hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥φ (v i)∥ ≤ M) → ∥φ∥ ≤ C * M⟩ := hv.op_norm_le,
@@ -269,7 +269,7 @@ begin
     have : ∀ i, ∃ n, ∥φ (v i) - u n∥ ≤ ε/(2*C),
     { simp only [norm_sub_rev],
       intro i,
-      have : φ (v i) ∈ closure (range u), by simp [hu],
+      have : φ (v i) ∈ closure (range u) := hu _,
       obtain ⟨n, hn⟩ : ∃ n, ∥u n - φ (v i)∥ < ε / (2 * C),
       { rw mem_closure_iff_nhds_basis metric.nhds_basis_ball at this,
         specialize this (ε/(2*C)) hε2C,

src/geometry/manifold/mfderiv.lean

@@ -1230,10 +1230,17 @@ protected def mfderiv {x : M} (hx : x ∈ e.source) :
   end,
   .. mfderiv I I' e x }
 
+lemma mfderiv_bijective {x : M} (hx : x ∈ e.source) :
+  function.bijective (mfderiv I I' e x) :=
+(he.mfderiv hx).bijective
+
+lemma mfderiv_surjective {x : M} (hx : x ∈ e.source) :
+  function.surjective (mfderiv I I' e x) :=
+(he.mfderiv hx).surjective
 
 lemma range_mfderiv_eq_univ {x : M} (hx : x ∈ e.source) :
   range (mfderiv I I' e x) = univ :=
-(he.mfderiv hx).to_linear_equiv.to_equiv.range_eq_univ
+(he.mfderiv_surjective hx).range_eq
 
 lemma trans (he': e'.mdifferentiable I' I'') : (e.trans e').mdifferentiable I I'' :=
 begin
@@ -1313,16 +1320,15 @@ begin
     D₁.mono (by mfld_set_tac),
   -- The derivative `G'` is onto, as it is the derivative of a local diffeomorphism, the composition
   -- of the two charts and of `e`.
-  have C₁ : range (G' : E → E') = univ,
+  have C : dense_range (G' : E → E'),
   { have : G' = mfderiv I I' ((chart_at H z).symm ≫ₕ e ≫ₕ (chart_at H' x)) ((chart_at H z : M → H) z),
       by { rw (Diff.mdifferentiable_at Mmem).mfderiv, refl },
     rw this,
-    exact Diff.range_mfderiv_eq_univ Mmem },
-  have C₂ : closure (range (G' : E → E')) = univ, by rw [C₁, closure_univ],
+    exact (Diff.mfderiv_surjective Mmem).dense_range },
   -- key step: thanks to what we have proved about it, `G` preserves the unique derivative property
   have key : unique_diff_within_at 𝕜
     (G '' (F.symm ⁻¹' (s ∩ (e.source ∩ e ⁻¹' ((ext_chart_at I' x).source))) ∩ F.target))
-    (G (F z)) := D₂.unique_diff_within_at B C₂,
+    (G (F z)) := D₂.unique_diff_within_at B C,
   have : G (F z) = (ext_chart_at I' x) x, by { dsimp [G, F], simp only [hx.1] with mfld_simps },
   rw this at key,
   apply key.mono,

src/linear_algebra/basic.lean

@@ -924,17 +924,6 @@ span_eq_bot.trans $ by simp
 span_eq_of_le _ (image_subset _ subset_span) $ map_le_iff_le_comap.2 $
 span_le.2 $ image_subset_iff.1 subset_span
 
-lemma linear_eq_on (s : set M) {f g : M →ₗ[R] M₂} (H : ∀x∈s, f x = g x) {x} (h : x ∈ span R s) :
-  f x = g x :=
-by apply span_induction h H; simp {contextual := tt}
-
-lemma linear_map.ext_on {v : ι → M} {f g : M →ₗ[R] M₂} (hv : span R (range v) = ⊤)
-  (h : ∀i, f (v i) = g (v i)) : f = g :=
-begin
-  apply linear_map.ext (λ x, linear_eq_on (range v) _ (eq_top_iff'.1 hv _)),
-  exact (λ y hy, exists.elim (set.mem_range.1 hy) (λ i hi, by rw ←hi; exact h i))
-end
-
 lemma supr_eq_span {ι : Sort w} (p : ι → submodule R M) :
   (⨆ (i : ι), p i) = submodule.span R (⋃ (i : ι), ↑(p i)) :=
 le_antisymm
@@ -1140,6 +1129,33 @@ variables [semimodule R M] [semimodule R M₂] [semimodule R M₃]
 include R
 open submodule
 
+/-- If two linear maps are equal on a set `s`, then they are equal on `submodule.span s`.
+
+See also `linear_map.eq_on_span'` for a version using `set.eq_on`. -/
+lemma eq_on_span {s : set M} {f g : M →ₗ[R] M₂} (H : set.eq_on f g s) ⦃x⦄ (h : x ∈ span R s) :
+  f x = g x :=
+by apply span_induction h H; simp {contextual := tt}
+
+/-- If two linear maps are equal on a set `s`, then they are equal on `submodule.span s`.
+
+This version uses `set.eq_on`, and the hidden argument will expand to `h : x ∈ (span R s : set M)`.
+See `linear_map.eq_on_span` for a version that takes `h : x ∈ span R s` as an argument. -/
+lemma eq_on_span' {s : set M} {f g : M →ₗ[R] M₂} (H : set.eq_on f g s) :
+  set.eq_on f g (span R s : set M) :=
+eq_on_span H
+
+/-- If `s` generates the whole semimodule and linear maps `f`, `g` are equal on `s`, then they are
+equal. -/
+lemma ext_on {s : set M} {f g : M →ₗ[R] M₂} (hv : span R s = ⊤) (h : set.eq_on f g s) :
+  f = g :=
+linear_map.ext (λ x, eq_on_span h (eq_top_iff'.1 hv _))
+
+/-- If the range of `v : ι → M` generates the whole semimodule and linear maps `f`, `g` are equal at
+each `v i`, then they are equal. -/
+lemma ext_on_range {v : ι → M} {f g : M →ₗ[R] M₂} (hv : span R (set.range v) = ⊤)
+  (h : ∀i, f (v i) = g (v i)) : f = g :=
+ext_on hv (set.forall_range_iff.2 h)
+
 @[simp] lemma finsupp_sum {γ} [has_zero γ]
   (f : M →ₗ[R] M₂) {t : ι →₀ γ} {g : ι → γ → M} :
   f (t.sum g) = t.sum (λi d, f (g i d)) := f.map_sum

src/linear_algebra/basis.lean

@@ -104,7 +104,7 @@ lemma is_basis.total_comp_repr : (finsupp.total ι M R v).comp hv.repr = linear_
 linear_map.ext hv.total_repr
 
 lemma is_basis.ext {f g : M →ₗ[R] M'} (hv : is_basis R v) (h : ∀i, f (v i) = g (v i)) : f = g :=
-linear_map.ext_on hv.2 h
+linear_map.ext_on_range hv.2 h
 
 lemma is_basis.repr_ker : hv.repr.ker = ⊥ :=
 linear_map.ker_eq_bot.2 $ left_inverse.injective hv.total_repr

src/measure_theory/simple_func_dense.lean

@@ -134,7 +134,7 @@ lemma tendsto_approx_on {f : β → α} (hf : measurable f) {s : set α} {y₀ :
   tendsto (λ n, approx_on f hf s y₀ h₀ n x) at_top (𝓝 $ f x) :=
 begin
   haveI : nonempty s := ⟨⟨y₀, h₀⟩⟩,
-  rw [← @subtype.range_coe _ s, ← image_univ, ← dense_seq_dense s] at hx,
+  rw [← @subtype.range_coe _ s, ← image_univ, ← (dense_range_dense_seq s).closure_eq] at hx,
   simp only [approx_on, coe_comp],
   refine tendsto_nearest_pt (closure_minimal _ is_closed_closure hx),
   simp only [nat.range_cases_on, closure_union, range_comp coe],

src/topology/algebra/module.lean

@@ -238,6 +238,19 @@ lemma map_sum {ι : Type*} (s : finset ι) (g : ι → M) :
 
 @[simp, norm_cast] lemma coe_coe : ((f : M →ₗ[R] M₂) : (M → M₂)) = (f : M → M₂) := rfl
 
+/-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure
+of the `submodule.span` of this set. -/
+lemma eq_on_closure_span [t2_space M₂] {s : set M} {f g : M →L[R] M₂} (h : set.eq_on f g s) :
+  set.eq_on f g (closure (submodule.span R s : set M)) :=
+(linear_map.eq_on_span' h).closure f.continuous g.continuous
+
+/-- If the submodule generated by a set `s` is dense in the ambient semimodule, then two continuous
+linear maps equal on `s` are equal. -/
+lemma ext_on [t2_space M₂] {s : set M} (hs : dense (submodule.span R s : set M)) {f g : M →L[R] M₂}
+  (h : set.eq_on f g s) :
+  f = g :=
+ext $ λ x, eq_on_closure_span h (hs x)
+
 /-- The continuous map that is constantly zero. -/
 instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_const⟩⟩
 instance : inhabited (M →L[R] M₂) := ⟨0⟩

src/topology/bases.lean

@@ -108,42 +108,55 @@ let ⟨S, sb, su⟩ := sUnion_basis_of_is_open hB ou in
 
 variables (α)
 
-/-- A separable space is one with a countable dense subset. -/
+/-- A separable space is one with a countable dense subset, available through
+`topological_space.exists_countable_dense`. If `α` is also known to be nonempty, then
+`topological_space.dense_seq` provides a sequence `ℕ → α` with dense range, see
+`topological_space.dense_range_dense_seq`.
+
+If `α` is a uniform space with countably generated uniformity filter (e.g., an `emetric_space`),
+then this condition is equivalent to `topological_space.second_countable_topology α`. In this case
+the latter should be used as a typeclass argument in theorems because Lean can automatically deduce
+`separable_space` from `second_countable_topology` but it can't deduce `second_countable_topology`
+and `emetric_space`. -/
 class separable_space : Prop :=
-(exists_countable_closure_eq_univ : ∃s:set α, countable s ∧ closure s = univ)
-
-lemma exists_countable_closure_eq_univ [separable_space α] :
-  ∃ s : set α, countable s ∧ closure s = univ :=
-separable_space.exists_countable_closure_eq_univ
+(exists_countable_dense : ∃s:set α, countable s ∧ dense s)
 
 lemma exists_countable_dense [separable_space α] :
   ∃ s : set α, countable s ∧ dense s :=
-let ⟨s, hsc, hsd⟩ := exists_countable_closure_eq_univ α
-  in ⟨s, hsc, dense_iff_closure_eq.2 hsd⟩
+separable_space.exists_countable_dense
+
+/-- A nonempty separable space admits a sequence with dense range. Instead of running `cases` on the
+conclusion of this lemma, you might want to use `topological_space.dense_seq` and
+`topological_space.dense_range_dense_seq`.
 
-lemma exists_dense_seq [separable_space α] [nonempty α] : ∃ u : ℕ → α, closure (range u) = univ :=
+If `α` might be empty, then `exists_countable_dense` is the main way to use separability of `α`. -/
+lemma exists_dense_seq [separable_space α] [nonempty α] : ∃ u : ℕ → α, dense_range u :=
 begin
-  obtain ⟨s : set α, hs, s_dense⟩ := @separable_space.exists_countable_closure_eq_univ α _ _,
+  obtain ⟨s : set α, hs, s_dense⟩ := exists_countable_dense α,
   cases countable_iff_exists_surjective.mp hs with u hu,
-  use u,
-  apply eq_univ_of_univ_subset,
-  simpa [s_dense] using closure_mono hu
+  exact ⟨u, s_dense.mono hu⟩,
 end
 
-/-- A sequence dense in a non-empty separable topological space. -/
+/-- A sequence dense in a non-empty separable topological space.
+
+If `α` might be empty, then `exists_countable_dense` is the main way to use separability of `α`. -/
 def dense_seq [separable_space α] [nonempty α] : ℕ → α := classical.some (exists_dense_seq α)
 
-@[simp] lemma dense_seq_dense [separable_space α] [nonempty α] :
-  closure (range $ dense_seq α) = univ := classical.some_spec (exists_dense_seq α)
+/-- The sequence `dense_seq α` has dense range. -/
+@[simp] lemma dense_range_dense_seq [separable_space α] [nonempty α] :
+  dense_range (dense_seq α) := classical.some_spec (exists_dense_seq α)
 
 end topological_space
 
 open topological_space
 
-lemma dense_range.separable_space {α β : Type*} [topological_space α] [separable_space α]
-  [topological_space β] {f : α → β} (h : dense_range f) (h' : continuous f) : separable_space β :=
-let ⟨s, s_cnt, s_cl⟩ := exists_countable_closure_eq_univ α in
-⟨⟨f '' s, countable.image s_cnt f, h'.dense_image_of_dense_range h (dense_iff_closure_eq.mpr s_cl)⟩⟩
+/-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is
+a separable space as well. E.g., the completion of a separable uniform space is separable. -/
+protected lemma dense_range.separable_space {α β : Type*} [topological_space α] [separable_space α]
+  [topological_space β] {f : α → β} (h : dense_range f) (h' : continuous f) :
+  separable_space β :=
+let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α in
+⟨⟨f '' s, countable.image s_cnt f, h.dense_image h' s_dense⟩⟩
 
 namespace topological_space
 universe u
@@ -253,8 +266,7 @@ begin
   have : ∀ s ∈ b, set.nonempty s :=
     assume s hs, ne_empty_iff_nonempty.1 $ λ eq, absurd hs (eq.symm ▸ hbne),
   choose f hf,
-  refine ⟨⟨⋃ s ∈ b, {f s ‹_›}, hbc.bUnion (λ _ _, countable_singleton _), _⟩⟩,
-  refine eq_univ_of_forall (λ a, _),
+  refine ⟨⟨⋃ s ∈ b, {f s ‹_›}, hbc.bUnion (λ _ _, countable_singleton _), λ a, _⟩⟩,
   suffices : (⨅ s ∈ S a, 𝓟 (s ∩ ⋃ t ∈ b, {f t ‹_›})).ne_bot,
   { obtain ⟨t, htb, hta⟩ : a ∈ ⋃₀ b, { simp only [hbU] },
     have A : ∃ s, s ∈ S a := ⟨t, hta, htb⟩,