feat(topology/metric_space/isometry): use namespace, add lemmas (#15591)

* Use `namespace isometry`.
* Add lemmas like `isometry.preimage_ball`.

src/analysis/normed/group/add_torsor.lean

@@ -74,7 +74,7 @@ by rw [dist_comm, dist_vadd_left]
 addition/subtraction of `x : P`. -/
 @[simps] def isometric.vadd_const (x : P) : V ≃ᵢ P :=
 { to_equiv := equiv.vadd_const x,
-  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ _ _, dist_vadd_cancel_right _ _ _ }
+  isometry_to_fun := isometry.of_dist_eq $ λ _ _, dist_vadd_cancel_right _ _ _ }
 
 section
 
@@ -83,7 +83,7 @@ variable (P)
 /-- Self-isometry of a (semi)normed add torsor given by addition of a constant vector `x`. -/
 @[simps] def isometric.const_vadd (x : V) : P ≃ᵢ P :=
 { to_equiv := equiv.const_vadd P x,
-  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ _ _, dist_vadd_cancel_left _ _ _ }
+  isometry_to_fun := isometry.of_dist_eq $ λ _ _, dist_vadd_cancel_left _ _ _ }
 
 end
 
@@ -94,7 +94,7 @@ by rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
 subtraction from `x : P`. -/
 @[simps] def isometric.const_vsub (x : P) : P ≃ᵢ V :=
 { to_equiv := equiv.const_vsub x,
-  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_vsub_cancel_left _ _ _ }
+  isometry_to_fun := isometry.of_dist_eq $ λ y z, dist_vsub_cancel_left _ _ _ }
 
 @[simp] lemma dist_vsub_cancel_right (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y :=
 (isometric.vadd_const z).symm.dist_eq x y

src/analysis/normed/group/basic.lean

@@ -378,7 +378,7 @@ namespace isometric
 
 /-- Addition `y ↦ y + x` as an `isometry`. -/
 protected def add_right (x : E) : E ≃ᵢ E :=
-{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_add_right _ _ _,
+{ isometry_to_fun := isometry.of_dist_eq $ λ y z, dist_add_right _ _ _,
   .. equiv.add_right x }
 
 @[simp] lemma add_right_to_equiv (x : E) :
@@ -394,7 +394,7 @@ ext $ λ y, rfl
 
 /-- Addition `y ↦ x + y` as an `isometry`. -/
 protected def add_left (x : E) : E ≃ᵢ E :=
-{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_add_left _ _ _,
+{ isometry_to_fun := isometry.of_dist_eq $ λ y z, dist_add_left _ _ _,
   to_equiv := equiv.add_left x }
 
 @[simp] lemma add_left_to_equiv (x : E) :
@@ -410,7 +410,7 @@ variable (E)
 
 /-- Negation `x ↦ -x` as an `isometry`. -/
 protected def neg : E ≃ᵢ E :=
-{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ x y, dist_neg_neg _ _,
+{ isometry_to_fun := isometry.of_dist_eq $ λ x y, dist_neg_neg _ _,
   to_equiv := equiv.neg E }
 
 variable {E}
@@ -511,7 +511,7 @@ end
 lemma add_monoid_hom_class.isometry_iff_norm {𝓕 : Type*} [add_monoid_hom_class 𝓕 E F]
   (f : 𝓕) : isometry f ↔ ∀ x, ∥f x∥ = ∥x∥ :=
 begin
-  simp only [isometry_emetric_iff_metric, dist_eq_norm, ←map_sub],
+  simp only [isometry_iff_dist_eq, dist_eq_norm, ←map_sub],
   refine ⟨λ h x, _, λ h x y, h _⟩,
   simpa using h x 0
 end

src/analysis/normed_space/basic.lean

@@ -411,7 +411,7 @@ variables (𝕜 𝕜')
 /-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
 lemma algebra_map_isometry [norm_one_class 𝕜'] : isometry (algebra_map 𝕜 𝕜') :=
 begin
-  refine isometry_emetric_iff_metric.2 (λx y, _),
+  refine isometry.of_dist_eq (λx y, _),
   rw [dist_eq_norm, dist_eq_norm, ← ring_hom.map_sub, norm_algebra_map'],
 end
 

src/measure_theory/function/conditional_expectation.lean

@@ -475,12 +475,8 @@ end
 
 lemma isometry_Lp_meas_subgroup_to_Lp_trim [hp : fact (1 ≤ p)] (hm : m ≤ m0) :
   isometry (Lp_meas_subgroup_to_Lp_trim F p μ hm) :=
-begin
-  rw isometry_emetric_iff_metric,
-  intros f g,
-  rw [dist_eq_norm, ← Lp_meas_subgroup_to_Lp_trim_sub, Lp_meas_subgroup_to_Lp_trim_norm_map,
-    dist_eq_norm],
-end
+isometry.of_dist_eq $ λ f g, by rw [dist_eq_norm, ← Lp_meas_subgroup_to_Lp_trim_sub,
+  Lp_meas_subgroup_to_Lp_trim_norm_map, dist_eq_norm]
 
 variables (F p μ)
 /-- `Lp_meas_subgroup` and `Lp F p (μ.trim hm)` are isometric. -/

src/topology/continuous_function/bounded.lean

@@ -392,7 +392,7 @@ end
 
 lemma isometry_extend (f : α ↪ δ) (h : δ →ᵇ β) :
   isometry (λ g : α →ᵇ β, extend f g h) :=
-isometry_emetric_iff_metric.2 $ λ g₁ g₂, by simp [dist_nonneg]
+isometry.of_dist_eq $ λ g₁ g₂, by simp [dist_nonneg]
 
 end extend
 

src/topology/metric_space/completion.lean

@@ -173,7 +173,7 @@ instance : metric_space (completion α) :=
 
 /-- The embedding of a metric space in its completion is an isometry. -/
 lemma coe_isometry : isometry (coe : α → completion α) :=
-isometry_emetric_iff_metric.2 completion.dist_eq
+isometry.of_dist_eq completion.dist_eq
 
 @[simp] protected lemma edist_eq (x y : α) : edist (x : completion α) y = edist x y :=
 coe_isometry x y

src/topology/metric_space/gluing.lean

@@ -338,11 +338,11 @@ lemma sum.dist_eq {x y : X ⊕ Y} : dist x y = sum.dist x y := rfl
 
 /-- The left injection of a space in a disjoint union is an isometry -/
 lemma isometry_inl : isometry (sum.inl : X → (X ⊕ Y)) :=
-isometry_emetric_iff_metric.2 $ λx y, rfl
+isometry.of_dist_eq $ λ x y, rfl
 
 /-- The right injection of a space in a disjoint union is an isometry -/
 lemma isometry_inr : isometry (sum.inr : Y → (X ⊕ Y)) :=
-isometry_emetric_iff_metric.2 $ λx y, rfl
+isometry.of_dist_eq $ λ x y, rfl
 
 end sum
 
@@ -487,7 +487,7 @@ open filter
 
 /-- The injection of a space in a disjoint union is an isometry -/
 lemma isometry_mk (i : ι) : isometry (sigma.mk i : E i → Σ k, E k) :=
-isometry_emetric_iff_metric.2 (by simp)
+isometry.of_dist_eq (λ x y, by simp)
 
 /-- A disjoint union of complete metric spaces is complete. -/
 protected lemma complete_space [∀ i, complete_space (E i)] : complete_space (Σ i, E i) :=
@@ -559,10 +559,10 @@ begin
 end
 
 lemma to_glue_l_isometry (hΦ : isometry Φ) (hΨ : isometry Ψ) : isometry (to_glue_l hΦ hΨ) :=
-isometry_emetric_iff_metric.2 $ λ_ _, rfl
+isometry.of_dist_eq $ λ_ _, rfl
 
 lemma to_glue_r_isometry (hΦ : isometry Φ) (hΨ : isometry Ψ) : isometry (to_glue_r hΦ hΨ) :=
-isometry_emetric_iff_metric.2 $ λ_ _, rfl
+isometry.of_dist_eq $ λ_ _, rfl
 
 end gluing --section
 
@@ -656,7 +656,7 @@ instance (I : ∀ n, isometry (f n)) [inhabited (X 0)] : inhabited (inductive_li
 
 /-- The map `to_inductive_limit n` mapping `X n` to the inductive limit is an isometry. -/
 lemma to_inductive_limit_isometry (I : ∀ n, isometry (f n)) (n : ℕ) :
-  isometry (to_inductive_limit I n) := isometry_emetric_iff_metric.2 $ λx y,
+  isometry (to_inductive_limit I n) := isometry.of_dist_eq $ λ x y,
 begin
   change inductive_limit_dist f ⟨n, x⟩ ⟨n, y⟩ = dist x y,
   rw [inductive_limit_dist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n),

src/topology/metric_space/gromov_hausdorff.lean

@@ -534,8 +534,8 @@ begin
     glue_metric_approx (λ x:s, (x:X)) (λ x, Φ x) (ε₂/2 + δ) (by linarith) this,
   let Fl := @sum.inl X Y,
   let Fr := @sum.inr X Y,
-  have Il : isometry Fl := isometry_emetric_iff_metric.2 (λ x y, rfl),
-  have Ir : isometry Fr := isometry_emetric_iff_metric.2 (λ x y, rfl),
+  have Il : isometry Fl := isometry.of_dist_eq (λ x y, rfl),
+  have Ir : isometry Fr := isometry.of_dist_eq (λ x y, rfl),
   /- The proof goes as follows : the `GH_dist` is bounded by the Hausdorff distance of the images
   in the coupling, which is bounded (using the triangular inequality) by the sum of the Hausdorff
   distances of `X` and `s` (in the coupling or, equivalently in the original space), of `s` and

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -461,7 +461,7 @@ def optimal_GH_injl (x : X) : optimal_GH_coupling X Y := ⟦inl x⟧
 /-- The injection of `X` in the optimal coupling between `X` and `Y` is an isometry. -/
 lemma isometry_optimal_GH_injl : isometry (optimal_GH_injl X Y) :=
 begin
-  refine isometry_emetric_iff_metric.2 (λx y, _),
+  refine isometry.of_dist_eq (λx y, _),
   change dist ⟦inl x⟧ ⟦inl y⟧ = dist x y,
   exact candidates_dist_inl (optimal_GH_dist_mem_candidates_b X Y) _ _,
 end
@@ -472,7 +472,7 @@ def optimal_GH_injr (y : Y) : optimal_GH_coupling X Y := ⟦inr y⟧
 /-- The injection of `Y` in the optimal coupling between `X` and `Y` is an isometry. -/
 lemma isometry_optimal_GH_injr : isometry (optimal_GH_injr X Y) :=
 begin
-  refine isometry_emetric_iff_metric.2 (λx y, _),
+  refine isometry.of_dist_eq (λx y, _),
   change dist ⟦inr x⟧ ⟦inr y⟧ = dist x y,
   exact candidates_dist_inr (optimal_GH_dist_mem_candidates_b X Y) _ _,
 end