refactor(topology/continuity): remove inhabited from dense extend

analysis/topology/continuity.lean

@@ -838,40 +838,45 @@ have t ∩ range e ∈ (nhds b ⊓ principal (range e)).sets,
 let ⟨_, ⟨hx₁, y, rfl⟩⟩ := inhabited_of_mem_sets de.nhds_inf_neq_bot this in
 subset_ne_empty hs $ ne_empty_of_mem hx₁
 
-variables [topological_space γ] [inhabited γ] [regular_space γ]
+variables [topological_space γ]
 /-- If `e : α → β` is a dense embedding, then any function `α → γ` extends to a function `β → γ`. -/
-def ext (de : dense_embedding e) (f : α → γ) : β → γ := lim ∘ map f ∘ vmap e ∘ nhds
+def extend (de : dense_embedding e) (f : α → γ) (b : β) : γ :=
+have nonempty γ, from
+let ⟨_, ⟨_, a, _⟩⟩ := exists_mem_of_ne_empty
+  (mem_closure_iff.1 (de.dense b) _ is_open_univ trivial) in ⟨f a⟩,
+@lim _ (classical.inhabited_of_nonempty this) _ (map f (vmap e (nhds b)))
 
-lemma ext_eq {b : β} {c : γ} {f : α → γ} (hf : map f (vmap e (nhds b)) ≤ nhds c) : de.ext f b = c :=
-lim_eq begin simp; exact vmap_nhds_neq_bot de end hf
+lemma extend_eq [t2_space γ] {b : β} {c : γ} {f : α → γ}
+  (hf : map f (vmap e (nhds b)) ≤ nhds c) : de.extend f b = c :=
+@lim_eq _ (id _) _ _ _ _ (by simp; exact vmap_nhds_neq_bot de) hf
 
-lemma ext_e_eq {a : α} {f : α → γ} (de : dense_embedding e)
-  (hf : map f (nhds a) ≤ nhds (f a)) : de.ext f (e a) = f a :=
-de.ext_eq begin rw de.induced; exact hf end
+lemma extend_e_eq [t2_space γ] {a : α} {f : α → γ} (de : dense_embedding e)
+  (hf : map f (nhds a) ≤ nhds (f a)) : de.extend f (e a) = f a :=
+de.extend_eq begin rw de.induced; exact hf end
 
-lemma tendsto_ext {b : β} {f : α → γ} (de : dense_embedding e)
+lemma tendsto_extend [regular_space γ] {b : β} {f : α → γ} (de : dense_embedding e)
   (hf : {b | ∃c, tendsto f (vmap e $ nhds b) (nhds c)} ∈ (nhds b).sets) :
-  tendsto (de.ext f) (nhds b) (nhds (de.ext f b)) :=
-let φ := {b | tendsto f (vmap e $ nhds b) (nhds $ de.ext f b)} in
+  tendsto (de.extend f) (nhds b) (nhds (de.extend f b)) :=
+let φ := {b | tendsto f (vmap e $ nhds b) (nhds $ de.extend f b)} in
 have hφ : φ ∈ (nhds b).sets,
   from (nhds b).upwards_sets hf $ assume b ⟨c, hc⟩,
-    show tendsto f (vmap e (nhds b)) (nhds (de.ext f b)), from (de.ext_eq hc).symm ▸ hc,
+    show tendsto f (vmap e (nhds b)) (nhds (de.extend f b)), from (de.extend_eq hc).symm ▸ hc,
 assume s hs,
 let ⟨s'', hs''₁, hs''₂, hs''₃⟩ := nhds_is_closed hs in
 let ⟨s', hs'₁, (hs'₂ : e ⁻¹' s' ⊆ f ⁻¹' s'')⟩ := mem_of_nhds hφ hs''₁ in
 let ⟨t, (ht₁ : t ⊆ φ ∩ s'), ht₂, ht₃⟩ := mem_nhds_sets_iff.mp $ inter_mem_sets hφ hs'₁ in
 have h₁ : closure (f '' (e ⁻¹' s')) ⊆ s'',
   by rw [closure_subset_iff_subset_of_is_closed hs''₃, image_subset_iff]; exact hs'₂,
-have h₂ : t ⊆ de.ext f ⁻¹' closure (f '' (e ⁻¹' t)), from
+have h₂ : t ⊆ de.extend f ⁻¹' closure (f '' (e ⁻¹' t)), from
   assume b' hb',
   have nhds b' ≤ principal t, by simp; exact mem_nhds_sets ht₂ hb',
-  have map f (vmap e (nhds b')) ≤ nhds (de.ext f b') ⊓ principal (f '' (e ⁻¹' t)),
+  have map f (vmap e (nhds b')) ≤ nhds (de.extend f b') ⊓ principal (f '' (e ⁻¹' t)),
     from calc _ ≤ map f (vmap e (nhds b' ⊓ principal t)) : map_mono $ vmap_mono $ le_inf (le_refl _) this
       ... ≤ map f (vmap e (nhds b')) ⊓ map f (vmap e (principal t)) :
         le_inf (map_mono $ vmap_mono $ inf_le_left) (map_mono $ vmap_mono $ inf_le_right)
       ... ≤ map f (vmap e (nhds b')) ⊓ principal (f '' (e ⁻¹' t)) : by simp [le_refl]
       ... ≤ _ : inf_le_inf ((ht₁ hb').left) (le_refl _),
-  show de.ext f b' ∈ closure (f '' (e ⁻¹' t)),
+  show de.extend f b' ∈ closure (f '' (e ⁻¹' t)),
   begin
     rw [closure_eq_nhds],
     apply neq_bot_of_le_neq_bot _ this,
@@ -880,15 +885,15 @@ have h₂ : t ⊆ de.ext f ⁻¹' closure (f '' (e ⁻¹' t)), from
   end,
 (nhds b).upwards_sets
   (show t ∈ (nhds b).sets, from mem_nhds_sets ht₂ ht₃)
-  (calc t ⊆ de.ext f ⁻¹' closure (f '' (e ⁻¹' t)) : h₂
-    ... ⊆ de.ext f ⁻¹' closure (f '' (e ⁻¹' s')) :
+  (calc t ⊆ de.extend f ⁻¹' closure (f '' (e ⁻¹' t)) : h₂
+    ... ⊆ de.extend f ⁻¹' closure (f '' (e ⁻¹' s')) :
       preimage_mono $ closure_mono $ image_subset f $ preimage_mono $ subset.trans ht₁ $ inter_subset_right _ _
-    ... ⊆ de.ext f ⁻¹' s'' : preimage_mono h₁
-    ... ⊆ de.ext f ⁻¹' s : preimage_mono hs''₂)
+    ... ⊆ de.extend f ⁻¹' s'' : preimage_mono h₁
+    ... ⊆ de.extend f ⁻¹' s : preimage_mono hs''₂)
 
-lemma continuous_ext {f : α → γ} (de : dense_embedding e)
-  (hf : ∀b, ∃c, tendsto f (vmap e (nhds b)) (nhds c)) : continuous (de.ext f) :=
-continuous_iff_tendsto.mpr $ assume b, de.tendsto_ext $ univ_mem_sets' hf
+lemma continuous_extend [regular_space γ] {f : α → γ} (de : dense_embedding e)
+  (hf : ∀b, ∃c, tendsto f (vmap e (nhds b)) (nhds c)) : continuous (de.extend f) :=
+continuous_iff_tendsto.mpr $ assume b, de.tendsto_extend $ univ_mem_sets' hf
 
 end dense_embedding
 

analysis/topology/uniform_space.lean

@@ -1032,13 +1032,12 @@ variables
   (h_dense : ∀x, x ∈ closure (range e))
   {f : β → γ}
   (h_f : uniform_continuous f)
-  [inhabited γ]
 
-local notation `ψ` := (h_e.dense_embedding h_dense).ext f
+local notation `ψ` := (h_e.dense_embedding h_dense).extend f
 
 lemma uniformly_extend_of_emb [cγ : complete_space γ] [sγ : separated γ] {b : β} :
   ψ (e b) = f b :=
-dense_embedding.ext_e_eq _ $ continuous_iff_tendsto.mp h_f.continuous b
+dense_embedding.extend_e_eq _ $ continuous_iff_tendsto.mp h_f.continuous b
 
 lemma uniformly_extend_exists [complete_space γ] [sγ : separated γ] {a : α} :
   ∃c, tendsto f (vmap e (nhds a)) (nhds c) :=
@@ -1052,7 +1051,7 @@ complete_space.complete this
 
 lemma uniformly_extend_spec [complete_space γ] [sγ : separated γ] {a : α} :
   tendsto f (vmap e (nhds a)) (nhds (ψ a)) :=
-lim_spec $ uniformly_extend_exists h_e h_dense h_f
+@lim_spec _ (id _) _ _ $ uniformly_extend_exists h_e h_dense h_f
 
 lemma uniform_continuous_uniformly_extend [cγ : complete_space γ] [sγ : separated γ] :
   uniform_continuous ψ :=