chore(Topology/UniformSpace): rename uniformContinuous_iff to uniformContinuous_iff_le_comap (leanprover-community#39762)

Rename `uniformContinuous_iff` to `uniformContinuous_iff_le_comap`, to match `continuous_iff_le_induced`, and also to have symmetry with a possible lemma `uniformContinuous_iff_map_le` which doesn't exist now but could be added in the future.

Author: plp127

Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

@@ -51,7 +51,7 @@ noncomputable def uniformEquiv_unitization_addEquiv_prod :
     WithLp 1 (Unitization 𝕜 A) ≃ᵤ WithLp 1 (𝕜 × A) :=
   { unitization_addEquiv_prod 𝕜 A with
     uniformContinuous_invFun := uniformContinuous_comap' uniformContinuous_id
-    uniformContinuous_toFun := uniformContinuous_iff.mpr le_rfl }
+    uniformContinuous_toFun := uniformContinuous_iff_le_comap.mpr le_rfl }
 
 instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] :
     CompleteSpace (WithLp 1 (Unitization 𝕜 A)) :=

Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean

@@ -195,15 +195,15 @@ theorem coverEntropy_image_le_of_uniformContinuous [UniformSpace X] [UniformSpac
     {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) :
     coverEntropy T (φ '' F) ≤ coverEntropy S F := by
   rw [coverEntropy_image_of_comap _ h F]
-  exact coverEntropy_antitone S F (uniformContinuous_iff.1 h')
+  exact coverEntropy_antitone S F (uniformContinuous_iff_le_comap.1 h')
 
 /-- The entropy of `φ '' F` is at most the entropy of `F` if `φ` is uniformly continuous. This
   version uses a `liminf`. -/
 theorem coverEntropyInf_image_le_of_uniformContinuous [UniformSpace X] [UniformSpace Y] {S : X → X}
     {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) :
     coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F := by
   rw [coverEntropyInf_image_of_comap _ h F]
-  exact coverEntropyInf_antitone S F (uniformContinuous_iff.1 h')
+  exact coverEntropyInf_antitone S F (uniformContinuous_iff_le_comap.1 h')
 
 lemma coverEntropy_image_le_of_uniformContinuousOn_invariant [UniformSpace X] [UniformSpace Y]
     {S : X → X} {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) {F G : Set X}

Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

@@ -338,8 +338,8 @@ def opUniformEquivRight
   letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
   letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
   refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-  · simp [uniformContinuous_iff, ← comap_op_leftUniformSpace]
-  · simp [uniformContinuous_iff, ← comap_op_leftUniformSpace, ← UniformSpace.comap_comap]
+  · simp [uniformContinuous_iff_le_comap, ← comap_op_leftUniformSpace]
+  · simp [uniformContinuous_iff_le_comap, ← comap_op_leftUniformSpace, ← UniformSpace.comap_comap]
 
 /-- The equivalence between a topological group `G` and `Gᵐᵒᵖ` as a uniform equivalence when `G`
 is equipped with the left uniformity and `Gᵐᵒᵖ` with the right uniformity. -/
@@ -352,8 +352,8 @@ def opUniformEquivLeft
   letI : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
   letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
   refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-  · simp [uniformContinuous_iff, ← comap_op_rightUniformSpace]
-  · simp [uniformContinuous_iff, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap]
+  · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace]
+  · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap]
 
 end MulOpposite
 
@@ -381,11 +381,11 @@ def UniformEquiv.inv : @UniformEquiv G G (IsTopologicalGroup.rightUniformSpace G
     (IsTopologicalGroup.leftUniformSpace G) := by
   have A : @UniformContinuous G G (IsTopologicalGroup.rightUniformSpace G)
       (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) := by
-    apply uniformContinuous_iff.2
+    apply uniformContinuous_iff_le_comap.2
     rw [← comap_inv_leftUniformSpace]
   have B : @UniformContinuous G G (IsTopologicalGroup.leftUniformSpace G)
       (IsTopologicalGroup.rightUniformSpace G) (Equiv.inv G) := by
-    apply uniformContinuous_iff.2
+    apply uniformContinuous_iff_le_comap.2
     rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]
     simp
   exact @UniformEquiv.mk G G (IsTopologicalGroup.rightUniformSpace G)

Mathlib/Topology/UniformSpace/Basic.lean

@@ -454,13 +454,16 @@ theorem UniformSpace.comap_mono {α γ} {f : α → γ} :
     Monotone fun u : UniformSpace γ => u.comap f := fun _ _ hu =>
   Filter.comap_mono hu
 
-theorem uniformContinuous_iff {α β} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} :
-    UniformContinuous f ↔ uα ≤ uβ.comap f :=
+theorem uniformContinuous_iff_le_comap {α β} {uα : UniformSpace α} {uβ : UniformSpace β}
+    {f : α → β} : UniformContinuous f ↔ uα ≤ uβ.comap f :=
   Filter.map_le_iff_le_comap
 
+@[deprecated (since := "2026-05-23")]
+alias uniformContinuous_iff := uniformContinuous_iff_le_comap
+
 theorem le_iff_uniformContinuous_id {u v : UniformSpace α} :
     u ≤ v ↔ @UniformContinuous _ _ u v id := by
-  rw [uniformContinuous_iff, uniformSpace_comap_id, id]
+  rw [uniformContinuous_iff_le_comap, uniformSpace_comap_id, id]
 
 theorem uniformContinuous_comap {f : α → β} [u : UniformSpace β] :
     @UniformContinuous α β (UniformSpace.comap f u) u f :=
@@ -520,7 +523,7 @@ variable [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β} {
 
 theorem UniformContinuous.continuous (hf : UniformContinuous f) : Continuous f :=
   continuous_iff_le_induced.mpr <| UniformSpace.toTopologicalSpace_mono <|
-    uniformContinuous_iff.1 hf
+    uniformContinuous_iff_le_comap.1 hf
 
 lemma UniformContinuous.uniformContinuousOn (hf : UniformContinuous f) :
     UniformContinuousOn f s :=

Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

@@ -84,6 +84,6 @@ variable {x} in
 /-- On a space with a discrete uniformity, any function is uniformly continuous. -/
 theorem uniformContinuous {Y : Type*} [UniformSpace Y] (f : X → Y) :
     UniformContinuous f := by
-  simp only [uniformContinuous_iff, DiscreteUniformity.eq_bot, bot_le]
+  simp only [uniformContinuous_iff_le_comap, DiscreteUniformity.eq_bot, bot_le]
 
 end DiscreteUniformity

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

@@ -404,10 +404,10 @@ protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β}
     (hf : UniformContinuous f) :
     UniformContinuous (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) := by
   -- This is a direct consequence of `UniformFun.comap_eq`
-    refine uniformContinuous_iff.mpr ?_
+    refine uniformContinuous_iff_le_comap.mpr ?_
     calc
       𝒰(α, γ, _) ≤ 𝒰(α, γ, ‹UniformSpace β›.comap f) :=
-        UniformFun.mono (uniformContinuous_iff.mp hf)
+        UniformFun.mono (uniformContinuous_iff_le_comap.mp hf)
       _ = 𝒰(α, β, _).comap (f ∘ ·) := by exact UniformFun.comap_eq
 
 /-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ γ) ≃ᵤ (α →ᵤ β)` by
@@ -892,8 +892,9 @@ More precisely, if `f : γ → β` is uniformly continuous, then
 protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β}
     (hf : UniformContinuous f) : UniformContinuous (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) := by
   -- This is a direct consequence of `UniformOnFun.comap_eq`
-  rw [uniformContinuous_iff]
-  exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq
+  rw [uniformContinuous_iff_le_comap]
+  exact (UniformOnFun.mono (uniformContinuous_iff_le_comap.mp hf)
+    subset_rfl).trans_eq UniformOnFun.comap_eq
 
 /-- Post-composition by a uniform inducing is a uniform inducing for the
 uniform structures of `𝔖`-convergence.
@@ -1120,9 +1121,9 @@ theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ
     simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union,
       ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS
   refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)
-  · rw [← uniformContinuous_iff]
+  · rw [← uniformContinuous_iff_le_comap]
     exact UniformOnFun.precomp_uniformContinuous h_image₁
-  · rw [← uniformContinuous_iff]
+  · rw [← uniformContinuous_iff_le_comap]
     exact UniformOnFun.precomp_uniformContinuous h_image₂
   · simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf,
       ← UniformSpace.comap_comap]
@@ -1145,7 +1146,7 @@ theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ
   -- With a better theory of ideals we may be able to simplify the following by replacing `𝔗 i`
   -- by `(φ i ⁻¹' ·) '' 𝔖`.
   refine le_antisymm (le_iInf fun i ↦ ?_) (le_iInf₂ fun S hS ↦ ?_)
-  · rw [← uniformContinuous_iff]
+  · rw [← uniformContinuous_iff_le_comap]
     exact UniformOnFun.precomp_uniformContinuous (h_image i)
   · simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
     exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl