chore(topology/metric_space/isometry): rename isometric to isometry_e…

…quiv (#18191)

The name for isometric bijections is changed to `isometry_equiv`, to be consistent with `linear_isometry_equiv` and `affine_isometry_equiv`.

src/analysis/normed/group/add_torsor.lean

@@ -85,7 +85,7 @@ by rw [dist_comm, dist_vadd_left]
 
 /-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
 addition/subtraction of `x : P`. -/
-@[simps] def isometric.vadd_const (x : P) : V ≃ᵢ P :=
+@[simps] def isometry_equiv.vadd_const (x : P) : V ≃ᵢ P :=
 { to_equiv := equiv.vadd_const x,
   isometry_to_fun := isometry.of_dist_eq $ λ _ _, dist_vadd_cancel_right _ _ _ }
 
@@ -94,7 +94,7 @@ section
 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 :=
+@[simps] def isometry_equiv.const_vadd (x : V) : P ≃ᵢ P :=
 { to_equiv := equiv.const_vadd P x,
   isometry_to_fun := isometry.of_dist_eq $ λ _ _, dist_vadd_cancel_left _ _ _ }
 
@@ -105,28 +105,28 @@ by rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
 
 /-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
 subtraction from `x : P`. -/
-@[simps] def isometric.const_vsub (x : P) : P ≃ᵢ V :=
+@[simps] def isometry_equiv.const_vsub (x : P) : P ≃ᵢ V :=
 { to_equiv := equiv.const_vsub x,
   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
+(isometry_equiv.vadd_const z).symm.dist_eq x y
 
 section pointwise
 
 open_locale pointwise
 
 @[simp] lemma vadd_ball (x : V) (y : P) (r : ℝ) :
   x +ᵥ metric.ball y r = metric.ball (x +ᵥ y) r :=
-(isometric.const_vadd P x).image_ball y r
+(isometry_equiv.const_vadd P x).image_ball y r
 
 @[simp] lemma vadd_closed_ball (x : V) (y : P) (r : ℝ) :
   x +ᵥ metric.closed_ball y r = metric.closed_ball (x +ᵥ y) r :=
-(isometric.const_vadd P x).image_closed_ball y r
+(isometry_equiv.const_vadd P x).image_closed_ball y r
 
 @[simp] lemma vadd_sphere (x : V) (y : P) (r : ℝ) :
   x +ᵥ metric.sphere y r = metric.sphere (x +ᵥ y) r :=
-(isometric.const_vadd P x).image_sphere y r
+(isometry_equiv.const_vadd P x).image_sphere y r
 
 end pointwise
 

src/analysis/normed/group/basic.lean

@@ -493,7 +493,7 @@ def norm_group_seminorm : group_seminorm E := ⟨norm, norm_one', norm_mul_le',
 
 variables {E}
 
-namespace isometric
+namespace isometry_equiv
 -- TODO This material is superseded by similar constructions such as
 -- `affine_isometry_equiv.const_vadd`; deduplicate
 
@@ -504,18 +504,19 @@ protected def mul_right (x : E) : E ≃ᵢ E :=
   .. equiv.mul_right x }
 
 @[simp, to_additive]
-lemma mul_right_to_equiv (x : E) : (isometric.mul_right x).to_equiv = equiv.mul_right x := rfl
+lemma mul_right_to_equiv (x : E) : (isometry_equiv.mul_right x).to_equiv = equiv.mul_right x := rfl
 
 @[simp, to_additive]
-lemma coe_mul_right (x : E) : (isometric.mul_right x : E → E) = λ y, y * x := rfl
+lemma coe_mul_right (x : E) : (isometry_equiv.mul_right x : E → E) = λ y, y * x := rfl
 
-@[to_additive] lemma mul_right_apply (x y : E) : (isometric.mul_right x : E → E) y = y * x := rfl
+@[to_additive] lemma mul_right_apply (x y : E) : (isometry_equiv.mul_right x : E → E) y = y * x :=
+rfl
 
 @[simp, to_additive]
-lemma mul_right_symm (x : E) : (isometric.mul_right x).symm = isometric.mul_right x⁻¹ :=
+lemma mul_right_symm (x : E) : (isometry_equiv.mul_right x).symm = isometry_equiv.mul_right x⁻¹ :=
 ext $ λ y, rfl
 
-end isometric
+end isometry_equiv
 
 @[to_additive] lemma normed_comm_group.tendsto_nhds_one {f : α → E} {l : filter α} :
   tendsto f l (𝓝 1) ↔ ∀ ε > 0, ∀ᶠ x in l, ‖ f x ‖ < ε :=
@@ -1107,7 +1108,7 @@ by { ext, simp [mem_closed_ball, set.mem_smul_set, dist_eq_norm_div, div_eq_inv_
 by { ext, simp [mem_ball, set.mem_smul_set, dist_eq_norm_div, div_eq_inv_mul,
   ← eq_inv_mul_iff_mul_eq, mul_assoc], }
 
-namespace isometric
+namespace isometry_equiv
 
 /-- Multiplication `y ↦ x * y` as an `isometry`. -/
 @[to_additive "Addition `y ↦ x + y` as an `isometry`"]
@@ -1116,12 +1117,12 @@ protected def mul_left (x : E) : E ≃ᵢ E :=
   to_equiv := equiv.mul_left x }
 
 @[simp, to_additive] lemma mul_left_to_equiv (x : E) :
-  (isometric.mul_left x).to_equiv = equiv.mul_left x := rfl
+  (isometry_equiv.mul_left x).to_equiv = equiv.mul_left x := rfl
 
-@[simp, to_additive] lemma coe_mul_left (x : E) : ⇑(isometric.mul_left x) = (*) x := rfl
+@[simp, to_additive] lemma coe_mul_left (x : E) : ⇑(isometry_equiv.mul_left x) = (*) x := rfl
 
 @[simp, to_additive] lemma mul_left_symm (x : E) :
-  (isometric.mul_left x).symm = isometric.mul_left x⁻¹ :=
+  (isometry_equiv.mul_left x).symm = isometry_equiv.mul_left x⁻¹ :=
 ext $ λ y, rfl
 
 variables (E)
@@ -1133,11 +1134,11 @@ variables (E)
 
 variables {E}
 
-@[simp, to_additive] lemma inv_symm : (isometric.inv E).symm = isometric.inv E := rfl
-@[simp, to_additive] lemma inv_to_equiv : (isometric.inv E).to_equiv = equiv.inv E := rfl
-@[simp, to_additive] lemma coe_inv : ⇑(isometric.inv E) = has_inv.inv := rfl
+@[simp, to_additive] lemma inv_symm : (isometry_equiv.inv E).symm = isometry_equiv.inv E := rfl
+@[simp, to_additive] lemma inv_to_equiv : (isometry_equiv.inv E).to_equiv = equiv.inv E := rfl
+@[simp, to_additive] lemma coe_inv : ⇑(isometry_equiv.inv E) = has_inv.inv := rfl
 
-end isometric
+end isometry_equiv
 
 open finset
 

src/analysis/normed_space/add_torsor.lean

@@ -32,7 +32,7 @@ lemma affine_subspace.is_closed_direction_iff (s : affine_subspace 𝕜 Q) :
   is_closed (s.direction : set W) ↔ is_closed (s : set Q) :=
 begin
   rcases s.eq_bot_or_nonempty with rfl|⟨x, hx⟩, { simp [is_closed_singleton] },
-  rw [← (isometric.vadd_const x).to_homeomorph.symm.is_closed_image,
+  rw [← (isometry_equiv.vadd_const x).to_homeomorph.symm.is_closed_image,
     affine_subspace.coe_direction_eq_vsub_set_right hx],
   refl
 end

src/analysis/normed_space/affine_isometry.lean

@@ -317,18 +317,18 @@ variables (e : P ≃ᵃⁱ[𝕜] P₂)
 
 protected lemma isometry : isometry e := e.to_affine_isometry.isometry
 
-/-- Reinterpret a `affine_isometry_equiv` as an `isometric`. -/
-def to_isometric : P ≃ᵢ P₂ := ⟨e.to_affine_equiv.to_equiv, e.isometry⟩
+/-- Reinterpret a `affine_isometry_equiv` as an `isometry_equiv`. -/
+def to_isometry_equiv : P ≃ᵢ P₂ := ⟨e.to_affine_equiv.to_equiv, e.isometry⟩
 
-@[simp] lemma coe_to_isometric : ⇑e.to_isometric = e := rfl
+@[simp] lemma coe_to_isometry_equiv : ⇑e.to_isometry_equiv = e := rfl
 
 include V V₂
 lemma range_eq_univ (e : P ≃ᵃⁱ[𝕜] P₂) : set.range e = set.univ :=
-by { rw ← coe_to_isometric, exact isometric.range_eq_univ _, }
+by { rw ← coe_to_isometry_equiv, exact isometry_equiv.range_eq_univ _, }
 omit V V₂
 
 /-- Reinterpret a `affine_isometry_equiv` as an `homeomorph`. -/
-def to_homeomorph : P ≃ₜ P₂ := e.to_isometric.to_homeomorph
+def to_homeomorph : P ≃ₜ P₂ := e.to_isometry_equiv.to_homeomorph
 
 @[simp] lemma coe_to_homeomorph : ⇑e.to_homeomorph = e := rfl
 
@@ -351,7 +351,7 @@ instance : inhabited (P ≃ᵃⁱ[𝕜] P) := ⟨refl 𝕜 P⟩
 
 @[simp] lemma coe_refl : ⇑(refl 𝕜 P) = id := rfl
 @[simp] lemma to_affine_equiv_refl : (refl 𝕜 P).to_affine_equiv = affine_equiv.refl 𝕜 P := rfl
-@[simp] lemma to_isometric_refl : (refl 𝕜 P).to_isometric = isometric.refl P := rfl
+@[simp] lemma to_isometry_equiv_refl : (refl 𝕜 P).to_isometry_equiv = isometry_equiv.refl P := rfl
 @[simp] lemma to_homeomorph_refl : (refl 𝕜 P).to_homeomorph = homeomorph.refl P := rfl
 omit V
 
@@ -365,7 +365,7 @@ def symm : P₂ ≃ᵃⁱ[𝕜] P :=
 @[simp] lemma symm_symm : e.symm.symm = e := ext $ λ x, rfl
 
 @[simp] lemma to_affine_equiv_symm : e.to_affine_equiv.symm = e.symm.to_affine_equiv := rfl
-@[simp] lemma to_isometric_symm : e.to_isometric.symm = e.symm.to_isometric := rfl
+@[simp] lemma to_isometry_equiv_symm : e.to_isometry_equiv.symm = e.symm.to_isometry_equiv := rfl
 @[simp] lemma to_homeomorph_symm : e.to_homeomorph.symm = e.symm.to_homeomorph := rfl
 
 include V₃

src/analysis/normed_space/linear_isometry.lean

@@ -456,24 +456,24 @@ to_linear_isometry_injective.eq_iff
 
 protected lemma isometry : isometry e := e.to_linear_isometry.isometry
 
-/-- Reinterpret a `linear_isometry_equiv` as an `isometric`. -/
-def to_isometric : E ≃ᵢ E₂ := ⟨e.to_linear_equiv.to_equiv, e.isometry⟩
+/-- Reinterpret a `linear_isometry_equiv` as an `isometry_equiv`. -/
+def to_isometry_equiv : E ≃ᵢ E₂ := ⟨e.to_linear_equiv.to_equiv, e.isometry⟩
 
-lemma to_isometric_injective :
-  function.injective (to_isometric : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ᵢ E₂) :=
-λ x y h, coe_injective (congr_arg _ h : ⇑x.to_isometric = _)
+lemma to_isometry_equiv_injective :
+  function.injective (to_isometry_equiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ᵢ E₂) :=
+λ x y h, coe_injective (congr_arg _ h : ⇑x.to_isometry_equiv = _)
 
-@[simp] lemma to_isometric_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
-  f.to_isometric = g.to_isometric ↔ f = g :=
-to_isometric_injective.eq_iff
+@[simp] lemma to_isometry_equiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
+  f.to_isometry_equiv = g.to_isometry_equiv ↔ f = g :=
+to_isometry_equiv_injective.eq_iff
 
-@[simp] lemma coe_to_isometric : ⇑e.to_isometric = e := rfl
+@[simp] lemma coe_to_isometry_equiv : ⇑e.to_isometry_equiv = e := rfl
 
 lemma range_eq_univ (e : E ≃ₛₗᵢ[σ₁₂] E₂) : set.range e = set.univ :=
-by { rw ← coe_to_isometric, exact isometric.range_eq_univ _, }
+by { rw ← coe_to_isometry_equiv, exact isometry_equiv.range_eq_univ _, }
 
 /-- Reinterpret a `linear_isometry_equiv` as an `homeomorph`. -/
-def to_homeomorph : E ≃ₜ E₂ := e.to_isometric.to_homeomorph
+def to_homeomorph : E ≃ₜ E₂ := e.to_isometry_equiv.to_homeomorph
 
 lemma to_homeomorph_injective :
   function.injective (to_homeomorph : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₜ E₂) :=
@@ -531,7 +531,7 @@ def symm : E₂ ≃ₛₗᵢ[σ₂₁] E :=
 @[simp] lemma symm_symm : e.symm.symm = e := ext $ λ x, rfl
 
 @[simp] lemma to_linear_equiv_symm : e.to_linear_equiv.symm = e.symm.to_linear_equiv := rfl
-@[simp] lemma to_isometric_symm : e.to_isometric.symm = e.symm.to_isometric := rfl
+@[simp] lemma to_isometry_equiv_symm : e.to_isometry_equiv.symm = e.symm.to_isometry_equiv := rfl
 @[simp] lemma to_homeomorph_symm : e.to_homeomorph.symm = e.symm.to_homeomorph := rfl
 
 /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
@@ -624,7 +624,7 @@ include σ₂₁
 
 /-- Reinterpret a `linear_isometry_equiv` as a `continuous_linear_equiv`. -/
 instance : has_coe_t (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂) :=
-⟨λ e, ⟨e.to_linear_equiv, e.continuous, e.to_isometric.symm.continuous⟩⟩
+⟨λ e, ⟨e.to_linear_equiv, e.continuous, e.to_isometry_equiv.symm.continuous⟩⟩
 
 instance : has_coe_t (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂) := ⟨λ e, ↑(e : E ≃SL[σ₁₂] E₂)⟩
 
@@ -678,27 +678,27 @@ e.isometry.diam_image s
 
 @[simp] lemma preimage_ball (x : E₂) (r : ℝ) :
   e ⁻¹' (metric.ball x r) = metric.ball (e.symm x) r :=
-e.to_isometric.preimage_ball x r
+e.to_isometry_equiv.preimage_ball x r
 
 @[simp] lemma preimage_sphere (x : E₂) (r : ℝ) :
   e ⁻¹' (metric.sphere x r) = metric.sphere (e.symm x) r :=
-e.to_isometric.preimage_sphere x r
+e.to_isometry_equiv.preimage_sphere x r
 
 @[simp] lemma preimage_closed_ball (x : E₂) (r : ℝ) :
   e ⁻¹' (metric.closed_ball x r) = metric.closed_ball (e.symm x) r :=
-e.to_isometric.preimage_closed_ball x r
+e.to_isometry_equiv.preimage_closed_ball x r
 
 @[simp] lemma image_ball (x : E) (r : ℝ) :
   e '' (metric.ball x r) = metric.ball (e x) r :=
-e.to_isometric.image_ball x r
+e.to_isometry_equiv.image_ball x r
 
 @[simp] lemma image_sphere (x : E) (r : ℝ) :
   e '' (metric.sphere x r) = metric.sphere (e x) r :=
-e.to_isometric.image_sphere x r
+e.to_isometry_equiv.image_sphere x r
 
 @[simp] lemma image_closed_ball (x : E) (r : ℝ) :
   e '' (metric.closed_ball x r) = metric.closed_ball (e x) r :=
-e.to_isometric.image_closed_ball x r
+e.to_isometry_equiv.image_closed_ball x r
 
 variables {α : Type*} [topological_space α]
 

src/analysis/normed_space/mazur_ulam.lean

@@ -13,12 +13,12 @@ import linear_algebra.affine_space.midpoint
 Mazur-Ulam theorem states that an isometric bijection between two normed affine spaces over `ℝ` is
 affine. We formalize it in three definitions:
 
-* `isometric.to_real_linear_isometry_equiv_of_map_zero` : given `E ≃ᵢ F` sending `0` to `0`,
+* `isometry_equiv.to_real_linear_isometry_equiv_of_map_zero` : given `E ≃ᵢ F` sending `0` to `0`,
   returns `E ≃ₗᵢ[ℝ] F` with the same `to_fun` and `inv_fun`;
-* `isometric.to_real_linear_isometry_equiv` : given `f : E ≃ᵢ F`, returns a linear isometry
+* `isometry_equiv.to_real_linear_isometry_equiv` : given `f : E ≃ᵢ F`, returns a linear isometry
   equivalence `g : E ≃ₗᵢ[ℝ] F` with `g x = f x - f 0`.
-* `isometric.to_real_affine_isometry_equiv` : given `f : PE ≃ᵢ PF`, returns an affine isometry
-  equivalence `g : PE ≃ᵃⁱ[ℝ] PF` whose underlying `isometric` is `f`
+* `isometry_equiv.to_real_affine_isometry_equiv` : given `f : PE ≃ᵢ PF`, returns an affine isometry
+  equivalence `g : PE ≃ᵃⁱ[ℝ] PF` whose underlying `isometry_equiv` is `f`
 
 The formalization is based on [Jussi Väisälä, *A Proof of the Mazur-Ulam Theorem*][Vaisala_2003].
 
@@ -35,7 +35,7 @@ open set affine_map affine_isometry_equiv
 
 noncomputable theory
 
-namespace isometric
+namespace isometry_equiv
 
 include E
 
@@ -48,7 +48,7 @@ begin
   set z := midpoint ℝ x y,
   -- Consider the set of `e : E ≃ᵢ E` such that `e x = x` and `e y = y`
   set s := { e : PE ≃ᵢ PE | e x = x ∧ e y = y },
-  haveI : nonempty s := ⟨⟨isometric.refl PE, rfl, rfl⟩⟩,
+  haveI : nonempty s := ⟨⟨isometry_equiv.refl PE, rfl, rfl⟩⟩,
   -- On the one hand, `e` cannot send the midpoint `z` of `[x, y]` too far
   have h_bdd : bdd_above (range $ λ e : s, dist (e z) z),
   { refine ⟨dist x z + dist x z, forall_range_iff.2 $ subtype.forall.2 _⟩,
@@ -59,7 +59,7 @@ begin
   -- On the other hand, consider the map `f : (E ≃ᵢ E) → (E ≃ᵢ E)`
   -- sending each `e` to `R ∘ e⁻¹ ∘ R ∘ e`, where `R` is the point reflection in the
   -- midpoint `z` of `[x, y]`.
-  set R : PE ≃ᵢ PE := (point_reflection ℝ z).to_isometric,
+  set R : PE ≃ᵢ PE := (point_reflection ℝ z).to_isometry_equiv,
   set f : (PE ≃ᵢ PE) → (PE ≃ᵢ PE) := λ e, ((e.trans R).trans e.symm).trans R,
   -- Note that `f` doubles the value of ``dist (e z) z`
   have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z,
@@ -89,14 +89,14 @@ include F
 lemma map_midpoint (f : PE ≃ᵢ PF) (x y : PE) : f (midpoint ℝ x y) = midpoint ℝ (f x) (f y) :=
 begin
   set e : PE ≃ᵢ PE :=
-    ((f.trans $ (point_reflection ℝ $ midpoint ℝ (f x) (f y)).to_isometric).trans f.symm).trans
-    (point_reflection ℝ $ midpoint ℝ x y).to_isometric,
+    ((f.trans $ (point_reflection ℝ $ midpoint ℝ (f x) (f y)).to_isometry_equiv).trans f.symm).trans
+    (point_reflection ℝ $ midpoint ℝ x y).to_isometry_equiv,
   have hx : e x = x, by simp,
   have hy : e y = y, by simp,
   have hm := e.midpoint_fixed hx hy,
   simp only [e, trans_apply] at hm,
-  rwa [← eq_symm_apply, to_isometric_symm, point_reflection_symm, coe_to_isometric,
-    coe_to_isometric, point_reflection_self, symm_apply_eq, point_reflection_fixed_iff] at hm
+  rwa [← eq_symm_apply, to_isometry_equiv_symm, point_reflection_symm, coe_to_isometry_equiv,
+    coe_to_isometry_equiv, point_reflection_self, symm_apply_eq, point_reflection_fixed_iff] at hm
 end
 
 /-!
@@ -121,7 +121,7 @@ def to_real_linear_isometry_equiv_of_map_zero (f : E ≃ᵢ F) (h0 : f 0 = 0) :
 /-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
 over `ℝ`, then `x ↦ f x - f 0` is a linear isometry equivalence. -/
 def to_real_linear_isometry_equiv (f : E ≃ᵢ F) : E ≃ₗᵢ[ℝ] F :=
-(f.trans (isometric.add_right (f 0)).symm).to_real_linear_isometry_equiv_of_map_zero
+(f.trans (isometry_equiv.add_right (f 0)).symm).to_real_linear_isometry_equiv_of_map_zero
   (by simpa only [sub_eq_add_neg] using sub_self (f 0))
 
 @[simp] lemma to_real_linear_equiv_apply (f : E ≃ᵢ F) (x : E) :
@@ -144,7 +144,7 @@ affine_isometry_equiv.mk' f
 rfl
 
 @[simp] lemma coe_to_real_affine_isometry_equiv (f : PE ≃ᵢ PF) :
-  f.to_real_affine_isometry_equiv.to_isometric = f :=
+  f.to_real_affine_isometry_equiv.to_isometry_equiv = f :=
 by { ext, refl }
 
-end isometric
+end isometry_equiv

src/measure_theory/function/conditional_expectation/basic.lean

@@ -303,7 +303,7 @@ section complete_subspace
 
 /-! ## The subspace `Lp_meas` is complete.
 
-We define an `isometric` between `Lp_meas_subgroup` and the `Lp` space corresponding to the
+We define an `isometry_equiv` between `Lp_meas_subgroup` and the `Lp` space corresponding to the
 measure `μ.trim hm`. As a consequence, the completeness of `Lp` implies completeness of
 `Lp_meas_subgroup` (and `Lp_meas`). -/
 
@@ -488,7 +488,7 @@ variables (𝕜)
 /-- `Lp_meas_subgroup` and `Lp_meas` are isometric. -/
 def Lp_meas_subgroup_to_Lp_meas_iso [hp : fact (1 ≤ p)] :
   Lp_meas_subgroup F m p μ ≃ᵢ Lp_meas F 𝕜 m p μ :=
-isometric.refl (Lp_meas_subgroup F m p μ)
+isometry_equiv.refl (Lp_meas_subgroup F m p μ)
 
 /-- `Lp_meas` and `Lp F p (μ.trim hm)` are isometric, with a linear equivalence. -/
 def Lp_meas_to_Lp_trim_lie [hp : fact (1 ≤ p)] (hm : m ≤ m0) :

src/measure_theory/measure/hausdorff.lean

@@ -387,13 +387,13 @@ lemma isometry_map_mk_metric (m : ℝ≥0∞ → ℝ≥0∞) {f : X → Y} (hf :
   map f (mk_metric m) = restrict (range f) (mk_metric m) :=
 by rw [← isometry_comap_mk_metric _ hf H, map_comap]
 
-lemma isometric_comap_mk_metric (m : ℝ≥0∞ → ℝ≥0∞) (f : X ≃ᵢ Y) :
+lemma isometry_equiv_comap_mk_metric (m : ℝ≥0∞ → ℝ≥0∞) (f : X ≃ᵢ Y) :
   comap f (mk_metric m) = mk_metric m :=
 isometry_comap_mk_metric _ f.isometry (or.inr f.surjective)
 
-lemma isometric_map_mk_metric (m : ℝ≥0∞ → ℝ≥0∞) (f : X ≃ᵢ Y) :
+lemma isometry_equiv_map_mk_metric (m : ℝ≥0∞ → ℝ≥0∞) (f : X ≃ᵢ Y) :
   map f (mk_metric m) = mk_metric m :=
-by rw [← isometric_comap_mk_metric _ f, map_comap_of_surjective f.surjective]
+by rw [← isometry_equiv_comap_mk_metric _ f, map_comap_of_surjective f.surjective]
 
 lemma trim_mk_metric [measurable_space X] [borel_space X] (m : ℝ≥0∞ → ℝ≥0∞) :
   (mk_metric m : outer_measure X).trim = mk_metric m :=
@@ -942,7 +942,7 @@ end
 
 end isometry
 
-namespace isometric
+namespace isometry_equiv
 
 @[simp] lemma hausdorff_measure_image (e : X ≃ᵢ Y) (d : ℝ) (s : set X) :
   μH[d] (e '' s) = μH[d] s :=
@@ -952,4 +952,4 @@ e.isometry.hausdorff_measure_image (or.inr e.surjective) s
   μH[d] (e ⁻¹' s) = μH[d] s :=
 by rw [← e.image_symm, e.symm.hausdorff_measure_image]
 
-end isometric
+end isometry_equiv