chore(topology/maps): add tendsto_nhds_iff lemmas (#8693)

This adds lemmas of the form `something.tendsto_nhds_iff` to ease use.

I also had to get lemmas out of a section because `α` was duplicated and that caused typechecking problems.

src/topology/maps.lean

@@ -146,7 +146,7 @@ hf.1.map_nhds_of_mem a h
 lemma embedding.tendsto_nhds_iff {ι : Type*}
   {f : ι → β} {g : β → γ} {a : filter ι} {b : β} (hg : embedding g) :
   tendsto f a (𝓝 b) ↔ tendsto (g ∘ f) a (𝓝 (g b)) :=
-by rw [tendsto, tendsto, hg.induced, nhds_induced, ← map_le_iff_le_comap, filter.map_map]
+hg.to_inducing.tendsto_nhds_iff
 
 lemma embedding.continuous_iff {f : α → β} {g : β → γ} (hg : embedding g) :
   continuous f ↔ continuous (g ∘ f) :=
@@ -341,6 +341,11 @@ lemma open_embedding.open_iff_image_open {f : α → β} (hf : open_embedding f)
    apply preimage_image_eq _ hf.inj
  end⟩
 
+lemma open_embedding.tendsto_nhds_iff {ι : Type*}
+  {f : ι → β} {g : β → γ} {a : filter ι} {b : β} (hg : open_embedding g) :
+  tendsto f a (𝓝 b) ↔ tendsto (g ∘ f) a (𝓝 (g b)) :=
+hg.to_embedding.tendsto_nhds_iff
+
 lemma open_embedding.continuous {f : α → β} (hf : open_embedding f) : continuous f :=
 hf.to_embedding.continuous
 
@@ -386,6 +391,11 @@ structure closed_embedding (f : α → β) extends embedding f : Prop :=
 
 variables {f : α → β}
 
+lemma closed_embedding.tendsto_nhds_iff {ι : Type*}
+  {g : ι → α} {a : filter ι} {b : α} (hf : closed_embedding f) :
+  tendsto g a (𝓝 b) ↔ tendsto (f ∘ g) a (𝓝 (f b)) :=
+hf.to_embedding.tendsto_nhds_iff
+
 lemma closed_embedding.continuous (hf : closed_embedding f) : continuous f :=
 hf.to_embedding.continuous
 

src/topology/metric_space/isometry.lean

@@ -23,6 +23,7 @@ universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 open function set
+open_locale topological_space
 
 /-- An isometry (also known as isometric embedding) is a map preserving the edistance
 between pseudoemetric spaces, or equivalently the distance between pseudometric space.  -/
@@ -45,7 +46,7 @@ theorem isometry.dist_eq [pseudo_metric_space α] [pseudo_metric_space β] {f :
   (hf : isometry f) (x y : α) : dist (f x) (f y) = dist x y :=
 by rw [dist_edist, dist_edist, hf]
 
-section emetric_isometry
+section pseudo_emetric_isometry
 
 variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ]
 variables {f : α → β} {x y z : α}  {s : set α}
@@ -80,17 +81,6 @@ theorem isometry.uniform_inducing (hf : isometry f) :
   uniform_inducing f :=
 hf.antilipschitz.uniform_inducing hf.lipschitz.uniform_continuous
 
-/-- An isometry from a metric space is a uniform embedding -/
-theorem isometry.uniform_embedding {α : Type u} {β : Type v} [emetric_space α]
-  [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :
-  uniform_embedding f :=
-hf.antilipschitz.uniform_embedding hf.lipschitz.uniform_continuous
-
-/-- An isometry from a complete emetric space is a closed embedding -/
-theorem isometry.closed_embedding {α : Type u} {β : Type v} [emetric_space α] [complete_space α]
-  [emetric_space β] {f : α → β} (hf : isometry f) : closed_embedding f :=
-hf.antilipschitz.closed_embedding hf.lipschitz.uniform_continuous
-
 /-- An isometry is continuous. -/
 lemma isometry.continuous (hf : isometry f) : continuous f :=
 hf.lipschitz.continuous
@@ -123,6 +113,26 @@ lemma isometry.comp_continuous_iff {γ} [topological_space γ] (hf : isometry f)
   continuous (f ∘ g) ↔ continuous g :=
 hf.uniform_inducing.inducing.continuous_iff.symm
 
+end pseudo_emetric_isometry --section
+
+section emetric_isometry
+variables [emetric_space α]
+
+/-- An isometry from a metric space is a uniform embedding -/
+theorem isometry.uniform_embedding [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :
+  uniform_embedding f :=
+hf.antilipschitz.uniform_embedding hf.lipschitz.uniform_continuous
+
+/-- An isometry from a complete emetric space is a closed embedding -/
+theorem isometry.closed_embedding [complete_space α] [emetric_space β]
+  {f : α → β} (hf : isometry f) : closed_embedding f :=
+hf.antilipschitz.closed_embedding hf.lipschitz.uniform_continuous
+
+lemma isometry.tendsto_nhds_iff [complete_space α] [emetric_space β] {ι : Type*} {f : α → β}
+  {g : ι → α} {a : filter ι} {b : α} (hf : isometry f) :
+  filter.tendsto g a (𝓝 b) ↔ filter.tendsto (f ∘ g) a (𝓝 (f b)) :=
+hf.closed_embedding.tendsto_nhds_iff
+
 end emetric_isometry --section
 
 /-- An isometry preserves the diameter in pseudometric spaces. -/