chore: Rename UniformEmbedding to IsUniformEmbedding (#17295)

`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighborhing declarations (which `DenseEmbedding` is)
2. namespacing it inside `Topology`

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

@@ -218,7 +218,7 @@ lemma QuasispectrumRestricts.isSelfAdjoint (a : A) (ha : QuasispectrumRestricts
 instance IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus :
     NonUnitalContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop) :=
   QuasispectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
-    Complex.isometry_ofReal.uniformEmbedding (.zero _)
+    Complex.isometry_ofReal.isUniformEmbedding (.zero _)
     (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts)
 
 end SelfAdjointNonUnital
@@ -264,7 +264,7 @@ lemma SpectrumRestricts.isSelfAdjoint (a : A) (ha : SpectrumRestricts a Complex.
 instance IsSelfAdjoint.instContinuousFunctionalCalculus :
     ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop) :=
   SpectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
-    Complex.isometry_ofReal.uniformEmbedding (.zero _)
+    Complex.isometry_ofReal.isUniformEmbedding (.zero _)
     (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts)
 
 lemma IsSelfAdjoint.spectrum_nonempty {A : Type*} [Ring A] [StarRing A]
@@ -313,7 +313,7 @@ open NNReal in
 instance Nonneg.instNonUnitalContinuousFunctionalCalculus :
     NonUnitalContinuousFunctionalCalculus ℝ≥0 (fun x : A ↦ 0 ≤ x) :=
   QuasispectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal
-    uniformEmbedding_subtype_val le_rfl
+    isUniformEmbedding_subtype_val le_rfl
     (fun _ ↦ nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts)
 
 open NNReal in
@@ -359,7 +359,7 @@ open NNReal in
 instance Nonneg.instContinuousFunctionalCalculus :
     ContinuousFunctionalCalculus ℝ≥0 (fun x : A ↦ 0 ≤ x) :=
   SpectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal
-    uniformEmbedding_subtype_val le_rfl (fun _ ↦ nonneg_iff_isSelfAdjoint_and_spectrumRestricts)
+    isUniformEmbedding_subtype_val le_rfl (fun _ ↦ nonneg_iff_isSelfAdjoint_and_spectrumRestricts)
 
 end Nonneg
 
@@ -605,14 +605,14 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A]
 
 lemma cfcHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) :
     cfcHom ha = ha.spectrumRestricts.starAlgHom (cfcHom ha.isStarNormal) (f := Complex.reCLM) :=
-  ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding
+  ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal.isUniformEmbedding
     ha ha.isStarNormal
 
 lemma cfc_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac)  :
     cfc f a = cfc (fun x ↦ f x.re : ℂ → ℂ) a := by
   replace ha : IsSelfAdjoint a := ha -- hack to avoid issues caused by autoParam
   exact ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM)
-    Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal f
+    Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal f
 
 end RealEqComplex
 
@@ -626,14 +626,14 @@ variable {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module
 lemma cfcₙHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) :
     cfcₙHom ha = (ha.quasispectrumRestricts.2).nonUnitalStarAlgHom (cfcₙHom ha.isStarNormal)
       (f := Complex.reCLM) :=
-  ha.quasispectrumRestricts.2.cfcₙHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding
+  ha.quasispectrumRestricts.2.cfcₙHom_eq_restrict Complex.isometry_ofReal.isUniformEmbedding
     ha ha.isStarNormal
 
 lemma cfcₙ_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac)  :
     cfcₙ f a = cfcₙ (fun x ↦ f x.re : ℂ → ℂ) a := by
   replace ha : IsSelfAdjoint a := ha -- hack to avoid issues caused by autoParam
   exact ha.quasispectrumRestricts.2.cfcₙ_eq_restrict (f := Complex.reCLM)
-    Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal f
+    Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal f
 
 end RealEqComplexNonUnital
 
@@ -650,13 +650,13 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A]
 lemma cfcHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) :
     cfcHom ha = (SpectrumRestricts.nnreal_of_nonneg ha).starAlgHom
       (cfcHom (IsSelfAdjoint.of_nonneg ha)) := by
-  apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict uniformEmbedding_subtype_val
+  apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict isUniformEmbedding_subtype_val
 
 lemma cfc_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac)  :
     cfc f a = cfc (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by
   replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam
   apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict
-    uniformEmbedding_subtype_val ha (.of_nonneg ha)
+    isUniformEmbedding_subtype_val ha (.of_nonneg ha)
 
 end NNRealEqReal
 
@@ -675,13 +675,13 @@ lemma cfcₙHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) :
     cfcₙHom ha = (QuasispectrumRestricts.nnreal_of_nonneg ha).nonUnitalStarAlgHom
       (cfcₙHom (IsSelfAdjoint.of_nonneg ha)) := by
   apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict
-    uniformEmbedding_subtype_val
+    isUniformEmbedding_subtype_val
 
 lemma cfcₙ_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac)  :
     cfcₙ f a = cfcₙ (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by
   replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam
   apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙ_eq_restrict
-    uniformEmbedding_subtype_val ha (.of_nonneg ha)
+    isUniformEmbedding_subtype_val ha (.of_nonneg ha)
 
 end NNRealEqRealNonUnital
 

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -692,7 +692,7 @@ lemma closedEmbedding_cfcₙHom_of_cfcHom {a : A} (ha : p a) :
   let f : C(spectrum R a, σₙ R a) :=
     ⟨_, continuous_inclusion <| spectrum_subset_quasispectrum R a⟩
   refine (cfcHom_closedEmbedding ha).comp <|
-    (UniformInducing.uniformEmbedding ⟨?_⟩).toClosedEmbedding
+    (UniformInducing.isUniformEmbedding ⟨?_⟩).toClosedEmbedding
   have := uniformSpace_eq_inf_precomp_of_cover (β := R) f (0 : C(Unit, σₙ R a))
     (map_continuous f).isProperMap (map_continuous 0).isProperMap <| by
       simp only [← Subtype.val_injective.image_injective.eq_iff, f, ContinuousMap.coe_mk,

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

@@ -84,17 +84,17 @@ variable [CompleteSpace R]
 
 lemma closedEmbedding_starAlgHom {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A}
     (hφ : ClosedEmbedding φ) {f : C(S, R)} (h : SpectrumRestricts a f)
-    (halg : UniformEmbedding (algebraMap R S)) :
+    (halg : IsUniformEmbedding (algebraMap R S)) :
     ClosedEmbedding (h.starAlgHom φ) :=
-  hφ.comp <| UniformEmbedding.toClosedEmbedding <| .comp
-    (ContinuousMap.uniformEmbedding_comp _ halg)
-    (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.uniformEmbedding)
+  hφ.comp <| IsUniformEmbedding.toClosedEmbedding <| .comp
+    (ContinuousMap.isUniformEmbedding_comp _ halg)
+    (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.isUniformEmbedding)
 
 /-- Given a `ContinuousFunctionalCalculus S q`. If we form the predicate `p` for `a : A`
 characterized by: `q a` and the spectrum of `a` restricts to the scalar subring `R` via
 `f : C(S, R)`, then we can get a restricted functional calculus
 `ContinuousFunctionalCalculus R p`. -/
-protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) (h0 : p 0)
+protected theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0)
     (h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) :
     ContinuousFunctionalCalculus R p where
   predicate_zero := h0
@@ -133,14 +133,14 @@ protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) (
 
 variable [ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A]
 
-lemma cfcHom_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S))
+lemma cfcHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S))
     {a : A} (hpa : p a) (hqa : q a) (h : SpectrumRestricts a f) :
     cfcHom hpa = h.starAlgHom (cfcHom hqa) := by
   apply cfcHom_eq_of_continuous_of_map_id
   · exact h.closedEmbedding_starAlgHom (cfcHom_closedEmbedding hqa) halg |>.continuous
   · exact h.starAlgHom_id (cfcHom_id hqa)
 
-lemma cfc_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A} (hpa : p a)
+lemma cfc_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a)
     (hqa : q a) (h : SpectrumRestricts a f) (g : R → R) :
     cfc g a = cfc (fun x ↦ algebraMap R S (g (f x))) a := by
   by_cases hg : ContinuousOn g (spectrum R a)
@@ -218,20 +218,20 @@ variable [CompleteSpace R]
 
 lemma closedEmbedding_nonUnitalStarAlgHom {a : A} {φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A}
     (hφ : ClosedEmbedding φ) {f : C(S, R)} (h : QuasispectrumRestricts a f)
-    (halg : UniformEmbedding (algebraMap R S)) :
+    (halg : IsUniformEmbedding (algebraMap R S)) :
     ClosedEmbedding (h.nonUnitalStarAlgHom φ) := by
   have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)
-  refine hφ.comp <| UniformEmbedding.toClosedEmbedding <| .comp
-    (ContinuousMapZero.uniformEmbedding_comp _ halg)
-    (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.uniformEmbedding)
+  refine hφ.comp <| IsUniformEmbedding.toClosedEmbedding <| .comp
+    (ContinuousMapZero.isUniformEmbedding_comp _ halg)
+    (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding)
 
 variable [IsScalarTower R A A] [SMulCommClass R A A]
 
 /-- Given a `NonUnitalContinuousFunctionalCalculus S q`. If we form the predicate `p` for `a : A`
 characterized by: `q a` and the quasispectrum of `a` restricts to the scalar subring `R` via
 `f : C(S, R)`, then we can get a restricted functional calculus
 `NonUnitalContinuousFunctionalCalculus R p`. -/
-protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) (h0 : p 0)
+protected theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0)
     (h : ∀ a, p a ↔ q a ∧ QuasispectrumRestricts a f) :
     NonUnitalContinuousFunctionalCalculus R p where
   predicate_zero := h0
@@ -275,15 +275,15 @@ protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) (
 variable [NonUnitalContinuousFunctionalCalculus R p]
 variable [UniqueNonUnitalContinuousFunctionalCalculus R A]
 
-lemma cfcₙHom_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A}
+lemma cfcₙHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A}
     (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a f) :
     cfcₙHom hpa = h.nonUnitalStarAlgHom (cfcₙHom hqa) := by
   apply cfcₙHom_eq_of_continuous_of_map_id
   · exact h.closedEmbedding_nonUnitalStarAlgHom (cfcₙHom_closedEmbedding hqa) halg |>.continuous
   · exact h.nonUnitalStarAlgHom_id (cfcₙHom_id hqa)
 
-lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A} (hpa : p a)
-    (hqa : q a) (h : QuasispectrumRestricts a f) (g : R → R) :
+lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A}
+    (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a f) (g : R → R) :
     cfcₙ g a = cfcₙ (fun x ↦ algebraMap R S (g (f x))) a := by
   by_cases hg : ContinuousOn g (σₙ R a) ∧ g 0 = 0
   · obtain ⟨hg, hg0⟩ := hg

Mathlib/Analysis/CStarAlgebra/Multiplier.lean

@@ -534,11 +534,15 @@ instance instNormedSpace : NormedSpace 𝕜 𝓜(𝕜, A) :=
 instance instNormedAlgebra : NormedAlgebra 𝕜 𝓜(𝕜, A) :=
   { DoubleCentralizer.instAlgebra, DoubleCentralizer.instNormedSpace with }
 
-theorem uniformEmbedding_toProdMulOpposite : UniformEmbedding (@toProdMulOpposite 𝕜 A _ _ _ _ _) :=
-  uniformEmbedding_comap toProdMulOpposite_injective
+theorem isUniformEmbedding_toProdMulOpposite :
+    IsUniformEmbedding (toProdMulOpposite (𝕜 := 𝕜) (A := A)) :=
+  isUniformEmbedding_comap toProdMulOpposite_injective
+
+@[deprecated (since := "2024-10-01")]
+alias uniformEmbedding_toProdMulOpposite := isUniformEmbedding_toProdMulOpposite
 
 instance [CompleteSpace A] : CompleteSpace 𝓜(𝕜, A) := by
-  rw [completeSpace_iff_isComplete_range uniformEmbedding_toProdMulOpposite.toUniformInducing]
+  rw [completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.toUniformInducing]
   apply IsClosed.isComplete
   simp only [range_toProdMulOpposite, Set.setOf_forall]
   refine isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq ?_ ?_

Mathlib/Analysis/Complex/Basic.lean

@@ -208,11 +208,14 @@ theorem antilipschitz_equivRealProd : AntilipschitzWith (NNReal.sqrt 2) equivRea
   AddMonoidHomClass.antilipschitz_of_bound equivRealProdLm fun z ↦ by
     simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using abs_le_sqrt_two_mul_max z
 
-theorem uniformEmbedding_equivRealProd : UniformEmbedding equivRealProd :=
-  antilipschitz_equivRealProd.uniformEmbedding lipschitz_equivRealProd.uniformContinuous
+theorem isUniformEmbedding_equivRealProd : IsUniformEmbedding equivRealProd :=
+  antilipschitz_equivRealProd.isUniformEmbedding lipschitz_equivRealProd.uniformContinuous
+
+@[deprecated (since := "2024-10-01")]
+alias uniformEmbedding_equivRealProd := isUniformEmbedding_equivRealProd
 
 instance : CompleteSpace ℂ :=
-  (completeSpace_congr uniformEmbedding_equivRealProd).mpr inferInstance
+  (completeSpace_congr isUniformEmbedding_equivRealProd).mpr inferInstance
 
 instance instT2Space : T2Space ℂ := TopologicalSpace.t2Space_of_metrizableSpace
 

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -103,7 +103,7 @@ variable (hT : Dense (T.domain : Set E))
 /-- The unique continuous extension of the operator `adjointDomainMkCLM` to `E`. -/
 def adjointDomainMkCLMExtend (y : T.adjointDomain) : E →L[𝕜] 𝕜 :=
   (T.adjointDomainMkCLM y).extend (Submodule.subtypeL T.domain) hT.denseRange_val
-    uniformEmbedding_subtype_val.toUniformInducing
+    isUniformEmbedding_subtype_val.toUniformInducing
 
 @[simp]
 theorem adjointDomainMkCLMExtend_apply (y : T.adjointDomain) (x : T.domain) :

Mathlib/Analysis/Normed/Algebra/Unitization.lean

@@ -208,11 +208,14 @@ def uniformEquivProd : (Unitization 𝕜 A) ≃ᵤ (𝕜 × A) :=
 instance instBornology : Bornology (Unitization 𝕜 A) :=
   Bornology.induced <| addEquiv 𝕜 A
 
-theorem uniformEmbedding_addEquiv {𝕜} [NontriviallyNormedField 𝕜] :
-    UniformEmbedding (addEquiv 𝕜 A) where
+theorem isUniformEmbedding_addEquiv {𝕜} [NontriviallyNormedField 𝕜] :
+    IsUniformEmbedding (addEquiv 𝕜 A) where
   comap_uniformity := rfl
   inj := (addEquiv 𝕜 A).injective
 
+@[deprecated (since := "2024-10-01")]
+alias uniformEmbedding_addEquiv := isUniformEmbedding_addEquiv
+
 /-- `Unitization 𝕜 A` is complete whenever `𝕜` and `A` are also. -/
 instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] :
     CompleteSpace (Unitization 𝕜 A) :=

Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

@@ -50,7 +50,7 @@ noncomputable def uniformEquiv_unitization_addEquiv_prod :
 
 instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] :
     CompleteSpace (WithLp 1 (Unitization 𝕜 A)) :=
-  completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).uniformEmbedding |>.mpr
+  completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).isUniformEmbedding |>.mpr
     CompleteSpace.prod
 
 variable {𝕜 A}

Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean

@@ -153,9 +153,13 @@ variable [Ring 𝕜] [Ring 𝕜₂]
 variable [NormedAddCommGroup E] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F]
 variable {σ : 𝕜 →+* 𝕜₂} (f g : E →SL[σ] F) (x y z : E)
 
-theorem ContinuousLinearMap.uniformEmbedding_of_bound {K : ℝ≥0} (hf : ∀ x, ‖x‖ ≤ K * ‖f x‖) :
-    UniformEmbedding f :=
-  (AddMonoidHomClass.antilipschitz_of_bound f hf).uniformEmbedding f.uniformContinuous
+theorem ContinuousLinearMap.isUniformEmbedding_of_bound {K : ℝ≥0} (hf : ∀ x, ‖x‖ ≤ K * ‖f x‖) :
+    IsUniformEmbedding f :=
+  (AddMonoidHomClass.antilipschitz_of_bound f hf).isUniformEmbedding f.uniformContinuous
+
+@[deprecated (since := "2024-10-01")]
+alias ContinuousLinearMap.uniformEmbedding_of_bound :=
+  ContinuousLinearMap.isUniformEmbedding_of_bound
 
 end Normed
 

Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean

@@ -230,7 +230,7 @@ variable {N : ℝ≥0} (h_e : ∀ x, ‖x‖ ≤ N * ‖e x‖) [RingHomIsometri
 /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the
 norm of the extension of `f` along `e` is bounded by `N * ‖f‖`. -/
 theorem opNorm_extend_le :
-    ‖f.extend e h_dense (uniformEmbedding_of_bound _ h_e).toUniformInducing‖ ≤ N * ‖f‖ := by
+    ‖f.extend e h_dense (isUniformEmbedding_of_bound _ h_e).toUniformInducing‖ ≤ N * ‖f‖ := by
   -- Add `opNorm_le_of_dense`?
   refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ ?_) fun x ↦ ?_)
   · cases le_total 0 N with

Mathlib/Analysis/Quaternion.lean

@@ -195,8 +195,8 @@ theorem continuous_im : Continuous fun q : ℍ => q.im := by
   simpa only [← sub_self_re] using continuous_id.sub (continuous_coe.comp continuous_re)
 
 instance : CompleteSpace ℍ :=
-  haveI : UniformEmbedding linearIsometryEquivTuple.toLinearEquiv.toEquiv.symm :=
-    linearIsometryEquivTuple.toContinuousLinearEquiv.symm.uniformEmbedding
+  haveI : IsUniformEmbedding linearIsometryEquivTuple.toLinearEquiv.toEquiv.symm :=
+    linearIsometryEquivTuple.toContinuousLinearEquiv.symm.isUniformEmbedding
   (completeSpace_congr this).1 inferInstance
 
 section infinite_sum

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -1064,7 +1064,7 @@ theorem MeasureTheory.Memℒp.of_comp_antilipschitzWith {α E F} {K'} [Measurabl
     rw [← dist_zero_right, ← dist_zero_right, ← g0]
     apply hg'.le_mul_dist
   have B : AEStronglyMeasurable f μ :=
-    (hg'.uniformEmbedding hg).embedding.aestronglyMeasurable_comp_iff.1 hL.1
+    (hg'.isUniformEmbedding hg).embedding.aestronglyMeasurable_comp_iff.1 hL.1
   exact hL.of_le_mul B (Filter.Eventually.of_forall A)
 
 namespace LipschitzWith

Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

@@ -679,16 +679,18 @@ variable [Fact (1 ≤ p)]
 protected theorem uniformContinuous : UniformContinuous ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
   uniformContinuous_comap
 
-protected theorem uniformEmbedding : UniformEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
-  uniformEmbedding_comap Subtype.val_injective
+lemma isUniformEmbedding : IsUniformEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
+  isUniformEmbedding_comap Subtype.val_injective
+
+@[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding
 
 protected theorem uniformInducing : UniformInducing ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
-  simpleFunc.uniformEmbedding.toUniformInducing
+  simpleFunc.isUniformEmbedding.toUniformInducing
 
 lemma isDenseEmbedding (hp_ne_top : p ≠ ∞) :
     IsDenseEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := by
   borelize E
-  apply simpleFunc.uniformEmbedding.isDenseEmbedding
+  apply simpleFunc.isUniformEmbedding.isDenseEmbedding
   intro f
   rw [mem_closure_iff_seq_limit]
   have hfi' : Memℒp f p μ := Lp.memℒp f

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -712,7 +712,7 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi
     rw [← top_le_iff, ← volume_Ici (a := b)]
     exact measure_mono hb
   rwa [B, ← Embedding.tendsto_nhds_iff] at A
-  exact (Completion.uniformEmbedding_coe E).embedding
+  exact (Completion.isUniformEmbedding_coe E).embedding
 
 variable [CompleteSpace E]
 
@@ -909,7 +909,7 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Iic
     rw [← volume_Iic (a := b)]
     exact measure_mono hb
   rwa [B, ← Embedding.tendsto_nhds_iff] at A
-  exact (Completion.uniformEmbedding_coe E).embedding
+  exact (Completion.isUniformEmbedding_coe E).embedding
 
 variable [CompleteSpace E]
 

Mathlib/MeasureTheory/Integral/SetIntegral.lean

@@ -1260,7 +1260,7 @@ variable [NormedSpace ℝ F] [NormedSpace ℝ E]
 
 theorem integral_comp_comm (L : E ≃L[𝕜] F) (φ : X → E) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) := by
   have : CompleteSpace E ↔ CompleteSpace F :=
-    completeSpace_congr (e := L.toEquiv) L.uniformEmbedding
+    completeSpace_congr (e := L.toEquiv) L.isUniformEmbedding
   obtain ⟨_, _⟩|⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this
   · exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _
   · simp [integral, *]