chore(topology/basic): add cluster_pt.map, rename mem_closure (#5065

)

* add `filter.prod_pure`, `filter.pure_prod`, `cluster_pt.map`, and `set.maps_to.closure`;
* rename `mem_closure` to `map_mem_closure`;
* rename `mem_closure2` to `map_mem_closure2`.

src/order/filter/basic.lean

@@ -2286,8 +2286,14 @@ by simp only [filter.prod, comap_inf, inf_comm, inf_assoc, inf_left_comm]
   (𝓟 s) ×ᶠ (𝓟 t) = 𝓟 (set.prod s t) :=
 by simp only [filter.prod, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; refl
 
-@[simp] lemma prod_pure_pure {a : α} {b : β} : (pure a) ×ᶠ (pure b) = pure (a, b) :=
-by simp only [← principal_singleton, prod_principal_principal, singleton_prod_singleton]
+@[simp] lemma pure_prod {a : α} {f : filter β} : pure a ×ᶠ f = map (prod.mk a) f :=
+by rw [prod_eq, map_pure, pure_seq_eq_map]
+
+@[simp] lemma prod_pure {f : filter α} {b : β} : f ×ᶠ pure b = map (λ a, (a, b)) f :=
+by rw [prod_eq, seq_pure, map_map]
+
+lemma prod_pure_pure {a : α} {b : β} : (pure a) ×ᶠ (pure b) = pure (a, b) :=
+by simp
 
 lemma prod_eq_bot {f : filter α} {g : filter β} : f ×ᶠ g = ⊥ ↔ (f = ⊥ ∨ g = ⊥) :=
 begin

src/topology/algebra/ring.lean

@@ -52,10 +52,10 @@ def ideal.closure (S : ideal α) : ideal α :=
 { carrier := closure S,
   zero_mem' := subset_closure S.zero_mem,
   add_mem'  := assume x y hx hy,
-    mem_closure2 continuous_add hx hy $ assume a b, S.add_mem,
+    map_mem_closure2 continuous_add hx hy $ assume a b, S.add_mem,
   smul_mem'  := assume c x hx,
     have continuous (λx:α, c * x) := continuous_const.mul continuous_id,
-    mem_closure this hx $ assume a, S.mul_mem_left }
+    map_mem_closure this hx $ assume a, S.mul_mem_left }
 
 @[simp] lemma ideal.coe_closure (S : ideal α) :
   (S.closure : set α) = closure S := rfl

src/topology/basic.lean

@@ -14,7 +14,7 @@ noncomputable theory
 The main definition is the type class `topological space α` which endows a type `α` with a topology.
 Then `set α` gets predicates `is_open`, `is_closed` and functions `interior`, `closure` and
 `frontier`. Each point `x` of `α` gets a neighborhood filter `𝓝 x`. A filter `F` on `α` has
-`x` as a cluster point if `is_cluster_pt x F : 𝓝 x ⊓ F ≠ ⊥`. A map `f : ι → α` clusters at `x`
+`x` as a cluster point if `cluster_pt x F : 𝓝 x ⊓ F ≠ ⊥`. A map `f : ι → α` clusters at `x`
 along `F : filter ι` if `map_cluster_pt x F f : cluster_pt x (map f F)`. In particular
 the notion of cluster point of a sequence `u` is `map_cluster_pt x at_top u`.
 
@@ -969,6 +969,11 @@ lemma continuous_at.preimage_mem_nhds {f : α → β} {x : α} {t : set β} (h :
   (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x :=
 h ht
 
+lemma cluster_pt.map {x : α} {la : filter α} {lb : filter β} (H : cluster_pt x la)
+  {f : α → β} (hfc : continuous_at f x) (hf : tendsto f la lb) :
+  cluster_pt (f x) lb :=
+ne_bot_of_le_ne_bot ((map_ne_bot_iff f).2 H) $ hfc.tendsto.inf hf
+
 lemma preimage_interior_subset_interior_preimage {f : α → β} {s : set β}
   (hf : continuous f) : f⁻¹' (interior s) ⊆ interior (f⁻¹' s) :=
 interior_maximal (preimage_mono interior_subset) (is_open_interior.preimage hf)
@@ -1110,23 +1115,21 @@ begin
   apply h', rw mem_nhds_sets_iff, exact ⟨s, set.subset.refl _, os, ys⟩
 end
 
+/-- If a continuous map `f` maps `s` to `t`, then it maps `closure s` to `closure t`. -/
+lemma set.maps_to.closure {s : set α} {t : set β} {f : α → β} (h : maps_to f s t)
+  (hc : continuous f) : maps_to f (closure s) (closure t) :=
+begin
+  simp only [maps_to, mem_closure_iff_cluster_pt],
+  exact λ x hx, hx.map hc.continuous_at (tendsto_principal_principal.2 h)
+end
+
 lemma image_closure_subset_closure_image {f : α → β} {s : set α} (h : continuous f) :
   f '' closure s ⊆ closure (f '' s) :=
-have ∀ (a : α), cluster_pt a (𝓟 s) → cluster_pt (f a) (𝓟 (f '' s)),
-  from assume a ha,
-  have h₁ : ¬ map f (𝓝 a ⊓ 𝓟 s) = ⊥,
-    by rwa[map_eq_bot_iff],
-  have h₂ : map f (𝓝 a ⊓ 𝓟 s) ≤ 𝓝 (f a) ⊓ 𝓟 (f '' s),
-    from le_inf
-      (le_trans (map_mono inf_le_left) $ by rw [continuous_iff_continuous_at] at h; exact h a)
-      (le_trans (map_mono inf_le_right) $ by simp [subset_preimage_image] ),
-  ne_bot_of_le_ne_bot h₁ h₂,
-by simp [image_subset_iff, closure_eq_cluster_pts]; assumption
-
-lemma mem_closure {s : set α} {t : set β} {f : α → β} {a : α}
+((maps_to_image f s).closure h).image_subset
+
+lemma map_mem_closure {s : set α} {t : set β} {f : α → β} {a : α}
   (hf : continuous f) (ha : a ∈ closure s) (ht : ∀a∈s, f a ∈ t) : f a ∈ closure t :=
-subset.trans (image_closure_subset_closure_image hf) (closure_mono $ image_subset_iff.2 ht) $
-  (mem_image_of_mem f ha)
+set.maps_to.closure ht hf ha
 
 /-!
 ### Function with dense range

src/topology/constructions.lean

@@ -303,13 +303,13 @@ have (𝓝 a ×ᶠ 𝓝 b) ⊓ 𝓟 (set.prod s t) = (𝓝 a ⊓ 𝓟 s) ×ᶠ (
   by rw [←prod_inf_prod, prod_principal_principal],
 by simp [closure_eq_cluster_pts, cluster_pt, nhds_prod_eq, this]; exact prod_ne_bot
 
-lemma mem_closure2 {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β}
+lemma map_mem_closure2 {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β}
   (hf : continuous (λp:α×β, f p.1 p.2)) (ha : a ∈ closure s) (hb : b ∈ closure t)
   (hu : ∀a b, a ∈ s → b ∈ t → f a b ∈ u) :
   f a b ∈ closure u :=
 have (a, b) ∈ closure (set.prod s t), by rw [closure_prod_eq]; from ⟨ha, hb⟩,
 show (λp:α×β, f p.1 p.2) (a, b) ∈ closure u, from
-  mem_closure hf this $ assume ⟨a, b⟩ ⟨ha, hb⟩, hu a b ha hb
+  map_mem_closure hf this $ assume ⟨a, b⟩ ⟨ha, hb⟩, hu a b ha hb
 
 lemma is_closed.prod {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
   is_closed (set.prod s₁ s₂) :=

src/topology/metric_space/basic.lean

@@ -1475,7 +1475,7 @@ begin
     intros x y x_in y_in,
     exact this (x, y) (mk_mem_prod x_in y_in) },
   intros p p_in,
-  have := mem_closure continuous_dist p_in h,
+  have := map_mem_closure continuous_dist p_in h,
   rwa (is_closed_le' C).closure_eq at this
 end