refactor(topology/dense_embedding): simplify proof (leanprover-commun…

…ity#3329)

Using filter bases, we can give a cleaner proof of continuity of extension by continuity. Also switch to use the "new" `continuous_at` in the statement.

src/topology/basic.lean

@@ -471,6 +471,17 @@ lemma mem_nhds_sets {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
   s ∈ 𝓝 a :=
 mem_nhds_sets_iff.2 ⟨s, subset.refl _, hs, ha⟩
 
+lemma nhds_basis_opens' (a : α) : (𝓝 a).has_basis (λ s : set α, s ∈ 𝓝 a ∧ is_open s) (λ x, x) :=
+begin
+  convert nhds_basis_opens a,
+  ext s,
+  split,
+  { rintros ⟨s_in, s_op⟩,
+    exact ⟨mem_of_nhds s_in, s_op⟩ },
+  { rintros ⟨a_in, s_op⟩,
+    exact ⟨mem_nhds_sets s_op a_in, s_op⟩ },
+end
+
 /-- If a predicate is true in a neighbourhood of `a`, then for `y` sufficiently close
 to `a` this predicate is true in a neighbourhood of `y`. -/
 lemma filter.eventually.eventually_nhds {p : α → Prop} {a : α} (h : ∀ᶠ y in 𝓝 a, p y) :

src/topology/dense_embedding.lean

@@ -173,46 +173,36 @@ lemma extend_eq_of_cont [t2_space γ] {f : α → γ} (hf : continuous f) (a : 
   di.extend f (i a) = f a :=
 di.extend_e_eq a (continuous_iff_continuous_at.1 hf a)
 
-lemma tendsto_extend [regular_space γ] {b : β} {f : α → γ} (di : dense_inducing i)
-  (hf : {b | ∃c, tendsto f (comap i $ 𝓝 b) (𝓝 c)} ∈ 𝓝 b) :
-  tendsto (di.extend f) (𝓝 b) (𝓝 (di.extend f b)) :=
-let φ := {b | tendsto f (comap i $ 𝓝 b) (𝓝 $ di.extend f b)} in
-have hφ : φ ∈ 𝓝 b,
-  from (𝓝 b).sets_of_superset hf $ assume b ⟨c, hc⟩,
-    show tendsto f (comap i (𝓝 b)) (𝓝 (di.extend f b)), from (di.extend_eq hc).symm ▸ hc,
-assume s hs,
-let ⟨s'', hs''₁, hs''₂, hs''₃⟩ := nhds_is_closed hs in
-let ⟨s', hs'₁, (hs'₂ : i ⁻¹' 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 '' (i ⁻¹' s')) ⊆ s'',
-  by rw [hs''₃.closure_subset_iff, image_subset_iff]; exact hs'₂,
-have h₂ : t ⊆ di.extend f ⁻¹' closure (f '' (i ⁻¹' t)), from
-  assume b' hb',
-  have 𝓝 b' ≤ 𝓟 t, by simp; exact mem_nhds_sets ht₂ hb',
-  have map f (comap i (𝓝 b')) ≤ 𝓝 (di.extend f b') ⊓ 𝓟 (f '' (i ⁻¹' t)),
-    from calc _ ≤ map f (comap i (𝓝 b' ⊓ 𝓟 t)) : map_mono $ comap_mono $ le_inf (le_refl _) this
-      ... ≤ map f (comap i (𝓝 b')) ⊓ map f (comap i (𝓟 t)) :
-        le_inf (map_mono $ comap_mono $ inf_le_left) (map_mono $ comap_mono $ inf_le_right)
-      ... ≤ map f (comap i (𝓝 b')) ⊓ 𝓟 (f '' (i ⁻¹' t)) : by simp [le_refl]
-      ... ≤ _ : inf_le_inf_right _ (ht₁ hb').left,
-  show di.extend f b' ∈ closure (f '' (i ⁻¹' t)),
-  begin
-    rw [closure_eq_cluster_pts],
-    apply ne_bot_of_le_ne_bot _ this,
-    simp,
-    exact di.comap_nhds_ne_bot
-  end,
-(𝓝 b).sets_of_superset
-  (show t ∈ 𝓝 b, from mem_nhds_sets ht₂ ht₃)
-  (calc t ⊆ di.extend f ⁻¹' closure (f '' (i ⁻¹' t)) : h₂
-    ... ⊆ di.extend f ⁻¹' closure (f '' (i ⁻¹' s')) :
-      preimage_mono $ closure_mono $ image_subset f $ preimage_mono $ subset.trans ht₁ $ inter_subset_right _ _
-    ... ⊆ di.extend f ⁻¹' s'' : preimage_mono h₁
-    ... ⊆ di.extend f ⁻¹' s : preimage_mono hs''₂)
+lemma continuous_at_extend [regular_space γ] {b : β} {f : α → γ} (di : dense_inducing i)
+  (hf : ∀ᶠ x in 𝓝 b, ∃c, tendsto f (comap i $ 𝓝 x) (𝓝 c)) :
+  continuous_at (di.extend f) b :=
+begin
+  set φ := di.extend f,
+  suffices : ∀ V' ∈ 𝓝 (φ b), is_closed V' → φ ⁻¹' V' ∈ 𝓝 b,
+    by simpa [continuous_at, (closed_nhds_basis _).tendsto_right_iff],
+  intros V' V'_in V'_closed,
+  set V₁ := {x | tendsto f (comap i $ 𝓝 x) (𝓝 $ φ x)},
+  have V₁_in : V₁ ∈ 𝓝 b,
+  { filter_upwards [hf],
+    rintros x ⟨c, hc⟩,
+    change tendsto f (comap i (𝓝 x)) (𝓝 (φ x)),
+    convert hc,
+    exact di.extend_eq hc },
+  obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, is_open V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V',
+  { simpa [and_assoc] using ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp
+                            (mem_of_nhds V₁_in : b ∈ V₁) V' V'_in },
+  suffices : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V',
+  { filter_upwards [inter_mem_sets V₁_in V₂_in], exact this },
+  rintros x ⟨x_in₁, x_in₂⟩,
+  have hV₂x : V₂ ∈ 𝓝 x := mem_nhds_sets V₂_op x_in₂,
+  apply mem_of_closed_of_tendsto (comap_nhds_ne_bot di) x_in₁ V'_closed,
+  use V₂,
+  tauto,
+end
 
 lemma continuous_extend [regular_space γ] {f : α → γ} (di : dense_inducing i)
   (hf : ∀b, ∃c, tendsto f (comap i (𝓝 b)) (𝓝 c)) : continuous (di.extend f) :=
-continuous_iff_continuous_at.mpr $ assume b, di.tendsto_extend $ univ_mem_sets' hf
+continuous_iff_continuous_at.mpr $ assume b, di.continuous_at_extend $ univ_mem_sets' hf
 
 lemma mk'
   (i : α → β)

src/topology/separation.lean

@@ -388,6 +388,11 @@ let ⟨t, ht₁, ht₂, ht₃⟩ := this in
   subset.trans (compl_subset_comm.1 ht₂) h₁,
   is_closed_compl_iff.mpr ht₁⟩
 
+lemma closed_nhds_basis [regular_space α] (a : α) :
+  (𝓝 a).has_basis (λ s : set α, s ∈ 𝓝 a ∧ is_closed s) id :=
+⟨λ t, ⟨λ t_in, let ⟨s, s_in, h_st, h⟩ := nhds_is_closed t_in in ⟨s, ⟨s_in, h⟩, h_st⟩,
+       λ ⟨s, ⟨s_in, hs⟩, hst⟩, mem_sets_of_superset s_in hst⟩⟩
+
 instance subtype.regular_space [regular_space α] {p : α → Prop} : regular_space (subtype p) :=
 ⟨begin
    intros s a hs ha,